Mathlib.CategoryTheory.Limits.Shapes.Biproducts

CategoryTheory.Limits.Bicone structure

(F : J → C)

Full source

/-- A `c : Bicone F` is:
* an object `c.pt` and
* morphisms `π j : pt ⟶ F j` and `ι j : F j ⟶ pt` for each `j`,
* such that `ι j ≫ π j'` is the identity when `j = j'` and zero otherwise.
-/
structure Bicone (F : J → C) where
  pt : C
  π : ∀ j, pt ⟶ F j
  ι : ∀ j, F j ⟶ pt
  ι_π : ∀ j j', ι j ≫ π j' =
    if h : j = j' then eqToHom (congrArg F h) else 0 := by aesop

Bicone structure for biproducts

Informal description

A bicone for a family of objects $ F : J \to C $ in a category $ C $ consists of: - An object $ \text{pt} $ (the "point" of the bicone) - For each $ j \in J $, morphisms $ \pi_j : \text{pt} \to F_j $ and $ \iota_j : F_j \to \text{pt} $ such that: - $ \iota_j \circ \pi_j = \text{id}_{F_j} $ for each $ j $ - $ \iota_j \circ \pi_{j'} = 0 $ whenever $ j \neq j' $ This structure simultaneously encodes both cone and cocone data that are compatible in a way that makes them suitable for defining biproducts.

CategoryTheory.Limits.bicone_ι_π_self theorem

{F : J → C} (B : Bicone F) (j : J) : B.ι j ≫ B.π j = 𝟙 (F j)

Full source

@[reassoc (attr := simp)]
theorem bicone_ι_π_self {F : J → C} (B : Bicone F) (j : J) : B.ι j ≫ B.π j = 𝟙 (F j) := by
  simpa using B.ι_π j j

Identity Property of Bicone Components: $\iota_j \circ \pi_j = \text{id}_{F_j}$

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, and for any index $j \in J$, the composition of the $j$-th inclusion morphism $\iota_j$ and the $j$-th projection morphism $\pi_j$ equals the identity morphism on $F_j$, i.e., $\iota_j \circ \pi_j = \text{id}_{F_j}$.

CategoryTheory.Limits.bicone_ι_π_ne theorem

{F : J → C} (B : Bicone F) {j j' : J} (h : j ≠ j') : B.ι j ≫ B.π j' = 0

Full source

@[reassoc (attr := simp)]
theorem bicone_ι_π_ne {F : J → C} (B : Bicone F) {j j' : J} (h : j ≠ j') : B.ι j ≫ B.π j' = 0 := by
  simpa [h] using B.ι_π j j'

Vanishing of Bicone Compositions for Distinct Indices: $\iota_j \circ \pi_{j'} = 0$ when $j \ne j'$

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, and for any distinct indices $j \ne j'$ in $J$, the composition of the injection morphism $\iota_j : F_j \to B.\text{pt}$ with the projection morphism $\pi_{j'} : B.\text{pt} \to F_{j'}$ is the zero morphism, i.e., $\iota_j \circ \pi_{j'} = 0$.

CategoryTheory.Limits.BiconeMorphism structure

{F : J → C} (A B : Bicone F)

Full source

/-- A bicone morphism between two bicones for the same diagram is a morphism of the bicone points
which commutes with the cone and cocone legs. -/
structure BiconeMorphism {F : J → C} (A B : Bicone F) where
  /-- A morphism between the two vertex objects of the bicones -/
  hom : A.pt ⟶ B.pt
  /-- The triangle consisting of the two natural transformations and `hom` commutes -/
  wπ : ∀ j : J, hom ≫ B.π j = A.π j := by aesop_cat
  /-- The triangle consisting of the two natural transformations and `hom` commutes -/
  wι : ∀ j : J, A.ι j ≫ hom = B.ι j := by aesop_cat

Bicone morphism

Informal description

A morphism between two bicones $ A $ and $ B $ for the same diagram $ F : J \to C $ in a category $ C $ consists of a morphism $ f : A.\text{pt} \to B.\text{pt} $ between their apex objects that commutes with both the cone legs ($ f \circ A.\pi_j = B.\pi_j $ for all $ j \in J $) and the cocone legs ($ A.\iota_j \circ f = B.\iota_j $ for all $ j \in J $).

CategoryTheory.Limits.Bicone.category instance

: Category (Bicone F)

Full source

/-- The category of bicones on a given diagram. -/
@[simps]
instance Bicone.category : Category (Bicone F) where
  Hom A B := BiconeMorphism A B
  comp f g := { hom := f.hom ≫ g.hom }
  id B := { hom := 𝟙 B.pt }

-- Porting note: if we do not have `simps` automatically generate the lemma for simplifying
-- the `hom` field of a category, we need to write the `ext` lemma in terms of the categorical
-- morphism, rather than the underlying structure.

The Category of Bicones over a Diagram $F$

Informal description

For any family of objects $F : J \to C$ in a category $C$, the collection of bicones over $F$ forms a category. In this category: - Objects are bicones $(X, \pi_j, \iota_j)$ where $X$ is an object in $C$, and $\pi_j : X \to F_j$ and $\iota_j : F_j \to X$ are morphisms satisfying $\iota_j \circ \pi_j = \text{id}_{F_j}$ and $\iota_j \circ \pi_{j'} = 0$ for $j \neq j'$. - Morphisms between bicones $(X, \pi_j, \iota_j)$ and $(Y, \pi'_j, \iota'_j)$ are morphisms $f : X \to Y$ in $C$ that commute with both the $\pi$ and $\iota$ maps (i.e., $f \circ \pi_j = \pi'_j$ and $\iota_j \circ f = \iota'_j$ for all $j$).

CategoryTheory.Limits.BiconeMorphism.ext theorem

{c c' : Bicone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Full source

@[ext]
theorem BiconeMorphism.ext {c c' : Bicone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g := by
  cases f
  cases g
  congr

Extensionality of Bicone Morphisms

Informal description

For any two morphisms $f, g$ between bicones $c$ and $c'$ over the same diagram $F$, if the underlying morphisms $f.\text{hom}$ and $g.\text{hom}$ are equal, then $f = g$ as bicone morphisms.

CategoryTheory.Limits.Bicones.functoriality definition

(G : C ⥤ D) [Functor.PreservesZeroMorphisms G] : Bicone F ⥤ Bicone (G.obj ∘ F)

Full source

/-- A functor `G : C ⥤ D` sends bicones over `F` to bicones over `G.obj ∘ F` functorially. -/
@[simps]
def functoriality (G : C ⥤ D) [Functor.PreservesZeroMorphisms G] :
    BiconeBicone F ⥤ Bicone (G.obj ∘ F) where
  obj A :=
    { pt := G.obj A.pt
      π := fun j => G.map (A.π j)
      ι := fun j => G.map (A.ι j)
      ι_π := fun i j => (Functor.map_comp _ _ _).symm.trans <| by
        rw [A.ι_π]
        aesop_cat }
  map f :=
    { hom := G.map f.hom
      wπ := fun j => by simp [-BiconeMorphism.wπ, ← f.wπ j]
      wι := fun j => by simp [-BiconeMorphism.wι, ← f.wι j] }

Functoriality of bicones under a zero-preserving functor

Informal description

Given a functor $ G : C \to D $ that preserves zero morphisms, the functoriality construction maps a bicone $ A $ over a diagram $ F : J \to C $ to a bicone over $ G \circ F $ in $ D $. Specifically: - The object part sends a bicone $ A $ with point $ A.\text{pt} $ to a bicone with point $ G(A.\text{pt}) $, where the projection and injection morphisms are obtained by applying $ G $ to $ A.\pi_j $ and $ A.\iota_j $ respectively. - The morphism part sends a bicone morphism $ f $ to the morphism $ G(f.\text{hom}) $, which commutes with the projected and injected morphisms in the image bicone. This construction ensures that the relations $ \iota_j \circ \pi_j = \text{id} $ and $ \iota_j \circ \pi_{j'} = 0 $ for $ j \neq j' $ are preserved by $ G $.

CategoryTheory.Limits.Bicones.functoriality_full instance

[G.PreservesZeroMorphisms] [G.Full] [G.Faithful] : (functoriality F G).Full

Full source

instance functoriality_full [G.PreservesZeroMorphisms] [G.Full] [G.Faithful] :
    (functoriality F G).Full where
  map_surjective t :=
   ⟨{ hom := G.preimage t.hom
      wι := fun j => G.map_injective (by simpa using t.wι j)
      wπ := fun j => G.map_injective (by simpa using t.wπ j) }, by aesop_cat⟩

Fullness of Bicone Functoriality under Full and Faithful Functors

Informal description

Given a full and faithful functor $G : C \to D$ that preserves zero morphisms, the functoriality construction that maps bicones over $F : J \to C$ to bicones over $G \circ F$ in $D$ is full. This means that for any two bicones $c$ and $c'$ over $F$, every morphism between their images under the functoriality construction is induced by a morphism between $c$ and $c'$ in $C$.

CategoryTheory.Limits.Bicones.functoriality_faithful instance

[G.PreservesZeroMorphisms] [G.Faithful] : (functoriality F G).Faithful

Full source

instance functoriality_faithful [G.PreservesZeroMorphisms] [G.Faithful] :
    (functoriality F G).Faithful where
  map_injective {_X} {_Y} f g h :=
    BiconeMorphism.ext f g <| G.map_injective <| congr_arg BiconeMorphism.hom h

Faithfulness of Bicone Functoriality under a Faithful Zero-Preserving Functor

Informal description

Given a functor $G : C \to D$ that preserves zero morphisms and is faithful, the functoriality construction that maps bicones over $F : J \to C$ to bicones over $G \circ F$ in $D$ is also faithful. This means that if two morphisms between bicones are mapped to the same morphism under this construction, then the original morphisms must have been equal.

CategoryTheory.Limits.Bicone.toConeFunctor definition

: Bicone F ⥤ Cone (Discrete.functor F)

Full source

/-- Extract the cone from a bicone. -/
def toConeFunctor : BiconeBicone F ⥤ Cone (Discrete.functor F) where
  obj B := { pt := B.pt, π := { app := fun j => B.π j.as } }
  map {_ _} F := { hom := F.hom, w := fun _ => F.wπ _ }

Bicone to Cone Functor

Informal description

The functor that converts a bicone $B$ over a family of objects $F : J \to C$ into a cone over the discrete functor associated with $F$. Specifically: - The object part maps a bicone $(X, \pi_j, \iota_j)$ to a cone with apex $X$ and projections $\pi_j : X \to F_j$. - The morphism part maps a bicone morphism $f : X \to Y$ to a cone morphism with the same underlying morphism $f$, which commutes with the projections. This functor establishes a relationship between bicones and cones in the category $C$.

CategoryTheory.Limits.Bicone.toCone abbrev

(B : Bicone F) : Cone (Discrete.functor F)

Full source

/-- A shorthand for `toConeFunctor.obj` -/
abbrev toCone (B : Bicone F) : Cone (Discrete.functor F) := toConeFunctor.obj B

Construction of a Cone from a Bicone

Informal description

Given a bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, the construction $B.\text{toCone}$ yields a cone over the discrete functor associated with $F$. Specifically, the cone has apex $B.\text{pt}$ and projections given by the morphisms $B.\pi_j : B.\text{pt} \to F_j$ from the bicone structure.

CategoryTheory.Limits.Bicone.toCone_pt theorem

(B : Bicone F) : B.toCone.pt = B.pt

Full source

@[simp] theorem toCone_pt (B : Bicone F) : B.toCone.pt = B.pt := rfl

Apex Equality for Bicone-to-Cone Construction

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, the apex of the associated cone $B.\text{toCone}$ is equal to the apex $B.\text{pt}$ of the bicone.

CategoryTheory.Limits.Bicone.toCone_π_app theorem

(B : Bicone F) (j : Discrete J) : B.toCone.π.app j = B.π j.as

Full source

@[simp] theorem toCone_π_app (B : Bicone F) (j : Discrete J) : B.toCone.π.app j = B.π j.as := rfl

Equality of Cone Projections from Bicone Structure

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, and for any discrete object $j$ in the discrete category associated with $J$, the projection morphism $\pi$ of the cone $B.\text{toCone}$ at $j$ is equal to the projection morphism $B.\pi_{j.\text{as}}$ from the bicone structure.

CategoryTheory.Limits.Bicone.toCone_π_app_mk theorem

(B : Bicone F) (j : J) : B.toCone.π.app ⟨j⟩ = B.π j

Full source

theorem toCone_π_app_mk (B : Bicone F) (j : J) : B.toCone.π.app ⟨j⟩ = B.π j := rfl

Equality of Bicone and Cone Projections at Discrete Index

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, and for any index $j \in J$, the projection morphism of the associated cone at the object $\langle j \rangle$ (viewed as an object in the discrete category) equals the projection morphism $\pi_j$ from the bicone structure. That is, $B.\text{toCone}.\pi.\text{app}(\langle j \rangle) = B.\pi_j$.

CategoryTheory.Limits.Bicone.toCone_proj theorem

(B : Bicone F) (j : J) : Fan.proj B.toCone j = B.π j

Full source

@[simp] theorem toCone_proj (B : Bicone F) (j : J) : Fan.proj B.toCone j = B.π j := rfl

Equality of Bicone and Cone Projections at Index $j$

Informal description

Given a bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, the projection morphism $\pi_j$ of the associated cone $B.\text{toCone}$ at index $j \in J$ is equal to the projection morphism $B.\pi_j$ from the bicone structure.

CategoryTheory.Limits.Bicone.toCoconeFunctor definition

: Bicone F ⥤ Cocone (Discrete.functor F)

Full source

/-- Extract the cocone from a bicone. -/
def toCoconeFunctor : BiconeBicone F ⥤ Cocone (Discrete.functor F) where
  obj B := { pt := B.pt, ι := { app := fun j => B.ι j.as } }
  map {_ _} F := { hom := F.hom, w := fun _ => F.wι _ }

Bicone to Cocone Functor

Informal description

The functor that converts a bicone $B$ over a diagram $F : J \to C$ into a cocone over the discrete functor of $F$. Specifically: - For each bicone object $B$, the cocone has the same point $B.pt$ - The cocone's injection morphisms are given by the bicone's $\iota$ maps: $\iota_j : F_j \to B.pt$ for each $j \in J$ - For any morphism $f$ between bicones, the corresponding cocone morphism uses the same underlying morphism $f.hom$ and satisfies the appropriate commutativity conditions with the $\iota$ maps. This construction preserves the cocone structure while forgetting the bicone's projection maps $\pi_j$.

CategoryTheory.Limits.Bicone.toCocone abbrev

(B : Bicone F) : Cocone (Discrete.functor F)

Full source

/-- A shorthand for `toCoconeFunctor.obj` -/
abbrev toCocone (B : Bicone F) : Cocone (Discrete.functor F) := toCoconeFunctor.obj B

Construction of Cocone from Bicone

Informal description

Given a bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, the function `toCocone` constructs a cocone over the discrete functor of $F$. Specifically: - The cocone's vertex is $B.\text{pt}$. - For each $j \in J$, the cocone's injection morphism is given by $B.\iota_j : F_j \to B.\text{pt}$.

CategoryTheory.Limits.Bicone.toCocone_pt theorem

(B : Bicone F) : B.toCocone.pt = B.pt

Full source

@[simp] theorem toCocone_pt (B : Bicone F) : B.toCocone.pt = B.pt := rfl

Vertex Equality in Bicone-to-Cocone Construction

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$, the vertex (point) of the associated cocone $B.\text{toCocone}$ is equal to the vertex $B.\text{pt}$ of the bicone itself.

CategoryTheory.Limits.Bicone.toCocone_ι_app theorem

(B : Bicone F) (j : Discrete J) : B.toCocone.ι.app j = B.ι j.as

Full source

@[simp]
theorem toCocone_ι_app (B : Bicone F) (j : Discrete J) : B.toCocone.ι.app j = B.ι j.as := rfl

Equality of Cocone Injection and Bicone Injection Morphisms

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, and for any object $j$ in the discrete category of $J$, the cocone injection morphism $\iota$ at $j$ is equal to the bicone injection morphism $\iota_{j.\text{as}}$, where $j.\text{as}$ denotes the underlying object in $J$.

CategoryTheory.Limits.Bicone.toCocone_inj theorem

(B : Bicone F) (j : J) : Cofan.inj B.toCocone j = B.ι j

Full source

@[simp] theorem toCocone_inj (B : Bicone F) (j : J) : Cofan.inj B.toCocone j = B.ι j := rfl

Equality of Cocone Injection and Bicone Inclusion Morphisms

Informal description

Given a bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, for any index $j \in J$, the $j$-th injection morphism of the cocone constructed from $B$ is equal to the inclusion morphism $B.\iota_j$ from the bicone.

CategoryTheory.Limits.Bicone.toCocone_ι_app_mk theorem

(B : Bicone F) (j : J) : B.toCocone.ι.app ⟨j⟩ = B.ι j

Full source

theorem toCocone_ι_app_mk (B : Bicone F) (j : J) : B.toCocone.ι.app ⟨j⟩ = B.ι j := rfl

Cocone Injection at Index $j$ Equals Bicone Inclusion

Informal description

For any bicone $B$ over a family of objects $F : J \to C$ in a category $C$ with zero morphisms, and for any index $j \in J$, the cocone injection morphism at the object $\langle j \rangle$ (viewed as an object in the discrete category) is equal to the bicone's inclusion morphism $B.\iota_j : F_j \to B.\text{pt}$.

CategoryTheory.Limits.Bicone.ofLimitCone definition

{f : J → C} {t : Cone (Discrete.functor f)} (ht : IsLimit t) : Bicone f

Full source

/-- We can turn any limit cone over a discrete collection of objects into a bicone. -/
@[simps]
def ofLimitCone {f : J → C} {t : Cone (Discrete.functor f)} (ht : IsLimit t) : Bicone f where
  pt := t.pt
  π j := t.π.app ⟨j⟩
  ι j := ht.lift (Fan.mk _ fun j' => if h : j = j' then eqToHom (congr_arg f h) else 0)
  ι_π j j' := by simp

Bicone construction from a limit cone

Informal description

Given a limit cone `t` over a discrete diagram of objects `f : J → C` in a category `C` with zero morphisms, the function constructs a bicone where: - The point is the apex of the cone `t` - The projections `π j` are the cone's projections at each index `j` - The inclusions `ι j` are constructed using the universal property of the limit cone, defined as the lift of a fan where the morphisms are identity when `j = j'` and zero otherwise - The compatibility condition `ι j ≫ π j'` is satisfied (being identity when `j = j'` and zero otherwise)

CategoryTheory.Limits.Bicone.ι_of_isLimit theorem

 {f : J → C} {t : Bicone f} (ht : IsLimit t.toCone) (j : J) :
  t.ι j = ht.lift (Fan.mk _ fun j' => if h : j = j' then eqToHom (congr_arg f h) else 0)

Full source

theorem ι_of_isLimit {f : J → C} {t : Bicone f} (ht : IsLimit t.toCone) (j : J) :
    t.ι j = ht.lift (Fan.mk _ fun j' => if h : j = j' then eqToHom (congr_arg f h) else 0) :=
  ht.hom_ext fun j' => by
    rw [ht.fac]
    simp [t.ι_π]

Characterization of Bicone Inclusions via Limit Property

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, $F : J \to \mathcal{C}$ a family of objects, and $t$ a bicone over $F$. If $t.\text{toCone}$ is a limit cone, then for each index $j \in J$, the inclusion morphism $t.\iota_j$ is equal to the limit lift of the fan where: - The apex is $t.\text{pt}$ - For each $j' \in J$, the projection is the identity morphism (via $\text{eqToHom}$) when $j = j'$, and the zero morphism otherwise. In symbols: $$ t.\iota_j = \text{ht.lift}\left(\text{Fan.mk}\ t.\text{pt}\ \left(\lambda j' \mapsto \begin{cases} \text{eqToHom}(\text{congr\_arg}\ F\ h) & \text{if } h : j = j' \\ 0 & \text{otherwise} \end{cases}\right)\right) $$

CategoryTheory.Limits.Bicone.ofColimitCocone definition

{f : J → C} {t : Cocone (Discrete.functor f)} (ht : IsColimit t) : Bicone f

Full source

/-- We can turn any colimit cocone over a discrete collection of objects into a bicone. -/
@[simps]
def ofColimitCocone {f : J → C} {t : Cocone (Discrete.functor f)} (ht : IsColimit t) :
    Bicone f where
  pt := t.pt
  π j := ht.desc (Cofan.mk _ fun j' => if h : j' = j then eqToHom (congr_arg f h) else 0)
  ι j := t.ι.app ⟨j⟩
  ι_π j j' := by simp

Bicone construction from a colimit cocone

Informal description

Given a colimit cocone `t` over a discrete diagram of objects `f : J → C` in a category `C` with zero morphisms, the function constructs a bicone where: - The point is the apex of the cocone `t` - The inclusions `ι j` are the cocone's injections at each index `j` - The projections `π j` are constructed using the universal property of the colimit cocone, defined as the descent of a cofan where the morphisms are identity when `j' = j` and zero otherwise - The compatibility condition `ι j ≫ π j'` is satisfied (being identity when `j = j'` and zero otherwise)

CategoryTheory.Limits.Bicone.π_of_isColimit theorem

 {f : J → C} {t : Bicone f} (ht : IsColimit t.toCocone) (j : J) :
  t.π j = ht.desc (Cofan.mk _ fun j' => if h : j' = j then eqToHom (congr_arg f h) else 0)

Full source

theorem π_of_isColimit {f : J → C} {t : Bicone f} (ht : IsColimit t.toCocone) (j : J) :
    t.π j = ht.desc (Cofan.mk _ fun j' => if h : j' = j then eqToHom (congr_arg f h) else 0) :=
  ht.hom_ext fun j' => by
    rw [ht.fac]
    simp [t.ι_π]

Characterization of Bicone Projections via Colimit Property

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, $F : J \to \mathcal{C}$ a family of objects, and $t$ a bicone over $F$. If $t.\text{toCocone}$ is a colimit cocone, then for each index $j \in J$, the projection morphism $t.\pi_j$ is equal to the colimit descent of the cofan where: - The apex is $t.\text{pt}$ - For each $j' \in J$, the injection is the identity morphism (via $\text{eqToHom}$) when $j' = j$, and the zero morphism otherwise. In symbols: $$ t.\pi_j = \text{ht.desc}\left(\text{Cofan.mk}\ t.\text{pt}\ \left(\lambda j' \mapsto \begin{cases} \text{eqToHom}(\text{congr\_arg}\ F\ h) & \text{if } h : j' = j \\ 0 & \text{otherwise} \end{cases}\right)\right) $$

CategoryTheory.Limits.Bicone.IsBilimit structure

{F : J → C} (B : Bicone F)

Full source

/-- Structure witnessing that a bicone is both a limit cone and a colimit cocone. -/
structure IsBilimit {F : J → C} (B : Bicone F) where
  isLimit : IsLimit B.toCone
  isColimit : IsColimit B.toCocone

Bilimit Bicone

Informal description

A structure witnessing that a bicone $ B $ for a family of objects $ F : J \to C $ is both a limit cone and a colimit cocone. This means that the bicone simultaneously satisfies the universal properties of both a limit and a colimit for the diagram $ F $.

CategoryTheory.Limits.Bicone.subsingleton_isBilimit instance

{f : J → C} {c : Bicone f} : Subsingleton c.IsBilimit

Full source

instance subsingleton_isBilimit {f : J → C} {c : Bicone f} : Subsingleton c.IsBilimit :=
  ⟨fun _ _ => Bicone.IsBilimit.ext (Subsingleton.elim _ _) (Subsingleton.elim _ _)⟩

Uniqueness of Bicone Bilimit Property

Informal description

For any family of objects $ f : J \to C $ in a category $ C $ and any bicone $ c $ over $ f $, the property of $ c $ being a bilimit (i.e., simultaneously a limit and a colimit) is unique up to unique isomorphism. In other words, the type of witnesses that $ c $ is a bilimit is a subsingleton.

CategoryTheory.Limits.Bicone.whisker definition

{f : J → C} (c : Bicone f) (g : K ≃ J) : Bicone (f ∘ g)

Full source

/-- Whisker a bicone with an equivalence between the indexing types. -/
@[simps]
def whisker {f : J → C} (c : Bicone f) (g : K ≃ J) : Bicone (f ∘ g) where
  pt := c.pt
  π k := c.π (g k)
  ι k := c.ι (g k)
  ι_π k k' := by
    simp only [c.ι_π]
    split_ifs with h h' h' <;> simp [Equiv.apply_eq_iff_eq g] at h h' <;> tauto

Whiskering of a bicone along an index equivalence

Informal description

Given a bicone $ c $ for a family of objects $ f : J \to C $ in a category $ C $, and an equivalence $ g : K \simeq J $ between indexing types, the whiskered bicone $ c \circ g $ is defined by: - The same cone point $ \text{pt} $ as $ c $ - For each $ k \in K $, the projection $ \pi_k := \pi_{g(k)} $ and inclusion $ \iota_k := \iota_{g(k)} $ from the original bicone where the compositions $ \iota_k \circ \pi_{k'} $ satisfy the same identity/zero conditions as in the original bicone, translated through the equivalence $ g $.

CategoryTheory.Limits.Bicone.whiskerToCone definition

 {f : J → C} (c : Bicone f) (g : K ≃ J) :
  (c.whisker g).toCone ≅
    (Cones.postcompose (Discrete.functorComp f g).inv).obj (c.toCone.whisker (Discrete.functor (Discrete.mk ∘ g)))

Full source

/-- Taking the cone of a whiskered bicone results in a cone isomorphic to one gained
by whiskering the cone and postcomposing with a suitable isomorphism. -/
def whiskerToCone {f : J → C} (c : Bicone f) (g : K ≃ J) :
    (c.whisker g).toCone ≅
      (Cones.postcompose (Discrete.functorComp f g).inv).obj
        (c.toCone.whisker (Discrete.functor (Discrete.mk ∘ g))) :=
  Cones.ext (Iso.refl _) (by simp)

Isomorphism between whiskered bicone cone and postcomposed whiskered cone

Informal description

Given a bicone $ c $ over a family of objects $ f : J \to C $ in a category $ C $ and an equivalence $ g : K \simeq J $ between indexing types, the cone obtained from the whiskered bicone $ c \circ g $ is isomorphic to the cone obtained by: 1. First whiskering the original cone $ c.\text{toCone} $ along the discrete functor induced by $ g $ 2. Then postcomposing with the inverse of the natural isomorphism coming from the composition of $ f $ with $ g $ The isomorphism is witnessed by the identity morphism on the cone point, and the construction satisfies the necessary coherence conditions.

CategoryTheory.Limits.Bicone.whiskerToCocone definition

 {f : J → C} (c : Bicone f) (g : K ≃ J) :
  (c.whisker g).toCocone ≅
    (Cocones.precompose (Discrete.functorComp f g).hom).obj (c.toCocone.whisker (Discrete.functor (Discrete.mk ∘ g)))

Full source

/-- Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained
by whiskering the cocone and precomposing with a suitable isomorphism. -/
def whiskerToCocone {f : J → C} (c : Bicone f) (g : K ≃ J) :
    (c.whisker g).toCocone ≅
      (Cocones.precompose (Discrete.functorComp f g).hom).obj
        (c.toCocone.whisker (Discrete.functor (Discrete.mk ∘ g))) :=
  Cocones.ext (Iso.refl _) (by simp)

Isomorphism between whiskered bicone cocone and precomposed whiskered cocone

Informal description

Given a bicone $ c $ over a family of objects $ f : J \to C $ in a category $ C $, and an equivalence $ g : K \simeq J $ between indexing types, the cocone obtained from the whiskered bicone $ c \circ g $ is isomorphic to the cocone obtained by: 1. First whiskering the original cocone $ c.\text{toCocone} $ along the functor induced by $ g $ 2. Then precomposing with the natural isomorphism $ \text{Discrete.functorComp} \, f \, g $.hom The isomorphism between these cocones is given by the identity isomorphism on their common vertex.

CategoryTheory.Limits.Bicone.whiskerIsBilimitIff definition

{f : J → C} (c : Bicone f) (g : K ≃ J) : (c.whisker g).IsBilimit ≃ c.IsBilimit

Full source

/-- Whiskering a bicone with an equivalence between types preserves being a bilimit bicone. -/
noncomputable def whiskerIsBilimitIff {f : J → C} (c : Bicone f) (g : K ≃ J) :
    (c.whisker g).IsBilimit ≃ c.IsBilimit := by
  refine equivOfSubsingletonOfSubsingleton (fun hc => ⟨?_, ?_⟩) fun hc => ⟨?_, ?_⟩
  · let this := IsLimit.ofIsoLimit hc.isLimit (Bicone.whiskerToCone c g)
    let this := (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _) this
    exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this
  · let this := IsColimit.ofIsoColimit hc.isColimit (Bicone.whiskerToCocone c g)
    let this := (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _) this
    exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this
  · apply IsLimit.ofIsoLimit _ (Bicone.whiskerToCone c g).symm
    apply (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _).symm _
    exact IsLimit.whiskerEquivalence hc.isLimit (Discrete.equivalence g)
  · apply IsColimit.ofIsoColimit _ (Bicone.whiskerToCocone c g).symm
    apply (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _).symm _
    exact IsColimit.whiskerEquivalence hc.isColimit (Discrete.equivalence g)

Preservation of bilimit property under whiskering by equivalence

Informal description

Given a bicone $ c $ over a family of objects $ f : J \to C $ in a category $ C $ and an equivalence $ g : K \simeq J $ between indexing types, the whiskered bicone $ c \circ g $ is a bilimit (i.e., simultaneously a limit and a colimit) if and only if the original bicone $ c $ is a bilimit. This establishes that the property of being a bilimit is preserved under whiskering by an equivalence of indexing types.

CategoryTheory.Limits.LimitBicone structure

(F : J → C)

Full source

/-- A bicone over `F : J → C`, which is both a limit cone and a colimit cocone. -/
structure LimitBicone (F : J → C) where
  bicone : Bicone F
  isBilimit : bicone.IsBilimit

Limit Bicone

Informal description

A limit bicone over a functor $ F : J \to C $ consists of a cone that is both a limit cone and a colimit cocone for $ F $. This means it provides a simultaneous limit and colimit structure for the functor $ F $.

CategoryTheory.Limits.HasBiproduct structure

(F : J → C)

Full source

/-- `HasBiproduct F` expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram `F`. -/
class HasBiproduct (F : J → C) : Prop where mk' ::
  exists_biproduct : Nonempty (LimitBicone F)

Existence of Biproduct for a Diagram

Informal description

The structure `HasBiproduct F` asserts the existence of a bicone for the diagram `F : J → C` that is simultaneously a limit and a colimit of `F`. This means there exists an object `X` in the category `C` along with morphisms `π_j : X → F j` and `ι_j : F j → X` for each `j` in `J`, such that the `π_j` form a limit cone and the `ι_j` form a colimit cocone, with the additional condition that `ι_j ≫ π_j'` is the identity when `j = j'` and zero otherwise.

CategoryTheory.Limits.HasBiproduct.mk theorem

{F : J → C} (d : LimitBicone F) : HasBiproduct F

Full source

theorem HasBiproduct.mk {F : J → C} (d : LimitBicone F) : HasBiproduct F :=
  ⟨Nonempty.intro d⟩

Construction of Biproduct from Limit Bicone

Informal description

Given a functor $F \colon J \to C$ and a limit bicone $d$ over $F$, there exists a biproduct of $F$ in the category $C$. This means that $d$ simultaneously provides both a limit and a colimit structure for $F$.

CategoryTheory.Limits.getBiproductData definition

(F : J → C) [HasBiproduct F] : LimitBicone F

Full source

/-- Use the axiom of choice to extract explicit `BiproductData F` from `HasBiproduct F`. -/
def getBiproductData (F : J → C) [HasBiproduct F] : LimitBicone F :=
  Classical.choice HasBiproduct.exists_biproduct

Construction of Biproduct Data via Axiom of Choice

Informal description

Given a functor $ F : J \to C $ in a category $ C $ with zero morphisms, and assuming the existence of a biproduct for $ F $, the function `getBiproductData` uses the axiom of choice to extract explicit data for a limit bicone that serves as both a limit and a colimit for $ F $. This bicone consists of an object $ X $ and morphisms $ \pi_j : X \to F j $ and $ \iota_j : F j \to X $ for each $ j \in J $, satisfying the conditions that $ \iota_j \circ \pi_{j'} $ is the identity when $ j = j' $ and zero otherwise.

CategoryTheory.Limits.biproduct.bicone definition

(F : J → C) [HasBiproduct F] : Bicone F

Full source

/-- A bicone for `F` which is both a limit cone and a colimit cocone. -/
def biproduct.bicone (F : J → C) [HasBiproduct F] : Bicone F :=
  (getBiproductData F).bicone

Bicone structure of a biproduct

Informal description

Given a functor $ F : J \to C $ in a category $ C $ with zero morphisms and assuming the existence of a biproduct for $ F $, the function `biproduct.bicone` returns the bicone structure associated with the biproduct. This bicone consists of: - An object $ X $ (the biproduct object) - For each $ j \in J $, morphisms $ \pi_j : X \to F j $ (projections) and $ \iota_j : F j \to X $ (injections) such that: - $ \iota_j \circ \pi_j = \text{id}_{F j} $ for each $ j $ - $ \iota_j \circ \pi_{j'} = 0 $ whenever $ j \neq j' $ This bicone simultaneously provides both limit and colimit structures for the diagram $ F $.

CategoryTheory.Limits.biproduct.isBilimit definition

(F : J → C) [HasBiproduct F] : (biproduct.bicone F).IsBilimit

Full source

/-- `biproduct.bicone F` is a bilimit bicone. -/
def biproduct.isBilimit (F : J → C) [HasBiproduct F] : (biproduct.bicone F).IsBilimit :=
  (getBiproductData F).isBilimit

Biproduct bicone is a bilimit

Informal description

Given a functor $ F : J \to C $ in a category $ C $ with zero morphisms and assuming the existence of a biproduct for $ F $, the term `biproduct.isBilimit` witnesses that the bicone associated with the biproduct of $ F $ is both a limit and a colimit. This means the bicone satisfies the universal properties of being both a limit cone and a colimit cocone for the diagram $ F $.

CategoryTheory.Limits.biproduct.isLimit definition

(F : J → C) [HasBiproduct F] : IsLimit (biproduct.bicone F).toCone

Full source

/-- `biproduct.bicone F` is a limit cone. -/
def biproduct.isLimit (F : J → C) [HasBiproduct F] : IsLimit (biproduct.bicone F).toCone :=
  (getBiproductData F).isBilimit.isLimit

Biproduct cone is a limit

Informal description

Given a functor $ F : J \to C $ in a category $ C $ with zero morphisms and assuming the existence of a biproduct for $ F $, the term `biproduct.isLimit` witnesses that the cone associated with the biproduct bicone of $ F $ is a limit cone. This means the cone satisfies the universal property of being a limit for the diagram $ F $.

CategoryTheory.Limits.biproduct.isColimit definition

(F : J → C) [HasBiproduct F] : IsColimit (biproduct.bicone F).toCocone

Full source

/-- `biproduct.bicone F` is a colimit cocone. -/
def biproduct.isColimit (F : J → C) [HasBiproduct F] : IsColimit (biproduct.bicone F).toCocone :=
  (getBiproductData F).isBilimit.isColimit

Biproduct cocone is a colimit

Informal description

Given a functor $ F : J \to C $ in a category $ C $ with zero morphisms and assuming the existence of a biproduct for $ F $, the term `biproduct.isColimit` witnesses that the cocone derived from the biproduct bicone of $ F $ is a colimit. This means the cocone satisfies the universal property of being a colimit cocone for the diagram $ F $.

CategoryTheory.Limits.hasProduct_of_hasBiproduct instance

[HasBiproduct F] : HasProduct F

Full source

instance (priority := 100) hasProduct_of_hasBiproduct [HasBiproduct F] : HasProduct F :=
  HasLimit.mk
    { cone := (biproduct.bicone F).toCone
      isLimit := biproduct.isLimit F }

Biproducts Imply Products

Informal description

For any category $\mathcal{C}$ with zero morphisms and any functor $F : J \to \mathcal{C}$, if $F$ has a biproduct, then $F$ also has a product.

CategoryTheory.Limits.hasCoproduct_of_hasBiproduct instance

[HasBiproduct F] : HasCoproduct F

Full source

instance (priority := 100) hasCoproduct_of_hasBiproduct [HasBiproduct F] : HasCoproduct F :=
  HasColimit.mk
    { cocone := (biproduct.bicone F).toCocone
      isColimit := biproduct.isColimit F }

Biproduct Implies Coproduct

Informal description

For any category $C$ with zero morphisms and any functor $F : J \to C$, if $F$ has a biproduct, then $F$ also has a coproduct.

CategoryTheory.Limits.HasBiproductsOfShape structure

Full source

/-- `C` has biproducts of shape `J` if we have
a limit and a colimit, with the same cone points,
of every function `F : J → C`. -/
class HasBiproductsOfShape : Prop where
  has_biproduct : ∀ F : J → C, HasBiproduct F

Biproducts in a category of shape $ J $

Informal description

A category $ C $ has biproducts of shape $ J $ if for every functor $ F : J \to C $, there exists an object $ X $ in $ C $ that is simultaneously a limit and a colimit of $ F $, with the same cone and cocone structures. This means $ X $ serves as both the product and coproduct of the family $ F $, with the additional property that the canonical morphisms satisfy the biproduct identities.

CategoryTheory.Limits.HasFiniteBiproducts structure

Full source

/-- `HasFiniteBiproducts C` represents a choice of biproduct for every family of objects in `C`
indexed by a finite type. -/
class HasFiniteBiproducts : Prop where
  out : ∀ n, HasBiproductsOfShape (Fin n) C

Category with finite biproducts

Informal description

The structure `HasFiniteBiproducts C` represents a category $ C $ equipped with a choice of biproduct for every finite family of objects in $ C $. A biproduct is both a product and a coproduct in a compatible way, meaning it simultaneously satisfies the universal properties of both limits and colimits for the given family of objects.

CategoryTheory.Limits.hasBiproductsOfShape_of_equiv theorem

{K : Type w'} [HasBiproductsOfShape K C] (e : J ≃ K) : HasBiproductsOfShape J C

Full source

theorem hasBiproductsOfShape_of_equiv {K : Type w'} [HasBiproductsOfShape K C] (e : J ≃ K) :
    HasBiproductsOfShape J C :=
  ⟨fun F =>
    let ⟨⟨h⟩⟩ := HasBiproductsOfShape.has_biproduct (F ∘ e.symm)
    let ⟨c, hc⟩ := h
    HasBiproduct.mk <| by
      simpa only [Function.comp_def, e.symm_apply_apply] using
        LimitBicone.mk (c.whisker e) ((c.whiskerIsBilimitIff _).2 hc)⟩

Preservation of biproducts under equivalence of indexing types

Informal description

Let $C$ be a category with biproducts of shape $K$, and let $e : J \simeq K$ be an equivalence between indexing types $J$ and $K$. Then $C$ also has biproducts of shape $J$.

CategoryTheory.Limits.hasBiproductsOfShape_finite instance

[HasFiniteBiproducts C] [Finite J] : HasBiproductsOfShape J C

Full source

instance (priority := 100) hasBiproductsOfShape_finite [HasFiniteBiproducts C] [Finite J] :
    HasBiproductsOfShape J C := by
  rcases Finite.exists_equiv_fin J with ⟨n, ⟨e⟩⟩
  haveI : HasBiproductsOfShape (Fin n) C := HasFiniteBiproducts.out n
  exact hasBiproductsOfShape_of_equiv C e

Finite Biproducts in Categories with Finite Biproducts

Informal description

For any category $C$ with finite biproducts and any finite indexing type $J$, $C$ has biproducts of shape $J$. This means that for every functor $F : J \to C$, there exists an object in $C$ that is simultaneously a product and coproduct of the family $F$.

CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteBiproducts instance

[HasFiniteBiproducts C] : HasFiniteProducts C

Full source

instance (priority := 100) hasFiniteProducts_of_hasFiniteBiproducts [HasFiniteBiproducts C] :
    HasFiniteProducts C where
  out _ := ⟨fun _ => hasLimit_of_iso Discrete.natIsoFunctor.symm⟩

Finite Biproducts Imply Finite Products

Informal description

Every category with finite biproducts also has finite products.

CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts instance

[HasFiniteBiproducts C] : HasFiniteCoproducts C

Full source

instance (priority := 100) hasFiniteCoproducts_of_hasFiniteBiproducts [HasFiniteBiproducts C] :
    HasFiniteCoproducts C where
  out _ := ⟨fun _ => hasColimit_of_iso Discrete.natIsoFunctor⟩

Finite Biproducts Imply Finite Coproducts

Informal description

Every category with finite biproducts also has finite coproducts.

CategoryTheory.Limits.hasProductsOfShape_of_hasBiproductsOfShape instance

[HasBiproductsOfShape J C] : HasProductsOfShape J C

Full source

instance (priority := 100) hasProductsOfShape_of_hasBiproductsOfShape [HasBiproductsOfShape J C] :
    HasProductsOfShape J C where
  has_limit _ := hasLimit_of_iso Discrete.natIsoFunctor.symm

Biproducts Imply Products in a Category

Informal description

For any category $\mathcal{C}$ with biproducts of shape $J$, $\mathcal{C}$ also has products of shape $J$.

CategoryTheory.Limits.hasCoproductsOfShape_of_hasBiproductsOfShape instance

[HasBiproductsOfShape J C] : HasCoproductsOfShape J C

Full source

instance (priority := 100) hasCoproductsOfShape_of_hasBiproductsOfShape [HasBiproductsOfShape J C] :
    HasCoproductsOfShape J C where
  has_colimit _ := hasColimit_of_iso Discrete.natIsoFunctor

Biproducts Imply Coproducts

Informal description

For any category $C$ with biproducts of shape $J$, $C$ also has coproducts of shape $J$.

CategoryTheory.Limits.biproductIso definition

(F : J → C) [HasBiproduct F] : Limits.piObj F ≅ Limits.sigmaObj F

Full source

/-- The isomorphism between the specified limit and the specified colimit for
a functor with a bilimit. -/
def biproductIso (F : J → C) [HasBiproduct F] : Limits.piObjLimits.piObj F ≅ Limits.sigmaObj F :=
  (IsLimit.conePointUniqueUpToIso (limit.isLimit _) (biproduct.isLimit F)).trans <|
    IsColimit.coconePointUniqueUpToIso (biproduct.isColimit F) (colimit.isColimit _)

Isomorphism between product and coproduct in a biproduct

Informal description

Given a functor $ F : J \to C $ in a category $ C $ with zero morphisms and assuming the existence of a biproduct for $ F $, the isomorphism `biproductIso F` provides a canonical isomorphism between the product $\prod_{j \in J} F_j$ and the coproduct $\coprod_{j \in J} F_j$ of the family $ F $. This isomorphism witnesses the fact that the biproduct simultaneously serves as both the limit and colimit of $ F $.

CategoryTheory.Limits.biproduct abbrev

(f : J → C) [HasBiproduct f] : C

Full source

/-- `biproduct f` computes the biproduct of a family of elements `f`. (It is defined as an
   abbreviation for `limit (Discrete.functor f)`, so for most facts about `biproduct f`, you will
   just use general facts about limits and colimits.) -/
abbrev biproduct (f : J → C) [HasBiproduct f] : C :=
  (biproduct.bicone f).pt

Biproduct of a family of objects

Informal description

Given a family of objects $f : J \to C$ in a category $C$ with zero morphisms, and assuming the existence of a biproduct for $f$, the term $\bigoplus f$ denotes the biproduct object in $C$. This object serves simultaneously as both the product and coproduct of the family $f$, equipped with projection and injection morphisms satisfying the biproduct conditions.

CategoryTheory.Limits.term⨁_ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc biproduct]
notation "⨁ " f:20 => biproduct f

Indexed biproduct notation

Informal description

The notation `⨁ f` represents the biproduct of a family of objects `f` in a category, which is both the categorical product and coproduct when they exist and coincide.

CategoryTheory.Limits.biproduct.π abbrev

(f : J → C) [HasBiproduct f] (b : J) : ⨁ f ⟶ f b

Full source

/-- The projection onto a summand of a biproduct. -/
abbrev biproduct.π (f : J → C) [HasBiproduct f] (b : J) : ⨁ f⨁ f ⟶ f b :=
  (biproduct.bicone f).π b

Projection from Biproduct to Component

Informal description

Given a family of objects $f : J \to C$ in a category $C$ with zero morphisms and biproducts, and an index $b \in J$, the morphism $\pi_b : \bigoplus f \to f(b)$ is the projection from the biproduct to its $b$-th component.

CategoryTheory.Limits.biproduct.bicone_π theorem

(f : J → C) [HasBiproduct f] (b : J) : (biproduct.bicone f).π b = biproduct.π f b

Full source

@[simp]
theorem biproduct.bicone_π (f : J → C) [HasBiproduct f] (b : J) :
    (biproduct.bicone f).π b = biproduct.π f b := rfl

Equality of Biproduct Bicone Projection and Biproduct Projection

Informal description

For a family of objects $f : J \to C$ in a category $C$ with zero morphisms and a biproduct, and for any index $b \in J$, the projection morphism $\pi_b$ from the biproduct bicone of $f$ to $f(b)$ is equal to the biproduct projection morphism $\pi_b : \bigoplus f \to f(b)$.

CategoryTheory.Limits.biproduct.ι abbrev

(f : J → C) [HasBiproduct f] (b : J) : f b ⟶ ⨁ f

Full source

/-- The inclusion into a summand of a biproduct. -/
abbrev biproduct.ι (f : J → C) [HasBiproduct f] (b : J) : f b ⟶ ⨁ f :=
  (biproduct.bicone f).ι b

Inclusion morphism into biproduct

Informal description

For a family of objects $f : J \to C$ in a category $C$ with zero morphisms and a biproduct $\bigoplus f$, the morphism $\iota_b : f(b) \to \bigoplus f$ is the inclusion of the $b$-th summand into the biproduct, for each $b \in J$.

CategoryTheory.Limits.biproduct.bicone_ι theorem

(f : J → C) [HasBiproduct f] (b : J) : (biproduct.bicone f).ι b = biproduct.ι f b

Full source

@[simp]
theorem biproduct.bicone_ι (f : J → C) [HasBiproduct f] (b : J) :
    (biproduct.bicone f).ι b = biproduct.ι f b := rfl

Equality of Bicone Inclusion and Canonical Biproduct Inclusion

Informal description

For a family of objects $f : J \to C$ in a category $C$ with zero morphisms and a biproduct $\bigoplus f$, the inclusion morphism $\iota_b$ in the bicone structure of the biproduct is equal to the canonical inclusion morphism $\iota_b : f(b) \to \bigoplus f$ for each $b \in J$.

CategoryTheory.Limits.biproduct.ι_π theorem

 [DecidableEq J] (f : J → C) [HasBiproduct f] (j j' : J) :
  biproduct.ι f j ≫ biproduct.π f j' = if h : j = j' then eqToHom (congr_arg f h) else 0

Full source

/-- Note that as this lemma has an `if` in the statement, we include a `DecidableEq` argument.
This means you may not be able to `simp` using this lemma unless you `open scoped Classical`. -/
@[reassoc]
theorem biproduct.ι_π [DecidableEq J] (f : J → C) [HasBiproduct f] (j j' : J) :
    biproduct.ιbiproduct.ι f j ≫ biproduct.π f j' = if h : j = j' then eqToHom (congr_arg f h) else 0 := by
  convert (biproduct.bicone f).ι_π j j'

Composition of Inclusion and Projection in Biproduct

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects in $C$. For any indices $j, j' \in J$, the composition of the inclusion morphism $\iota_j : f(j) \to \bigoplus f$ and the projection morphism $\pi_{j'} : \bigoplus f \to f(j')$ satisfies: \[ \iota_j \circ \pi_{j'} = \begin{cases} \mathrm{id}_{f(j)} & \text{if } j = j', \\ 0 & \text{otherwise.} \end{cases} \]

CategoryTheory.Limits.biproduct.ι_π_self theorem

(f : J → C) [HasBiproduct f] (j : J) : biproduct.ι f j ≫ biproduct.π f j = 𝟙 _

Full source

@[reassoc] -- Porting note: both versions proven by simp
theorem biproduct.ι_π_self (f : J → C) [HasBiproduct f] (j : J) :
    biproduct.ιbiproduct.ι f j ≫ biproduct.π f j = 𝟙 _ := by simp [biproduct.ι_π]

Identity Property of Biproduct Components: $\iota_j \circ \pi_j = \text{id}_{f(j)}$

Informal description

For any family of objects $f : J \to C$ in a category $C$ with zero morphisms and biproducts, and for any index $j \in J$, the composition of the $j$-th inclusion morphism $\iota_j : f(j) \to \bigoplus f$ and the $j$-th projection morphism $\pi_j : \bigoplus f \to f(j)$ is equal to the identity morphism on $f(j)$, i.e., $\iota_j \circ \pi_j = \text{id}_{f(j)}$.

CategoryTheory.Limits.biproduct.ι_π_ne theorem

(f : J → C) [HasBiproduct f] {j j' : J} (h : j ≠ j') : biproduct.ι f j ≫ biproduct.π f j' = 0

Full source

@[reassoc (attr := simp)]
theorem biproduct.ι_π_ne (f : J → C) [HasBiproduct f] {j j' : J} (h : j ≠ j') :
    biproduct.ιbiproduct.ι f j ≫ biproduct.π f j' = 0 := by simp [biproduct.ι_π, h]

Vanishing of Biproduct Component Compositions for Distinct Indices: $\iota_j \circ \pi_{j'} = 0$ when $j \ne j'$

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects in $C$. For any distinct indices $j \ne j'$ in $J$, the composition of the inclusion morphism $\iota_j : f(j) \to \bigoplus f$ and the projection morphism $\pi_{j'} : \bigoplus f \to f(j')$ is the zero morphism, i.e., $\iota_j \circ \pi_{j'} = 0$.

CategoryTheory.Limits.biproduct.eqToHom_comp_ι theorem

(f : J → C) [HasBiproduct f] {j j' : J} (w : j = j') : eqToHom (by simp [w]) ≫ biproduct.ι f j' = biproduct.ι f j

Full source

@[reassoc (attr := simp, nolint simpNF)]
theorem biproduct.eqToHom_comp_ι (f : J → C) [HasBiproduct f] {j j' : J} (w : j = j') :
    eqToHomeqToHom (by simp [w]) ≫ biproduct.ι f j' = biproduct.ι f j := by
  cases w
  simp

Compatibility of Inclusion Morphism with Object Equality in Biproducts

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects in $\mathcal{C}$. For any indices $j, j' \in J$ with an equality $w : j = j'$, the composition of the morphism $\text{eqToHom}(w) : f(j) \to f(j')$ (induced by the equality $w$) with the inclusion morphism $\iota_{j'} : f(j') \to \bigoplus f$ equals the inclusion morphism $\iota_j : f(j) \to \bigoplus f$.

CategoryTheory.Limits.biproduct.π_comp_eqToHom theorem

(f : J → C) [HasBiproduct f] {j j' : J} (w : j = j') : biproduct.π f j ≫ eqToHom (by simp [w]) = biproduct.π f j'

Full source

@[reassoc (attr := simp, nolint simpNF)]
theorem biproduct.π_comp_eqToHom (f : J → C) [HasBiproduct f] {j j' : J} (w : j = j') :
    biproduct.πbiproduct.π f j ≫ eqToHom (by simp [w]) = biproduct.π f j' := by
  cases w
  simp

Compatibility of Biproduct Projections with Equality Morphisms

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects in $\mathcal{C}$. For any indices $j, j' \in J$ with $j = j'$ (via equality $w$), the composition of the projection $\pi_j : \bigoplus f \to f(j)$ with the morphism $\text{eqToHom}$ (induced by $w$) equals the projection $\pi_{j'} : \bigoplus f \to f(j')$.

CategoryTheory.Limits.biproduct.lift abbrev

{f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, P ⟶ f b) : P ⟶ ⨁ f

Full source

/-- Given a collection of maps into the summands, we obtain a map into the biproduct. -/
abbrev biproduct.lift {f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, P ⟶ f b) : P ⟶ ⨁ f :=
  (biproduct.isLimit f).lift (Fan.mk P p)

Universal Property of Biproduct: Lifting Morphisms to Biproduct

Informal description

Given a category $\mathcal{C}$ with zero morphisms and a family of objects $f : J \to \mathcal{C}$ that has a biproduct, for any object $P$ in $\mathcal{C}$ and a family of morphisms $p_b : P \to f(b)$ for each $b \in J$, there exists a unique morphism $\text{biproduct.lift}\, p : P \to \bigoplus f$ such that for each $j \in J$, the composition $\text{biproduct.lift}\, p \circ \pi_j$ equals $p_j$, where $\pi_j$ is the projection from the biproduct to $f(j)$.

CategoryTheory.Limits.biproduct.desc abbrev

{f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, f b ⟶ P) : ⨁ f ⟶ P

Full source

/-- Given a collection of maps out of the summands, we obtain a map out of the biproduct. -/
abbrev biproduct.desc {f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, f b ⟶ P) : ⨁ f⨁ f ⟶ P :=
  (biproduct.isColimit f).desc (Cofan.mk P p)

Universal Morphism from Biproduct via Descending Morphisms

Informal description

Given a family of objects $f : J \to C$ in a category $C$ with zero morphisms and biproducts, and an object $P$ in $C$, for any collection of morphisms $p_b : f(b) \to P$ for each $b \in J$, there exists a unique morphism $\bigoplus f \to P$ induced by the $p_b$ via the universal property of the biproduct as a colimit.

CategoryTheory.Limits.biproduct.lift_π theorem

{f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, P ⟶ f b) (j : J) : biproduct.lift p ≫ biproduct.π f j = p j

Full source

@[reassoc (attr := simp)]
theorem biproduct.lift_π {f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, P ⟶ f b) (j : J) :
    biproduct.liftbiproduct.lift p ≫ biproduct.π f j = p j := (biproduct.isLimit f).fac _ ⟨j⟩

Commutativity of Biproduct Lift with Projections: $\text{lift}\, p \circ \pi_j = p_j$

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects with a biproduct $\bigoplus f$. For any object $P$ in $\mathcal{C}$ and any collection of morphisms $p_b : P \to f(b)$ for each $b \in J$, the composition of the lifted morphism $\text{biproduct.lift}\, p : P \to \bigoplus f$ with the projection $\pi_j : \bigoplus f \to f(j)$ equals $p_j$ for each $j \in J$. That is, $\text{biproduct.lift}\, p \circ \pi_j = p_j$.

CategoryTheory.Limits.biproduct.ι_desc theorem

{f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, f b ⟶ P) (j : J) : biproduct.ι f j ≫ biproduct.desc p = p j

Full source

@[reassoc (attr := simp)]
theorem biproduct.ι_desc {f : J → C} [HasBiproduct f] {P : C} (p : ∀ b, f b ⟶ P) (j : J) :
    biproduct.ιbiproduct.ι f j ≫ biproduct.desc p = p j := (biproduct.isColimit f).fac _ ⟨j⟩

Commutativity of Biproduct Inclusion with Descending Morphism: $\iota_j \circ \text{desc } p = p_j$

Informal description

For a family of objects $f : J \to C$ in a category $C$ with zero morphisms and biproducts, given an object $P$ in $C$ and a collection of morphisms $p_b : f(b) \to P$ for each $b \in J$, the composition of the inclusion morphism $\iota_j : f(j) \to \bigoplus f$ with the induced morphism $\text{desc } p : \bigoplus f \to P$ equals $p_j$ for each $j \in J$. That is, $\iota_j \circ (\text{desc } p) = p_j$.

CategoryTheory.Limits.biproduct.map abbrev

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) : ⨁ f ⟶ ⨁ g

Full source

/-- Given a collection of maps between corresponding summands of a pair of biproducts
indexed by the same type, we obtain a map between the biproducts. -/
abbrev biproduct.map {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) :
    ⨁ f⨁ f ⟶ ⨁ g :=
  IsLimit.map (biproduct.bicone f).toCone (biproduct.isLimit g)
    (Discrete.natTrans (fun j => p j.as))

Morphism between biproducts induced by component-wise maps

Informal description

Given two families of objects $f, g : J \to C$ in a category $C$ with zero morphisms, and assuming that both families have biproducts, the morphism $\bigoplus f \to \bigoplus g$ is constructed from a collection of morphisms $p_b : f b \to g b$ for each $b \in J$. This morphism is denoted as $\text{biproduct.map } p$ and is the unique morphism from $\bigoplus f$ to $\bigoplus g$ that commutes with the biproduct structure.

CategoryTheory.Limits.biproduct.map' abbrev

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) : ⨁ f ⟶ ⨁ g

Full source

/-- An alternative to `biproduct.map` constructed via colimits.
This construction only exists in order to show it is equal to `biproduct.map`. -/
abbrev biproduct.map' {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) :
    ⨁ f⨁ f ⟶ ⨁ g :=
  IsColimit.map (biproduct.isColimit f) (biproduct.bicone g).toCocone
    (Discrete.natTrans fun j => p j.as)

Colimit-Constructed Biproduct Map

Informal description

Given two families of objects $f, g : J \to C$ in a category $C$ with zero morphisms, and assuming the existence of biproducts for both $f$ and $g$, the morphism $\bigoplus f \to \bigoplus g$ is constructed from a family of morphisms $p : \forall b, f b \to g b$. This morphism is an alternative construction to `biproduct.map`, built using colimits, and is shown to be equal to `biproduct.map`.

CategoryTheory.Limits.biproduct.hom_ext theorem

 {f : J → C} [HasBiproduct f] {Z : C} (g h : Z ⟶ ⨁ f) (w : ∀ j, g ≫ biproduct.π f j = h ≫ biproduct.π f j) : g = h

Full source

@[ext 1001]
theorem biproduct.hom_ext {f : J → C} [HasBiproduct f] {Z : C} (g h : Z ⟶ ⨁ f)
    (w : ∀ j, g ≫ biproduct.π f j = h ≫ biproduct.π f j) : g = h :=
  (biproduct.isLimit f).hom_ext fun j => w j.as

Uniqueness of Morphisms into Biproduct via Projections

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects in $C$ with an existing biproduct $\bigoplus f$. For any object $Z$ in $C$ and any pair of morphisms $g, h : Z \to \bigoplus f$, if for every index $j \in J$ the compositions $g \circ \pi_j$ and $h \circ \pi_j$ are equal (where $\pi_j$ is the projection from the biproduct to $f(j)$), then $g = h$.

CategoryTheory.Limits.biproduct.hom_ext' theorem

 {f : J → C} [HasBiproduct f] {Z : C} (g h : ⨁ f ⟶ Z) (w : ∀ j, biproduct.ι f j ≫ g = biproduct.ι f j ≫ h) : g = h

Full source

@[ext]
theorem biproduct.hom_ext' {f : J → C} [HasBiproduct f] {Z : C} (g h : ⨁ f⨁ f ⟶ Z)
    (w : ∀ j, biproduct.ιbiproduct.ι f j ≫ g = biproduct.ιbiproduct.ι f j ≫ h) : g = h :=
  (biproduct.isColimit f).hom_ext fun j => w j.as

Uniqueness of Morphisms from Biproduct via Inclusions

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects in $C$ with biproduct $\bigoplus f$. For any object $Z$ in $C$ and any two morphisms $g, h : \bigoplus f \to Z$, if for every $j \in J$ the compositions $\iota_j \circ g$ and $\iota_j \circ h$ are equal (where $\iota_j : f(j) \to \bigoplus f$ is the inclusion morphism), then $g = h$.

CategoryTheory.Limits.biproduct.isoProduct definition

(f : J → C) [HasBiproduct f] : ⨁ f ≅ ∏ᶜ f

Full source

/-- The canonical isomorphism between the chosen biproduct and the chosen product. -/
def biproduct.isoProduct (f : J → C) [HasBiproduct f] : ⨁ f⨁ f ≅ ∏ᶜ f :=
  IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (limit.isLimit _)

Canonical isomorphism between biproduct and product

Informal description

Given a family of objects $ f : J \to C $ in a category $ C $ with zero morphisms and assuming the existence of a biproduct for $ f $, the canonical isomorphism $ \bigoplus f \cong \prod f $ identifies the biproduct object $ \bigoplus f $ with the product object $ \prod f $.

CategoryTheory.Limits.biproduct.isoProduct_hom theorem

{f : J → C} [HasBiproduct f] : (biproduct.isoProduct f).hom = Pi.lift (biproduct.π f)

Full source

@[simp]
theorem biproduct.isoProduct_hom {f : J → C} [HasBiproduct f] :
    (biproduct.isoProduct f).hom = Pi.lift (biproduct.π f) :=
  limit.hom_ext fun j => by simp [biproduct.isoProduct]

Homomorphism part of biproduct-product isomorphism equals product lift of projections

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects with biproduct $\bigoplus f$. The homomorphism part of the canonical isomorphism $\bigoplus f \cong \prod f$ is equal to the product lift of the biproduct projections $\pi_j : \bigoplus f \to f(j)$. In symbols, if $\varphi : \bigoplus f \to \prod f$ denotes the isomorphism, then $\varphi = \Pi.\mathrm{lift}(\pi)$ where $\pi$ is the family of projections $\{\pi_j\}_{j \in J}$.

CategoryTheory.Limits.biproduct.isoProduct_inv theorem

{f : J → C} [HasBiproduct f] : (biproduct.isoProduct f).inv = biproduct.lift (Pi.π f)

Full source

@[simp]
theorem biproduct.isoProduct_inv {f : J → C} [HasBiproduct f] :
    (biproduct.isoProduct f).inv = biproduct.lift (Pi.π f) :=
  biproduct.hom_ext _ _ fun j => by simp [Iso.inv_comp_eq]

Inverse of Biproduct-Product Isomorphism via Lifting Projections

Informal description

For a family of objects $f : J \to C$ in a category $C$ with zero morphisms and a biproduct $\bigoplus f$, the inverse of the canonical isomorphism $\bigoplus f \cong \prod f$ is equal to the biproduct lift of the product projections $\pi_j : \prod f \to f(j)$. That is, $( \bigoplus f \cong \prod f )^{-1} = \text{biproduct.lift}\, \pi$.

CategoryTheory.Limits.biproduct.isoCoproduct definition

(f : J → C) [HasBiproduct f] : ⨁ f ≅ ∐ f

Full source

/-- The canonical isomorphism between the chosen biproduct and the chosen coproduct. -/
def biproduct.isoCoproduct (f : J → C) [HasBiproduct f] : ⨁ f⨁ f ≅ ∐ f :=
  IsColimit.coconePointUniqueUpToIso (biproduct.isColimit f) (colimit.isColimit _)

Isomorphism between biproduct and coproduct

Informal description

Given a family of objects $ f : J \to C $ in a category $ C $ with zero morphisms and assuming the existence of a biproduct for $ f $, the canonical isomorphism $ \bigoplus f \cong \coprod f $ between the biproduct and the coproduct of $ f $ is established. This isomorphism is constructed using the universal properties of the biproduct and coproduct, ensuring compatibility with the category's structure.

CategoryTheory.Limits.biproduct.isoCoproduct_inv theorem

{f : J → C} [HasBiproduct f] : (biproduct.isoCoproduct f).inv = Sigma.desc (biproduct.ι f)

Full source

@[simp]
theorem biproduct.isoCoproduct_inv {f : J → C} [HasBiproduct f] :
    (biproduct.isoCoproduct f).inv = Sigma.desc (biproduct.ι f) :=
  colimit.hom_ext fun j => by simp [biproduct.isoCoproduct]

Inverse of Biproduct-Coproduct Isomorphism via Universal Property

Informal description

For a family of objects $f : J \to C$ in a category $C$ with zero morphisms and a biproduct $\bigoplus f$, the inverse of the isomorphism $\bigoplus f \cong \coprod f$ between the biproduct and the coproduct is given by the universal morphism $\Sigma.\mathrm{desc}$ applied to the inclusion morphisms $\iota_j : f(j) \to \bigoplus f$ for each $j \in J$.

CategoryTheory.Limits.biproduct.isoCoproduct_hom theorem

{f : J → C} [HasBiproduct f] : (biproduct.isoCoproduct f).hom = biproduct.desc (Sigma.ι f)

Full source

@[simp]
theorem biproduct.isoCoproduct_hom {f : J → C} [HasBiproduct f] :
    (biproduct.isoCoproduct f).hom = biproduct.desc (Sigma.ι f) :=
  biproduct.hom_ext' _ _ fun j => by simp [← Iso.eq_comp_inv]

Forward Isomorphism Component: $\text{biproduct.isoCoproduct}.hom = \text{biproduct.desc}(\Sigma.\iota)$

Informal description

For a family of objects $f : J \to C$ in a category $C$ with zero morphisms and a biproduct $\bigoplus f$, the forward morphism of the isomorphism $\bigoplus f \cong \coprod f$ is equal to the universal morphism $\text{biproduct.desc}$ applied to the coprojection morphisms $\Sigma.\iota_j : f(j) \to \coprod f$ for each $j \in J$.

CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim definition

[HasBiproductsOfShape J C] : colim (J := Discrete J) (C := C) ≅ lim

Full source

/-- If a category has biproducts of a shape `J`, its `colim` and `lim` functor on diagrams over `J`
are isomorphic. -/
@[simps!]
def HasBiproductsOfShape.colimIsoLim [HasBiproductsOfShape J C] :
    colimcolim (J := Discrete J) (C := C) ≅ lim :=
  NatIso.ofComponents (fun F => (Sigma.isoColimit F).symm ≪≫
      (biproduct.isoCoproduct _).symm ≪≫ biproduct.isoProduct _ ≪≫ Pi.isoLimit F)
    fun η => colimit.hom_ext fun ⟨i⟩ => limit.hom_ext fun ⟨j⟩ => by
      classical
      by_cases h : i = j <;>
       simp_all [h, Sigma.isoColimit, Pi.isoLimit, biproduct.ι_π, biproduct.ι_π_assoc]

Isomorphism between colimit and limit functors for biproducts

Informal description

For a category $\mathcal{C}$ with biproducts of shape $J$, the colimit and limit functors on diagrams over $J$ are isomorphic. Specifically, there is a natural isomorphism between the colimit functor $\text{colim}$ and the limit functor $\text{lim}$ when both are restricted to the discrete category on $J$.

CategoryTheory.Limits.biproduct.map_eq_map' theorem

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) : biproduct.map p = biproduct.map' p

Full source

theorem biproduct.map_eq_map' {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) :
    biproduct.map p = biproduct.map' p := by
  classical
  ext
  dsimp
  simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
    Category.assoc, ← Bicone.toCone_π_app_mk, ← biproduct.bicone_π, ← Bicone.toCocone_ι_app_mk,
    ← biproduct.bicone_ι]
  dsimp
  rw [biproduct.ι_π_assoc, biproduct.ι_π]
  split_ifs with h
  · subst h; simp
  · simp

Equality of Biproduct Maps via Limit and Colimit Constructions

Informal description

For any two families of objects $f, g : J \to C$ in a category $C$ with zero morphisms and biproducts, and for any family of morphisms $p : \forall b, f b \to g b$, the morphism $\text{biproduct.map } p$ constructed via the limit structure is equal to the morphism $\text{biproduct.map' } p$ constructed via the colimit structure.

CategoryTheory.Limits.biproduct.map_π theorem

 {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) (j : J) :
  biproduct.map p ≫ biproduct.π g j = biproduct.π f j ≫ p j

Full source

@[reassoc (attr := simp)]
theorem biproduct.map_π {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    (j : J) : biproduct.mapbiproduct.map p ≫ biproduct.π g j = biproduct.πbiproduct.π f j ≫ p j :=
  Limits.IsLimit.map_π _ _ _ (Discrete.mk j)

Commutativity of Biproduct Map with Projections

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f, g : J \to C$ be two families of objects in $C$ that have biproducts. For any collection of morphisms $p_j : f(j) \to g(j)$ for each $j \in J$, the composition of the induced morphism $\bigoplus f \to \bigoplus g$ with the projection $\pi_j : \bigoplus g \to g(j)$ equals the composition of the projection $\pi_j : \bigoplus f \to f(j)$ with $p_j$. In symbols: \[ \text{biproduct.map } p \circ \pi_j = \pi_j \circ p_j \]

CategoryTheory.Limits.biproduct.ι_map theorem

 {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) (j : J) :
  biproduct.ι f j ≫ biproduct.map p = p j ≫ biproduct.ι g j

Full source

@[reassoc (attr := simp)]
theorem biproduct.ι_map {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    (j : J) : biproduct.ιbiproduct.ι f j ≫ biproduct.map p = p j ≫ biproduct.ι g j := by
  rw [biproduct.map_eq_map']
  apply
    Limits.IsColimit.ι_map (biproduct.isColimit f) (biproduct.bicone g).toCocone
    (Discrete.natTrans fun j => p j.as) (Discrete.mk j)

Commutativity of Biproduct Map with Inclusions

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f, g : J \to C$ be two families of objects in $C$ that have biproducts. For any collection of morphisms $p_j : f(j) \to g(j)$ for each $j \in J$, the composition of the inclusion $\iota_j : f(j) \to \bigoplus f$ with the induced morphism $\bigoplus f \to \bigoplus g$ equals the composition of $p_j$ with the inclusion $\iota_j : g(j) \to \bigoplus g$. In symbols: \[ \iota_j \circ \text{biproduct.map } p = p_j \circ \iota_j \]

CategoryTheory.Limits.biproduct.map_desc theorem

 {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) {P : C} (k : ∀ j, g j ⟶ P) :
  biproduct.map p ≫ biproduct.desc k = biproduct.desc fun j => p j ≫ k j

Full source

@[reassoc (attr := simp)]
theorem biproduct.map_desc {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    {P : C} (k : ∀ j, g j ⟶ P) :
    biproduct.mapbiproduct.map p ≫ biproduct.desc k = biproduct.desc fun j => p j ≫ k j := by
  ext; simp

Commutativity of Biproduct Map with Descending Morphism: $\text{map } p \circ \text{desc } k = \text{desc } (p_j \circ k_j)$

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f, g : J \to C$ be two families of objects in $C$ that have biproducts. For any collection of morphisms $p_j : f(j) \to g(j)$ for each $j \in J$ and any object $P$ in $C$ with morphisms $k_j : g(j) \to P$ for each $j \in J$, the composition of the induced morphism $\bigoplus f \to \bigoplus g$ with the universal morphism $\bigoplus g \to P$ equals the universal morphism $\bigoplus f \to P$ induced by the compositions $p_j \circ k_j$. In symbols: \[ \text{biproduct.map } p \circ \text{biproduct.desc } k = \text{biproduct.desc } (p_j \circ k_j) \]

CategoryTheory.Limits.biproduct.lift_map theorem

 {f g : J → C} [HasBiproduct f] [HasBiproduct g] {P : C} (k : ∀ j, P ⟶ f j) (p : ∀ j, f j ⟶ g j) :
  biproduct.lift k ≫ biproduct.map p = biproduct.lift fun j => k j ≫ p j

Full source

@[reassoc (attr := simp)]
theorem biproduct.lift_map {f g : J → C} [HasBiproduct f] [HasBiproduct g] {P : C}
    (k : ∀ j, P ⟶ f j) (p : ∀ j, f j ⟶ g j) :
    biproduct.liftbiproduct.lift k ≫ biproduct.map p = biproduct.lift fun j => k j ≫ p j := by
  ext; simp

Commutativity of Biproduct Lift with Map: $\text{lift}\, k \circ \text{map}\, p = \text{lift}\, (k_j \circ p_j)$

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f, g : J \to C$ be two families of objects in $C$ that have biproducts. For any object $P$ in $C$, given a family of morphisms $k_j : P \to f(j)$ for each $j \in J$ and a family of morphisms $p_j : f(j) \to g(j)$ for each $j \in J$, the composition of the lifted morphism $\text{biproduct.lift}\, k : P \to \bigoplus f$ with the induced morphism $\text{biproduct.map}\, p : \bigoplus f \to \bigoplus g$ equals the lifted morphism $\text{biproduct.lift}\, (k_j \circ p_j) : P \to \bigoplus g$. In symbols: \[ \text{biproduct.lift}\, k \circ \text{biproduct.map}\, p = \text{biproduct.lift}\, (k_j \circ p_j) \]

CategoryTheory.Limits.biproduct.mapIso definition

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ≅ g b) : ⨁ f ≅ ⨁ g

Full source

/-- Given a collection of isomorphisms between corresponding summands of a pair of biproducts
indexed by the same type, we obtain an isomorphism between the biproducts. -/
@[simps]
def biproduct.mapIso {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ≅ g b) :
    ⨁ f⨁ f ≅ ⨁ g where
  hom := biproduct.map fun b => (p b).hom
  inv := biproduct.map fun b => (p b).inv

Isomorphism between biproducts induced by component-wise isomorphisms

Informal description

Given two families of objects $f, g : J \to C$ in a category $C$ with zero morphisms, and assuming that both families have biproducts, the isomorphism $\bigoplus f \cong \bigoplus g$ is constructed from a collection of isomorphisms $p_b : f b \cong g b$ for each $b \in J$. The isomorphism is defined by taking the biproduct of the homomorphisms $(p_b).\text{hom}$ as the forward direction and the biproduct of the inverse homomorphisms $(p_b).\text{inv}$ as the inverse direction.

CategoryTheory.Limits.biproduct.map_epi instance

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) [∀ j, Epi (p j)] : Epi (biproduct.map p)

Full source

instance biproduct.map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    [∀ j, Epi (p j)] : Epi (biproduct.map p) := by
  classical
  have : biproduct.map p =
      (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
    ext
    simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
      ι_colimMap_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app, colimit.ι_desc_assoc,
      Cofan.mk_pt, Cofan.mk_ι_app, ι_π, ι_π_assoc]
    split
    all_goals simp_all
  rw [this]
  infer_instance

Epimorphism Property of Biproduct Maps with Epimorphic Components

Informal description

For any two families of objects $f, g : J \to C$ in a category $C$ with zero morphisms and biproducts, if each component morphism $p_j : f(j) \to g(j)$ is an epimorphism, then the induced morphism $\bigoplus f \to \bigoplus g$ is also an epimorphism.

CategoryTheory.Limits.Pi.map_epi instance

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) [∀ j, Epi (p j)] : Epi (Pi.map p)

Full source

instance Pi.map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    [∀ j, Epi (p j)] : Epi (Pi.map p) := by
  rw [show Pi.map p = (biproduct.isoProduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoProduct _).hom by aesop]
  infer_instance

Epimorphisms Induce Epimorphisms on Products

Informal description

For any two families of objects $\{f(j)\}_{j \in J}$ and $\{g(j)\}_{j \in J}$ in a category $\mathcal{C}$ with biproducts, if each morphism $p_j : f(j) \to g(j)$ is an epimorphism, then the induced morphism $\prod_{j \in J} f(j) \to \prod_{j \in J} g(j)$ is also an epimorphism.

CategoryTheory.Limits.biproduct.map_mono instance

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) [∀ j, Mono (p j)] : Mono (biproduct.map p)

Full source

instance biproduct.map_mono {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    [∀ j, Mono (p j)] : Mono (biproduct.map p) := by
  rw [show biproduct.map p = (biproduct.isoProduct _).hom ≫ Pi.map p ≫
    (biproduct.isoProduct _).inv by aesop]
  infer_instance

Monomorphisms Induce Monomorphisms on Biproducts

Informal description

For any two families of objects $\{f(j)\}_{j \in J}$ and $\{g(j)\}_{j \in J}$ in a category $\mathcal{C}$ with biproducts, if each morphism $p_j : f(j) \to g(j)$ is a monomorphism, then the induced morphism $\bigoplus f \to \bigoplus g$ is also a monomorphism.

CategoryTheory.Limits.Sigma.map_mono instance

{f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j) [∀ j, Mono (p j)] : Mono (Sigma.map p)

Full source

instance Sigma.map_mono {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ j, f j ⟶ g j)
    [∀ j, Mono (p j)] : Mono (Sigma.map p) := by
  rw [show Sigma.map p = (biproduct.isoCoproduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoCoproduct _).hom by aesop]
  infer_instance

Monomorphisms Induce Monomorphisms on Coproducts

Informal description

For any two families of objects $\{f(j)\}_{j \in J}$ and $\{g(j)\}_{j \in J}$ in a category $\mathcal{C}$ with biproducts, if each morphism $p_j : f(j) \to g(j)$ is a monomorphism, then the induced morphism $\coprod_{j \in J} f(j) \to \coprod_{j \in J} g(j)$ is also a monomorphism.

CategoryTheory.Limits.biproduct.whiskerEquiv definition

 {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] : ⨁ f ≅ ⨁ g

Full source

/-- Two biproducts which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.

Unfortunately there are two natural ways to define each direction of this isomorphism
(because it is true for both products and coproducts separately).
We give the alternative definitions as lemmas below. -/
@[simps]
def biproduct.whiskerEquiv {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j)
    [HasBiproduct f] [HasBiproduct g] : ⨁ f⨁ f ≅ ⨁ g where
  hom := biproduct.desc fun j => (w j).inv ≫ biproduct.ι g (e j)
  inv := biproduct.desc fun k => eqToHom (by simp) ≫ (w (e.symm k)).hom ≫ biproduct.ι f _

Isomorphism of biproducts under index equivalence and factor isomorphism

Informal description

Given an equivalence $e : J \simeq K$ between indexing types and a family of isomorphisms $w_j : g(e(j)) \cong f(j)$ for each $j \in J$, where $f : J \to C$ and $g : K \to C$ are diagrams in a category $C$ with biproducts, there exists an isomorphism $\bigoplus f \cong \bigoplus g$ between their biproducts. The isomorphism is constructed using the universal properties of the biproducts, with the forward direction given by descending the inverses of $w_j$ composed with the inclusions $\iota_{e(j)}$ of $g$, and the inverse direction similarly constructed using the isomorphisms $w_j$ and the inclusions of $f$.

CategoryTheory.Limits.biproduct.whiskerEquiv_hom_eq_lift theorem

 {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
  (biproduct.whiskerEquiv e w).hom = biproduct.lift fun k => biproduct.π f (e.symm k) ≫ (w _).inv ≫ eqToHom (by simp)

Full source

lemma biproduct.whiskerEquiv_hom_eq_lift {f : J → C} {g : K → C} (e : J ≃ K)
    (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
    (biproduct.whiskerEquiv e w).hom =
      biproduct.lift fun k => biproduct.πbiproduct.π f (e.symm k) ≫ (w _).inv ≫ eqToHom (by simp) := by
  simp only [whiskerEquiv_hom]
  ext k j
  by_cases h : k = e j
  · subst h
    simp
  · simp only [ι_desc_assoc, Category.assoc, ne_eq, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · rintro rfl
      simp at h
    · exact Ne.symm h

Homomorphism of Biproduct Isomorphism Under Index Equivalence is a Lift

Informal description

Let $\mathcal{C}$ be a category with biproducts, and let $f \colon J \to \mathcal{C}$ and $g \colon K \to \mathcal{C}$ be families of objects indexed by types $J$ and $K$, respectively. Given an equivalence $e \colon J \simeq K$ and a family of isomorphisms $w_j \colon g(e(j)) \cong f(j)$ for each $j \in J$, the homomorphism part of the isomorphism $\bigoplus f \cong \bigoplus g$ induced by $e$ and $w$ is equal to the morphism obtained by lifting the family of morphisms $$ \pi_{e^{-1}(k)} \circ w_{e^{-1}(k)}^{-1} \circ \text{eqToHom}(\text{by simp}) \colon \bigoplus f \to g(k) $$ for each $k \in K$, where $\pi_j$ is the projection from $\bigoplus f$ to $f(j)$.

CategoryTheory.Limits.biproduct.whiskerEquiv_inv_eq_lift theorem

 {f : J → C} {g : K → C} (e : J ≃ K) (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
  (biproduct.whiskerEquiv e w).inv = biproduct.lift fun j => biproduct.π g (e j) ≫ (w j).hom

Full source

lemma biproduct.whiskerEquiv_inv_eq_lift {f : J → C} {g : K → C} (e : J ≃ K)
    (w : ∀ j, g (e j) ≅ f j) [HasBiproduct f] [HasBiproduct g] :
    (biproduct.whiskerEquiv e w).inv =
      biproduct.lift fun j => biproduct.πbiproduct.π g (e j) ≫ (w j).hom := by
  simp only [whiskerEquiv_inv]
  ext j k
  by_cases h : k = e j
  · subst h
    simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm,
      Equiv.symm_apply_apply, eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id,
      lift_π, bicone_ι_π_self_assoc]
  · simp only [ι_desc_assoc, Category.assoc, ne_eq, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · exact h
    · rintro rfl
      simp at h

Inverse of Biproduct Isomorphism via Lifting Projections and Isomorphisms

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ and $g : K \to \mathcal{C}$ be families of objects in $\mathcal{C}$ with biproducts $\bigoplus f$ and $\bigoplus g$ respectively. Given an equivalence $e : J \simeq K$ between the indexing sets and a family of isomorphisms $w_j : g(e(j)) \cong f(j)$ for each $j \in J$, the inverse of the isomorphism $\bigoplus f \cong \bigoplus g$ induced by $e$ and $w$ is equal to the morphism $\text{biproduct.lift}\, p$, where $p_j = \pi_{e(j)} \circ w_j.\text{hom}$ for each $j \in J$.

CategoryTheory.Limits.instHasBiproductSigmaFstSndOfBiproduct instance

 {ι} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasBiproduct (g i)] [HasBiproduct fun i => ⨁ g i] :
  HasBiproduct fun p : Σ i, f i => g p.1 p.2

Full source

instance {ι} (f : ι → Type*) (g : (i : ι) → (f i) → C)
    [∀ i, HasBiproduct (g i)] [HasBiproduct fun i => ⨁ g i] :
    HasBiproduct fun p : Σ i, f i => g p.1 p.2 where
  exists_biproduct := Nonempty.intro
    { bicone :=
      { pt := ⨁ fun i => ⨁ g i
        ι := fun X => biproduct.ιbiproduct.ι (g X.1) X.2 ≫ biproduct.ι (fun i => ⨁ g i) X.1
        π := fun X => biproduct.πbiproduct.π (fun i => ⨁ g i) X.1 ≫ biproduct.π (g X.1) X.2
        ι_π := fun ⟨j, x⟩ ⟨j', y⟩ => by
          split_ifs with h
          · obtain ⟨rfl, rfl⟩ := h
            simp
          · simp only [Sigma.mk.inj_iff, not_and] at h
            by_cases w : j = j'
            · cases w
              simp only [heq_eq_eq, forall_true_left] at h
              simp [biproduct.ι_π_ne _ h]
            · simp [biproduct.ι_π_ne_assoc _ w] }
      isBilimit :=
      { isLimit := mkFanLimit _
          (fun s => biproduct.lift fun b => biproduct.lift fun c => s.proj ⟨b, c⟩)
        isColimit := mkCofanColimit _
          (fun s => biproduct.desc fun b => biproduct.desc fun c => s.inj ⟨b, c⟩) } }

Existence of Biproduct for Sigma-Type Indexed Families

Informal description

For any family of types $f : \iota \to \text{Type}$ and a family of objects $g_i : f(i) \to C$ in a category $C$ with zero morphisms, if for each $i \in \iota$ the family $g_i$ has a biproduct and the family $\bigoplus g_i$ also has a biproduct, then the family $(g_{p.1} p.2)_{p \in \Sigma i, f(i)}$ has a biproduct.

CategoryTheory.Limits.biproductBiproductIso definition

 {ι} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasBiproduct (g i)] [HasBiproduct fun i => ⨁ g i] :
  (⨁ fun i => ⨁ g i) ≅ (⨁ fun p : Σ i, f i => g p.1 p.2)

Full source

/-- An iterated biproduct is a biproduct over a sigma type. -/
@[simps]
def biproductBiproductIso {ι} (f : ι → Type*) (g : (i : ι) → (f i) → C)
    [∀ i, HasBiproduct (g i)] [HasBiproduct fun i => ⨁ g i] :
    (⨁ fun i => ⨁ g i) ≅ (⨁ fun p : Σ i, f i => g p.1 p.2) where
  hom := biproduct.lift fun ⟨i, x⟩ => biproduct.π _ i ≫ biproduct.π _ x
  inv := biproduct.lift fun i => biproduct.lift fun x => biproduct.π _ (⟨i, x⟩ : Σ i, f i)

Isomorphism between iterated biproduct and sigma-indexed biproduct

Informal description

Given a family of types $f : \iota \to \text{Type}$ and a family of objects $g_i : f(i) \to C$ in a category $C$ with zero morphisms, if for each $i \in \iota$ the family $g_i$ has a biproduct and the family $\bigoplus g_i$ also has a biproduct, then there is a natural isomorphism between the iterated biproduct $\bigoplus_{i \in \iota} \bigoplus_{x \in f(i)} g_i(x)$ and the biproduct $\bigoplus_{p \in \Sigma i, f(i)} g_{p.1}(p.2)$ indexed by the sigma type. The isomorphism is given by: - The forward map sends a pair $(i, x)$ to the composition of the projection $\pi_i$ from the outer biproduct followed by the projection $\pi_x$ from the inner biproduct. - The inverse map sends an index $i$ to the lift of the family of projections $\pi_{(i,x)}$ for each $x \in f(i)$.

CategoryTheory.Limits.biproduct.fromSubtype definition

: ⨁ Subtype.restrict p f ⟶ ⨁ f

Full source

/-- The canonical morphism from the biproduct over a restricted index type to the biproduct of
the full index type. -/
def biproduct.fromSubtype : ⨁ Subtype.restrict p f⨁ Subtype.restrict p f ⟶ ⨁ f :=
  biproduct.desc fun j => biproduct.ι _ j.val

Inclusion morphism from restricted biproduct to full biproduct

Informal description

Given a family of objects $f : J \to C$ in a category $C$ with zero morphisms and a predicate $p$ on $J$, the morphism $\bigoplus_{j \in p} f(j) \to \bigoplus_{j \in J} f(j)$ is the canonical inclusion from the biproduct over the restricted index type $\{j \in J | p(j)\}$ to the biproduct over the full index type $J$. This is constructed using the inclusion morphisms $\iota_{j} : f(j) \to \bigoplus_{j \in p} f(j)$ for each $j$ satisfying $p(j)$.

CategoryTheory.Limits.biproduct.toSubtype definition

: ⨁ f ⟶ ⨁ Subtype.restrict p f

Full source

/-- The canonical morphism from a biproduct to the biproduct over a restriction of its index
type. -/
def biproduct.toSubtype : ⨁ f⨁ f ⟶ ⨁ Subtype.restrict p f :=
  biproduct.lift fun _ => biproduct.π _ _

Canonical morphism from biproduct to restricted biproduct

Informal description

Given a family of objects $f : J \to C$ in a category $C$ with zero morphisms and biproducts, and a predicate $p$ on $J$, the morphism $\text{biproduct.toSubtype} : \bigoplus f \to \bigoplus (\text{Subtype.restrict}\, p\, f)$ is the canonical morphism from the biproduct of the entire family to the biproduct of the subfamily restricted by $p$. This morphism is constructed using the universal property of the biproduct, where each component is given by the projection from the restricted biproduct.

CategoryTheory.Limits.biproduct.fromSubtype_π theorem

 [DecidablePred p] (j : J) :
  biproduct.fromSubtype f p ≫ biproduct.π f j = if h : p j then biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0

Full source

@[reassoc (attr := simp)]
theorem biproduct.fromSubtype_π [DecidablePred p] (j : J) :
    biproduct.fromSubtypebiproduct.fromSubtype f p ≫ biproduct.π f j =
      if h : p j then biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0 := by
  classical
  ext i; dsimp
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π]
  by_cases h : p j
  · rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
  · rw [dif_neg h, dif_neg (show (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)), comp_zero]

Composition of Restricted Biproduct Inclusion with Projection

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects in $C$. Given a decidable predicate $p$ on $J$ and an index $j \in J$, the composition of the inclusion morphism $\bigoplus_{j' \in p} f(j') \to \bigoplus_{j' \in J} f(j')$ with the projection $\bigoplus_{j' \in J} f(j') \to f(j)$ satisfies: \[ \text{fromSubtype}\, f\, p \circ \pi_j = \begin{cases} \pi_{\langle j, h\rangle} & \text{if } p(j) \text{ holds (with witness } h), \\ 0 & \text{otherwise.} \end{cases} \]

CategoryTheory.Limits.biproduct.fromSubtype_eq_lift theorem

 [DecidablePred p] :
  biproduct.fromSubtype f p = biproduct.lift fun j => if h : p j then biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0

Full source

theorem biproduct.fromSubtype_eq_lift [DecidablePred p] :
    biproduct.fromSubtype f p =
      biproduct.lift fun j => if h : p j then biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0 :=
  biproduct.hom_ext _ _ (by simp)

Inclusion from Restricted Biproduct as Lift of Conditional Projections

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects indexed by a type $J$ with a decidable predicate $p : J \to \mathrm{Prop}$. The inclusion morphism $\mathrm{fromSubtype}\, f\, p : \bigoplus_{j \in p} f(j) \to \bigoplus_{j \in J} f(j)$ is equal to the lift of the family of morphisms defined by: \[ \lambda j.\ \begin{cases} \pi_{\langle j, h\rangle} & \text{if } p(j) \text{ holds (with witness } h), \\ 0 & \text{otherwise.} \end{cases} \] where $\pi_{\langle j, h\rangle}$ is the projection from the restricted biproduct $\bigoplus_{j \in p} f(j)$ to $f(j)$.

CategoryTheory.Limits.biproduct.fromSubtype_π_subtype theorem

(j : Subtype p) : biproduct.fromSubtype f p ≫ biproduct.π f j = biproduct.π (Subtype.restrict p f) j

Full source

@[reassoc] -- Porting note: both version solved using simp
theorem biproduct.fromSubtype_π_subtype (j : Subtype p) :
    biproduct.fromSubtypebiproduct.fromSubtype f p ≫ biproduct.π f j = biproduct.π (Subtype.restrict p f) j := by
  classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Compatibility of Inclusion and Projection for Biproduct Subtypes

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects indexed by a type $J$ with a predicate $p : J \to \mathrm{Prop}$. For any $j \in \mathrm{Subtype}\ p$, the composition of the inclusion morphism $\mathrm{fromSubtype}\ f\ p : \bigoplus_{k \in \mathrm{Subtype}\ p} f(k) \to \bigoplus_{k \in J} f(k)$ with the projection morphism $\pi_j : \bigoplus_{k \in J} f(k) \to f(j)$ equals the projection morphism $\pi_j : \bigoplus_{k \in \mathrm{Subtype}\ p} f(k) \to f(j)$.

CategoryTheory.Limits.biproduct.toSubtype_π theorem

(j : Subtype p) : biproduct.toSubtype f p ≫ biproduct.π (Subtype.restrict p f) j = biproduct.π f j

Full source

@[reassoc (attr := simp)]
theorem biproduct.toSubtype_π (j : Subtype p) :
    biproduct.toSubtypebiproduct.toSubtype f p ≫ biproduct.π (Subtype.restrict p f) j = biproduct.π f j :=
  biproduct.lift_π _ _

Commutativity of Canonical Biproduct Morphism with Projections: $\text{toSubtype} \circ \pi_j = \pi_j$

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects with a biproduct $\bigoplus f$. Given a predicate $p$ on $J$ and an element $j$ in the subtype defined by $p$, the composition of the canonical morphism $\text{biproduct.toSubtype} : \bigoplus f \to \bigoplus (\text{Subtype.restrict}\, p\, f)$ with the projection $\pi_j : \bigoplus (\text{Subtype.restrict}\, p\, f) \to f(j)$ equals the projection $\pi_j : \bigoplus f \to f(j)$. That is, $\text{biproduct.toSubtype} \circ \pi_j = \pi_j$.

CategoryTheory.Limits.biproduct.ι_toSubtype theorem

 [DecidablePred p] (j : J) :
  biproduct.ι f j ≫ biproduct.toSubtype f p = if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0

Full source

@[reassoc (attr := simp)]
theorem biproduct.ι_toSubtype [DecidablePred p] (j : J) :
    biproduct.ιbiproduct.ι f j ≫ biproduct.toSubtype f p =
      if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0 := by
  classical
  ext i
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
  by_cases h : p j
  · rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
  · rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp]

Composition of Inclusion with Canonical Morphism to Restricted Biproduct

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects with a biproduct $\bigoplus f$. Given a decidable predicate $p$ on $J$, for any index $j \in J$, the composition of the inclusion morphism $\iota_j : f(j) \to \bigoplus f$ with the canonical morphism $\text{toSubtype} : \bigoplus f \to \bigoplus (\text{restrict}\, p\, f)$ satisfies: \[ \iota_j \circ \text{toSubtype} = \begin{cases} \iota_{\langle j, h \rangle} & \text{if } p(j) \text{ holds (with witness } h), \\ 0 & \text{otherwise.} \end{cases} \]

CategoryTheory.Limits.biproduct.toSubtype_eq_desc theorem

 [DecidablePred p] :
  biproduct.toSubtype f p = biproduct.desc fun j => if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0

Full source

theorem biproduct.toSubtype_eq_desc [DecidablePred p] :
    biproduct.toSubtype f p =
      biproduct.desc fun j => if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0 :=
  biproduct.hom_ext' _ _ (by simp)

Canonical Morphism to Restricted Biproduct as Universal Descending Morphism

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects indexed by $J$. Given a decidable predicate $p$ on $J$, the canonical morphism $\mathrm{toSubtype}\, f\, p : \bigoplus f \to \bigoplus (\mathrm{Subtype.restrict}\, p\, f)$ is equal to the morphism induced by the universal property of the biproduct, which sends each $j \in J$ to $\iota_{\langle j, h \rangle}$ if $p(j)$ holds (with witness $h$), and to the zero morphism otherwise. In symbols: \[ \mathrm{toSubtype}\, f\, p = \mathrm{desc} \left( \lambda j. \begin{cases} \iota_{\langle j, h \rangle} & \text{if } p(j) \text{ holds (with witness } h), \\ 0 & \text{otherwise.} \end{cases} \right). \]

CategoryTheory.Limits.biproduct.ι_toSubtype_subtype theorem

(j : Subtype p) : biproduct.ι f j ≫ biproduct.toSubtype f p = biproduct.ι (Subtype.restrict p f) j

Full source

@[reassoc]
theorem biproduct.ι_toSubtype_subtype (j : Subtype p) :
    biproduct.ιbiproduct.ι f j ≫ biproduct.toSubtype f p = biproduct.ι (Subtype.restrict p f) j := by
  classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Commutativity of Inclusion with Canonical Morphism to Restricted Biproduct

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $f : J \to \mathcal{C}$ be a family of objects indexed by $J$. Given a predicate $p$ on $J$ and an element $j \in \mathrm{Subtype}\, p$, the composition of the inclusion morphism $\iota_j : f(j) \to \bigoplus f$ with the canonical morphism $\mathrm{toSubtype}\, f\, p : \bigoplus f \to \bigoplus (\mathrm{Subtype.restrict}\, p\, f)$ equals the inclusion morphism $\iota_j : f(j) \to \bigoplus (\mathrm{Subtype.restrict}\, p\, f)$. In symbols: \[ \iota_j \circ \mathrm{toSubtype}\, f\, p = \iota_j. \]

CategoryTheory.Limits.biproduct.ι_fromSubtype theorem

(j : Subtype p) : biproduct.ι (Subtype.restrict p f) j ≫ biproduct.fromSubtype f p = biproduct.ι f j

Full source

@[reassoc (attr := simp)]
theorem biproduct.ι_fromSubtype (j : Subtype p) :
    biproduct.ιbiproduct.ι (Subtype.restrict p f) j ≫ biproduct.fromSubtype f p = biproduct.ι f j :=
  biproduct.ι_desc _ _

Commutativity of Restricted Biproduct Inclusion with Full Biproduct Inclusion: $\iota_j \circ \text{fromSubtype}_p = \iota_j$

Informal description

For any object $j$ in the subtype defined by the predicate $p$, the composition of the inclusion morphism $\iota_j$ from the restricted biproduct $\bigoplus_{k \in p} f(k)$ with the canonical inclusion morphism $\text{fromSubtype}_p$ into the full biproduct $\bigoplus_{k \in J} f(k)$ equals the inclusion morphism $\iota_j$ into the full biproduct. That is, $\iota_j \circ \text{fromSubtype}_p = \iota_j$.

CategoryTheory.Limits.biproduct.fromSubtype_toSubtype theorem

: biproduct.fromSubtype f p ≫ biproduct.toSubtype f p = 𝟙 (⨁ Subtype.restrict p f)

Full source

@[reassoc (attr := simp)]
theorem biproduct.fromSubtype_toSubtype :
    biproduct.fromSubtypebiproduct.fromSubtype f p ≫ biproduct.toSubtype f p = 𝟙 (⨁ Subtype.restrict p f) := by
  refine biproduct.hom_ext _ _ fun j => ?_
  rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]

Identity Property of Biproduct Inclusion and Restriction Morphisms

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects indexed by a type $J$ with a predicate $p : J \to \mathrm{Prop}$. The composition of the inclusion morphism $\mathrm{fromSubtype}\, f\, p : \bigoplus_{j \in \mathrm{Subtype}\, p} f(j) \to \bigoplus_{j \in J} f(j)$ with the canonical morphism $\mathrm{toSubtype}\, f\, p : \bigoplus_{j \in J} f(j) \to \bigoplus_{j \in \mathrm{Subtype}\, p} f(j)$ equals the identity morphism on the restricted biproduct $\bigoplus_{j \in \mathrm{Subtype}\, p} f(j)$. In symbols: \[ \mathrm{fromSubtype}\, f\, p \circ \mathrm{toSubtype}\, f\, p = \mathrm{id}_{\bigoplus_{j \in \mathrm{Subtype}\, p} f(j)}. \]

CategoryTheory.Limits.biproduct.toSubtype_fromSubtype theorem

 [DecidablePred p] :
  biproduct.toSubtype f p ≫ biproduct.fromSubtype f p = biproduct.map fun j => if p j then 𝟙 (f j) else 0

Full source

@[reassoc (attr := simp)]
theorem biproduct.toSubtype_fromSubtype [DecidablePred p] :
    biproduct.toSubtypebiproduct.toSubtype f p ≫ biproduct.fromSubtype f p =
      biproduct.map fun j => if p j then 𝟙 (f j) else 0 := by
  ext1 i
  by_cases h : p i
  · simp [h]
  · simp [h]

Composition of Biproduct Restriction and Inclusion Equals Component-wise Identity Map

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ be a family of objects with biproducts $\bigoplus f$ and $\bigoplus_{j \in p} f(j)$, where $p$ is a decidable predicate on $J$. The composition of the canonical morphism $\text{toSubtype}_p : \bigoplus f \to \bigoplus_{j \in p} f(j)$ with the inclusion morphism $\text{fromSubtype}_p : \bigoplus_{j \in p} f(j) \to \bigoplus f$ equals the biproduct map induced by the family of morphisms: \[ \text{toSubtype}_p \circ \text{fromSubtype}_p = \text{biproduct.map} \left( \lambda j, \begin{cases} \text{id}_{f(j)} & \text{if } p(j), \\ 0 & \text{otherwise.} \end{cases} \right) \]

CategoryTheory.Limits.biproduct.isLimitFromSubtype definition

: IsLimit (KernelFork.ofι (biproduct.fromSubtype f fun j => j ≠ i) (by simp) : KernelFork (biproduct.π f i))

Full source

/-- The kernel of `biproduct.π f i` is the inclusion from the biproduct which omits `i`
from the index set `J` into the biproduct over `J`. -/
def biproduct.isLimitFromSubtype :
    IsLimit (KernelFork.ofι (biproduct.fromSubtype f fun j => j ≠ i) (by simp) :
    KernelFork (biproduct.π f i)) :=
  Fork.IsLimit.mk' _ fun s =>
    ⟨s.ι ≫ biproduct.toSubtype _ _, by
      apply biproduct.hom_ext; intro j
      rw [KernelFork.ι_ofι, Category.assoc, Category.assoc,
        biproduct.toSubtype_fromSubtype_assoc, biproduct.map_π]
      rcases Classical.em (i = j) with (rfl | h)
      · rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]
      · rw [if_pos (Ne.symm h), Category.comp_id], by
      intro m hm
      rw [← hm, KernelFork.ι_ofι, Category.assoc, biproduct.fromSubtype_toSubtype]
      exact (Category.comp_id _).symm⟩

Kernel of biproduct projection as restricted biproduct

Informal description

The kernel of the projection $\pi_i : \bigoplus f \to f(i)$ is isomorphic to the biproduct $\bigoplus_{j \neq i} f(j)$, and the inclusion morphism $\bigoplus_{j \neq i} f(j) \to \bigoplus f$ exhibits this biproduct as the limit of the kernel fork of $\pi_i$.

CategoryTheory.Limits.instHasKernelπ instance

: HasKernel (biproduct.π f i)

Full source

instance : HasKernel (biproduct.π f i) :=
  HasLimit.mk ⟨_, biproduct.isLimitFromSubtype f i⟩

Existence of Kernels for Biproduct Projections

Informal description

For any family of objects $f : J \to C$ in a category $C$ with zero morphisms and biproducts, and any index $i \in J$, the projection morphism $\pi_i : \bigoplus f \to f(i)$ has a kernel.

CategoryTheory.Limits.kernelBiproductπIso definition

: kernel (biproduct.π f i) ≅ ⨁ Subtype.restrict (fun j => j ≠ i) f

Full source

/-- The kernel of `biproduct.π f i` is `⨁ Subtype.restrict {i}ᶜ f`. -/
@[simps!]
def kernelBiproductπIso : kernelkernel (biproduct.π f i) ≅ ⨁ Subtype.restrict (fun j => j ≠ i) f :=
  limit.isoLimitCone ⟨_, biproduct.isLimitFromSubtype f i⟩

Isomorphism between kernel of biproduct projection and restricted biproduct

Informal description

The kernel of the projection morphism $\pi_i : \bigoplus f \to f(i)$ is isomorphic to the biproduct $\bigoplus_{j \neq i} f(j)$ of the family $f$ restricted to indices $j \neq i$.

CategoryTheory.Limits.biproduct.isColimitToSubtype definition

 : IsColimit (CokernelCofork.ofπ (biproduct.toSubtype f fun j => j ≠ i) (by simp) : CokernelCofork (biproduct.ι f i))

Full source

/-- The cokernel of `biproduct.ι f i` is the projection from the biproduct over the index set `J`
onto the biproduct omitting `i`. -/
def biproduct.isColimitToSubtype :
    IsColimit (CokernelCofork.ofπ (biproduct.toSubtype f fun j => j ≠ i) (by simp) :
    CokernelCofork (biproduct.ι f i)) :=
  Cofork.IsColimit.mk' _ fun s =>
    ⟨biproduct.fromSubtype _ _ ≫ s.π, by
      apply biproduct.hom_ext'; intro j
      rw [CokernelCofork.π_ofπ, biproduct.toSubtype_fromSubtype_assoc, biproduct.ι_map_assoc]
      rcases Classical.em (i = j) with (rfl | h)
      · rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]
      · rw [if_pos (Ne.symm h), Category.id_comp], by
      intro m hm
      rw [← hm, CokernelCofork.π_ofπ, ← Category.assoc, biproduct.fromSubtype_toSubtype]
      exact (Category.id_comp _).symm⟩

Cokernel of biproduct inclusion as restricted biproduct

Informal description

The cokernel of the inclusion morphism $\iota_i : f(i) \to \bigoplus f$ is isomorphic to the biproduct $\bigoplus_{j \neq i} f(j)$, and the canonical morphism $\text{biproduct.toSubtype} : \bigoplus f \to \bigoplus_{j \neq i} f(j)$ induces a colimit cofork that realizes this cokernel. Specifically, the cofork formed by $\text{biproduct.toSubtype}$ is a colimit cocone, meaning it satisfies the universal property of the cokernel of $\iota_i$.

CategoryTheory.Limits.instHasCokernelι instance

: HasCokernel (biproduct.ι f i)

Full source

instance : HasCokernel (biproduct.ι f i) :=
  HasColimit.mk ⟨_, biproduct.isColimitToSubtype f i⟩

Existence of Cokernel for Biproduct Inclusion Morphism

Informal description

For any family of objects $f : J \to C$ in a category $C$ with zero morphisms and a biproduct $\bigoplus f$, the inclusion morphism $\iota_i : f(i) \to \bigoplus f$ has a cokernel.

CategoryTheory.Limits.cokernelBiproductιIso definition

: cokernel (biproduct.ι f i) ≅ ⨁ Subtype.restrict (fun j => j ≠ i) f

Full source

/-- The cokernel of `biproduct.ι f i` is `⨁ Subtype.restrict {i}ᶜ f`. -/
@[simps!]
def cokernelBiproductιIso : cokernelcokernel (biproduct.ι f i) ≅ ⨁ Subtype.restrict (fun j => j ≠ i) f :=
  colimit.isoColimitCocone ⟨_, biproduct.isColimitToSubtype f i⟩

Isomorphism between cokernel of biproduct inclusion and restricted biproduct

Informal description

The cokernel of the inclusion morphism $\iota_i : f(i) \to \bigoplus f$ is isomorphic to the biproduct $\bigoplus_{j \neq i} f(j)$ of the family $f$ restricted to indices $j \neq i$.

CategoryTheory.Limits.kernelForkBiproductToSubtype definition

(p : Set K) : LimitCone (parallelPair (biproduct.toSubtype f p) 0)

Full source

/-- The limit cone exhibiting `⨁ Subtype.restrict pᶜ f` as the kernel of
`biproduct.toSubtype f p` -/
@[simps]
def kernelForkBiproductToSubtype (p : Set K) :
    LimitCone (parallelPair (biproduct.toSubtype f p) 0) where
  cone :=
    KernelFork.ofι (biproduct.fromSubtype f pᶜ)
      (by
        classical
        ext j k
        simp only [Category.assoc, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
          comp_zero, zero_comp]
        rw [dif_neg k.2]
        simp only [zero_comp])
  isLimit :=
    KernelFork.IsLimit.ofι _ _ (fun {_} g _ => g ≫ biproduct.toSubtype f pᶜ)
      (by
        classical
        intro W' g' w
        ext j
        simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply,
          biproduct.map_π]
        split_ifs with h
        · simp
        · replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
          simpa using w.symm)
      (by aesop_cat)

Limit cone for the kernel of the biproduct-to-subtype morphism

Informal description

Given a family of objects $ f : K \to C $ in a category $ C $ with zero morphisms and biproducts, and a subset $ p \subseteq K $, the limit cone for the parallel pair consisting of the canonical morphism $ \text{biproduct.toSubtype} f p : \bigoplus f \to \bigoplus (\text{Subtype.restrict} p f) $ and the zero morphism is constructed. This limit cone exhibits $ \bigoplus (\text{Subtype.restrict} p^\complement f) $ as the kernel of $ \text{biproduct.toSubtype} f p $, where $ p^\complement $ denotes the complement of $ p $ in $ K $.

CategoryTheory.Limits.instHasKernelToSubtype instance

(p : Set K) : HasKernel (biproduct.toSubtype f p)

Full source

instance (p : Set K) : HasKernel (biproduct.toSubtype f p) :=
  HasLimit.mk (kernelForkBiproductToSubtype f p)

Existence of Kernels for Biproduct-to-Subtype Morphisms

Informal description

For any family of objects $f : K \to C$ in a category $C$ with zero morphisms and biproducts, and any subset $p \subseteq K$, the canonical morphism $\text{biproduct.toSubtype}\, f\, p : \bigoplus f \to \bigoplus (\text{Subtype.restrict}\, p\, f)$ has a kernel.

CategoryTheory.Limits.kernelBiproductToSubtypeIso definition

(p : Set K) : kernel (biproduct.toSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f

Full source

/-- The kernel of `biproduct.toSubtype f p` is `⨁ Subtype.restrict pᶜ f`. -/
@[simps!]
def kernelBiproductToSubtypeIso (p : Set K) :
    kernelkernel (biproduct.toSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f :=
  limit.isoLimitCone (kernelForkBiproductToSubtype f p)

Kernel of biproduct-to-subtype morphism is complement biproduct

Informal description

For a family of objects $ f : K \to C $ in a category $ C $ with zero morphisms and biproducts, and a subset $ p \subseteq K $, the kernel of the canonical morphism $ \text{biproduct.toSubtype}\, f\, p : \bigoplus f \to \bigoplus (\text{Subtype.restrict}\, p\, f) $ is isomorphic to the biproduct of the subfamily restricted to the complement $ p^\complement $ of $ p $. In symbols: \[ \ker\left(\bigoplus f \to \bigoplus_{k \in p} f(k)\right) \cong \bigoplus_{k \notin p} f(k) \]

CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype definition

(p : Set K) : ColimitCocone (parallelPair (biproduct.fromSubtype f p) 0)

Full source

/-- The colimit cocone exhibiting `⨁ Subtype.restrict pᶜ f` as the cokernel of
`biproduct.fromSubtype f p` -/
@[simps]
def cokernelCoforkBiproductFromSubtype (p : Set K) :
    ColimitCocone (parallelPair (biproduct.fromSubtype f p) 0) where
  cocone :=
    CokernelCofork.ofπ (biproduct.toSubtype f pᶜ)
      (by
        classical
        ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2)
  isColimit :=
    CokernelCofork.IsColimit.ofπ _ _ (fun {_} g _ => biproduct.fromSubtypebiproduct.fromSubtype f pᶜ ≫ g)
      (by
        classical
        intro W g' w
        ext j
        simp only [biproduct.toSubtype_fromSubtype_assoc, Pi.compl_apply, biproduct.ι_map_assoc]
        split_ifs with h
        · simp
        · replace w := biproduct.ιbiproduct.ι _ (⟨j, not_not.mp h⟩ : p) ≫= w
          simpa using w.symm)
      (by aesop_cat)

Cokernel cocone for the inclusion from a restricted biproduct

Informal description

Given a family of objects $ f : K \to C $ in a category $ C $ with zero morphisms and a subset $ p \subseteq K $, the colimit cocone for the parallel pair consisting of the inclusion morphism $ \text{biproduct.fromSubtype}\, f\, p : \bigoplus_{k \in p} f(k) \to \bigoplus_{k \in K} f(k) $ and the zero morphism exhibits $ \bigoplus_{k \notin p} f(k) $ as the cokernel of $ \text{biproduct.fromSubtype}\, f\, p $. This means that the cokernel of the inclusion morphism from the restricted biproduct (over $ p $) to the full biproduct is isomorphic to the biproduct over the complement of $ p $.

CategoryTheory.Limits.instHasCokernelFromSubtype instance

(p : Set K) : HasCokernel (biproduct.fromSubtype f p)

Full source

instance (p : Set K) : HasCokernel (biproduct.fromSubtype f p) :=
  HasColimit.mk (cokernelCoforkBiproductFromSubtype f p)

Existence of Cokernel for Inclusion from Restricted Biproduct

Informal description

For any family of objects $f : K \to C$ in a category $C$ with zero morphisms and any subset $p \subseteq K$, the inclusion morphism $\bigoplus_{k \in p} f(k) \to \bigoplus_{k \in K} f(k)$ has a cokernel.

CategoryTheory.Limits.cokernelBiproductFromSubtypeIso definition

(p : Set K) : cokernel (biproduct.fromSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f

Full source

/-- The cokernel of `biproduct.fromSubtype f p` is `⨁ Subtype.restrict pᶜ f`. -/
@[simps!]
def cokernelBiproductFromSubtypeIso (p : Set K) :
    cokernelcokernel (biproduct.fromSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f :=
  colimit.isoColimitCocone (cokernelCoforkBiproductFromSubtype f p)

Isomorphism between cokernel of inclusion and biproduct over complement

Informal description

For a family of objects $ f : K \to C $ in a category $ C $ with zero morphisms and a subset $ p \subseteq K $, the cokernel of the inclusion morphism $ \bigoplus_{k \in p} f(k) \to \bigoplus_{k \in K} f(k) $ is isomorphic to the biproduct $ \bigoplus_{k \notin p} f(k) $.

CategoryTheory.Limits.biproduct.matrix definition

(m : ∀ j k, f j ⟶ g k) : ⨁ f ⟶ ⨁ g

Full source

/-- Convert a (dependently typed) matrix to a morphism of biproducts. -/
def biproduct.matrix (m : ∀ j k, f j ⟶ g k) : ⨁ f⨁ f ⟶ ⨁ g :=
  biproduct.desc fun j => biproduct.lift fun k => m j k

Matrix-induced morphism between biproducts

Informal description

Given a family of objects $ f : J \to C $ and $ g : K \to C $ in a category $ C $ with zero morphisms and biproducts, and a matrix of morphisms $ m_{jk} : f(j) \to g(k) $ for each $ j \in J $ and $ k \in K $, the morphism $ \text{biproduct.matrix}\, m : \bigoplus f \to \bigoplus g $ is constructed by first lifting each row $ m_{j\bullet} $ to a morphism $ f(j) \to \bigoplus g $ and then descending these to a single morphism from the biproduct $ \bigoplus f $.

CategoryTheory.Limits.biproduct.matrix_π theorem

(m : ∀ j k, f j ⟶ g k) (k : K) : biproduct.matrix m ≫ biproduct.π g k = biproduct.desc fun j => m j k

Full source

@[reassoc (attr := simp)]
theorem biproduct.matrix_π (m : ∀ j k, f j ⟶ g k) (k : K) :
    biproduct.matrixbiproduct.matrix m ≫ biproduct.π g k = biproduct.desc fun j => m j k := by
  ext
  simp [biproduct.matrix]

Commutativity of Biproduct Matrix with Projections: $\text{matrix}\, m \circ \pi_k = \text{desc}\, (m_{\bullet,k})$

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ and $g : K \to C$ be families of objects with biproducts $\bigoplus f$ and $\bigoplus g$ respectively. Given a matrix of morphisms $m_{j,k} : f(j) \to g(k)$ for each $j \in J$ and $k \in K$, the composition of the induced morphism $\text{biproduct.matrix}\, m : \bigoplus f \to \bigoplus g$ with the projection $\pi_k : \bigoplus g \to g(k)$ equals the morphism $\text{biproduct.desc}\, (m_{\bullet,k}) : \bigoplus f \to g(k)$ induced by the $k$-th column of $m$.

CategoryTheory.Limits.biproduct.ι_matrix theorem

(m : ∀ j k, f j ⟶ g k) (j : J) : biproduct.ι f j ≫ biproduct.matrix m = biproduct.lift fun k => m j k

Full source

@[reassoc (attr := simp)]
theorem biproduct.ι_matrix (m : ∀ j k, f j ⟶ g k) (j : J) :
    biproduct.ιbiproduct.ι f j ≫ biproduct.matrix m = biproduct.lift fun k => m j k := by
  ext
  simp [biproduct.matrix]

Commutativity of inclusion with matrix morphism: $\iota_j \circ \text{matrix}\, m = \text{lift}\, (k \mapsto m_{jk})$

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ and $g : K \to C$ be families of objects with biproducts $\bigoplus f$ and $\bigoplus g$ respectively. Given a matrix of morphisms $m_{jk} : f(j) \to g(k)$ for each $j \in J$ and $k \in K$, the composition of the inclusion morphism $\iota_j : f(j) \to \bigoplus f$ with the matrix-induced morphism $\text{matrix}\, m : \bigoplus f \to \bigoplus g$ equals the lifted morphism $\text{lift}\, (k \mapsto m_{jk}) : f(j) \to \bigoplus g$ for each $j \in J$. That is, $\iota_j \circ (\text{matrix}\, m) = \text{lift}\, (k \mapsto m_{jk})$.

CategoryTheory.Limits.biproduct.components definition

(m : ⨁ f ⟶ ⨁ g) (j : J) (k : K) : f j ⟶ g k

Full source

/-- Extract the matrix components from a morphism of biproducts. -/
def biproduct.components (m : ⨁ f⨁ f ⟶ ⨁ g) (j : J) (k : K) : f j ⟶ g k :=
  biproduct.ιbiproduct.ι f j ≫ m ≫ biproduct.π g k

Matrix components of a biproduct morphism

Informal description

Given a morphism $m : \bigoplus f \to \bigoplus g$ between biproducts in a category with zero morphisms, and indices $j \in J$, $k \in K$, the component $(m)_{j,k} : f_j \to g_k$ is obtained by pre-composing $m$ with the inclusion $\iota_j : f_j \to \bigoplus f$ and post-composing with the projection $\pi_k : \bigoplus g \to g_k$.

CategoryTheory.Limits.biproduct.matrix_components theorem

(m : ∀ j k, f j ⟶ g k) (j : J) (k : K) : biproduct.components (biproduct.matrix m) j k = m j k

Full source

@[simp]
theorem biproduct.matrix_components (m : ∀ j k, f j ⟶ g k) (j : J) (k : K) :
    biproduct.components (biproduct.matrix m) j k = m j k := by simp [biproduct.components]

Matrix components of biproduct morphism: $(\text{matrix}\, m)_{j,k} = m_{j,k}$

Informal description

Let $C$ be a category with zero morphisms and biproducts, and let $f : J \to C$ and $g : K \to C$ be families of objects. Given a matrix of morphisms $m_{j,k} : f(j) \to g(k)$ for each $j \in J$ and $k \in K$, the $(j,k)$-th component of the induced morphism $\text{biproduct.matrix}\, m : \bigoplus f \to \bigoplus g$ equals $m_{j,k}$.

CategoryTheory.Limits.biproduct.components_matrix theorem

(m : ⨁ f ⟶ ⨁ g) : (biproduct.matrix fun j k => biproduct.components m j k) = m

Full source

@[simp]
theorem biproduct.components_matrix (m : ⨁ f⨁ f ⟶ ⨁ g) :
    (biproduct.matrix fun j k => biproduct.components m j k) = m := by
  ext
  simp [biproduct.components]

Matrix Reconstruction from Components: $\text{matrix}\, (m_{j,k}) = m$

Informal description

For any morphism $m : \bigoplus f \to \bigoplus g$ between biproducts in a category with zero morphisms, the matrix constructed from the components of $m$ equals $m$ itself. That is, if we extract the components $(m)_{j,k} : f_j \to g_k$ for each $j \in J$ and $k \in K$, and then form the morphism $\text{biproduct.matrix}\, (m_{j,k})$, the result is identical to the original morphism $m$.

CategoryTheory.Limits.biproduct.matrixEquiv definition

: (⨁ f ⟶ ⨁ g) ≃ ∀ j k, f j ⟶ g k

Full source

/-- Morphisms between direct sums are matrices. -/
@[simps]
def biproduct.matrixEquiv : (⨁ f ⟶ ⨁ g) ≃ ∀ j k, f j ⟶ g k where
  toFun := biproduct.components
  invFun := biproduct.matrix
  left_inv := biproduct.components_matrix
  right_inv m := by
    ext
    apply biproduct.matrix_components

Equivalence between biproduct morphisms and matrices

Informal description

The equivalence between morphisms $\bigoplus f \to \bigoplus g$ between biproducts and matrices of morphisms $(f_j \to g_k)_{j \in J, k \in K}$ in a category with zero morphisms and biproducts. The forward direction extracts the matrix components of a morphism, while the inverse constructs a morphism from a given matrix.

CategoryTheory.Limits.biproduct.ι_mono instance

(f : J → C) [HasBiproduct f] (b : J) : IsSplitMono (biproduct.ι f b)

Full source

instance biproduct.ι_mono (f : J → C) [HasBiproduct f] (b : J) : IsSplitMono (biproduct.ι f b) := by
  classical exact IsSplitMono.mk' { retraction := biproduct.desc <| Pi.single b (𝟙 (f b)) }

Inclusion into Biproduct is Split Mono

Informal description

For any family of objects $f : J \to C$ in a category $C$ with biproducts, and for any index $b \in J$, the inclusion morphism $\iota_b : f(b) \to \bigoplus f$ is a split monomorphism. This means there exists a morphism $\pi_b : \bigoplus f \to f(b)$ such that $\pi_b \circ \iota_b$ is the identity on $f(b)$.

CategoryTheory.Limits.biproduct.π_epi instance

(f : J → C) [HasBiproduct f] (b : J) : IsSplitEpi (biproduct.π f b)

Full source

instance biproduct.π_epi (f : J → C) [HasBiproduct f] (b : J) : IsSplitEpi (biproduct.π f b) := by
  classical exact IsSplitEpi.mk' { section_ := biproduct.lift <| Pi.single b (𝟙 (f b)) }

Biproduct Projections are Split Epimorphisms

Informal description

For any family of objects $f : J \to C$ in a category $C$ with zero morphisms and biproducts, and for any index $b \in J$, the projection morphism $\pi_b : \bigoplus f \to f(b)$ is a split epimorphism.

CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom theorem

 (f : J → C) [HasBiproduct f] {b : Bicone f} (hb : b.IsBilimit) :
  (hb.isLimit.conePointUniqueUpToIso (biproduct.isLimit _)).hom = biproduct.lift b.π

Full source

/-- Auxiliary lemma for `biproduct.uniqueUpToIso`. -/
theorem biproduct.conePointUniqueUpToIso_hom (f : J → C) [HasBiproduct f] {b : Bicone f}
    (hb : b.IsBilimit) :
    (hb.isLimit.conePointUniqueUpToIso (biproduct.isLimit _)).hom = biproduct.lift b.π :=
  rfl

Homomorphism part of the unique isomorphism between bicone apex and biproduct equals the lift of projections

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, and let $F : J \to \mathcal{C}$ be a family of objects in $\mathcal{C}$ that has a biproduct. Given a bicone $B$ over $F$ that is a bilimit (i.e., simultaneously a limit and colimit), the homomorphism part of the unique isomorphism between the apex of $B$ and the biproduct $\bigoplus F$ is equal to the morphism $\text{biproduct.lift}\, B.\pi$ induced by the projections $B.\pi_j : B.\text{pt} \to F(j)$.

CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv theorem

 (f : J → C) [HasBiproduct f] {b : Bicone f} (hb : b.IsBilimit) :
  (hb.isLimit.conePointUniqueUpToIso (biproduct.isLimit _)).inv = biproduct.desc b.ι

Full source

/-- Auxiliary lemma for `biproduct.uniqueUpToIso`. -/
theorem biproduct.conePointUniqueUpToIso_inv (f : J → C) [HasBiproduct f] {b : Bicone f}
    (hb : b.IsBilimit) :
    (hb.isLimit.conePointUniqueUpToIso (biproduct.isLimit _)).inv = biproduct.desc b.ι := by
  classical
  refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_
  rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

Inverse of Biproduct Isomorphism Equals Descending Morphism via Injections

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and biproducts, and let $F : J \to \mathcal{C}$ be a family of objects in $\mathcal{C}$. Given a bicone $B$ over $F$ that is a bilimit (i.e., simultaneously a limit and colimit), the inverse morphism of the unique isomorphism between the apex of $B$ and the biproduct $\bigoplus F$ is equal to the morphism $\text{biproduct.desc}\, B.\iota$ induced by the injections $B.\iota_j : F(j) \to B.\text{pt}$.

CategoryTheory.Limits.biproduct.uniqueUpToIso definition

(f : J → C) [HasBiproduct f] {b : Bicone f} (hb : b.IsBilimit) : b.pt ≅ ⨁ f

Full source

/-- Biproducts are unique up to isomorphism. This already follows because bilimits are limits,
    but in the case of biproducts we can give an isomorphism with particularly nice definitional
    properties, namely that `biproduct.lift b.π` and `biproduct.desc b.ι` are inverses of each
    other. -/
@[simps]
def biproduct.uniqueUpToIso (f : J → C) [HasBiproduct f] {b : Bicone f} (hb : b.IsBilimit) :
    b.pt ≅ ⨁ f where
  hom := biproduct.lift b.π
  inv := biproduct.desc b.ι
  hom_inv_id := by
    rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.hom_inv_id]
  inv_hom_id := by
    rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.inv_hom_id]

Canonical isomorphism between bicone point and biproduct

Informal description

Given a family of objects $ f : J \to C $ in a category $ C $ with zero morphisms and biproducts, and a bicone $ b $ for $ f $ that is both a limit and a colimit (i.e., $ b $ is a bilimit bicone), there exists a canonical isomorphism $ b.pt \cong \bigoplus f $ between the bicone point $ b.pt $ and the biproduct $ \bigoplus f $. This isomorphism is constructed using the universal properties of the biproduct, with the forward morphism given by lifting the bicone's projections $ b.π $ and the inverse morphism given by descending the bicone's injections $ b.ι $.

CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts instance

[HasFiniteBiproducts C] : HasZeroObject C

Full source

/-- A category with finite biproducts has a zero object. -/
instance (priority := 100) hasZeroObject_of_hasFiniteBiproducts [HasFiniteBiproducts C] :
    HasZeroObject C := by
  refine ⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩
  · intro a; apply biproduct.hom_ext'; simp
  · intro a; apply biproduct.hom_ext; simp

Existence of Zero Object in Categories with Finite Biproducts

Informal description

Every category with finite biproducts has a zero object.

CategoryTheory.Limits.limitBiconeOfUnique definition

[Unique J] (f : J → C) : LimitBicone f

Full source

/-- The limit bicone for the biproduct over an index type with exactly one term. -/
@[simps]
def limitBiconeOfUnique [Unique J] (f : J → C) : LimitBicone f where
  bicone :=
    { pt := f default
      π := fun j => eqToHom (by congr; rw [← Unique.uniq] )
      ι := fun j => eqToHom (by congr; rw [← Unique.uniq] ) }
  isBilimit :=
    { isLimit := (limitConeOfUnique f).isLimit
      isColimit := (colimitCoconeOfUnique f).isColimit }

Limit bicone for biproduct over a unique index type

Informal description

Given a category $ C $ and an index type $ J $ with exactly one term (i.e., `Unique J`), the limit bicone for the biproduct of a family of objects $ f : J \to C $ is constructed with the bicone point being $ f(\text{default}) $, where $\text{default}$ is the unique term of $ J $. The projection and injection morphisms are given by the identity morphisms (via `eqToHom`), utilizing the fact that $ J $ has only one term. The bicone is both a limit cone and a colimit cocone, inheriting these properties from the corresponding limit cone and colimit cocone constructions for unique index types.

CategoryTheory.Limits.hasBiproduct_unique instance

[Subsingleton J] [Nonempty J] (f : J → C) : HasBiproduct f

Full source

instance (priority := 100) hasBiproduct_unique [Subsingleton J] [Nonempty J] (f : J → C) :
    HasBiproduct f :=
  let ⟨_⟩ := nonempty_unique J; .mk (limitBiconeOfUnique f)

Existence of Biproducts for Diagrams over Subsingleton Index Types

Informal description

For any category $C$ with zero morphisms and any subsingleton nonempty index type $J$, every diagram $f \colon J \to C$ has a biproduct. This means there exists an object in $C$ that serves simultaneously as both the limit and colimit of $f$, with the appropriate projection and injection morphisms satisfying the biproduct conditions.

CategoryTheory.Limits.biproductUniqueIso definition

[Unique J] (f : J → C) : ⨁ f ≅ f default

Full source

/-- A biproduct over an index type with exactly one term is just the object over that term. -/
@[simps!]
def biproductUniqueIso [Unique J] (f : J → C) : ⨁ f⨁ f ≅ f default :=
  (biproduct.uniqueUpToIso _ (limitBiconeOfUnique f).isBilimit).symm

Canonical isomorphism between biproduct and object for unique index type

Informal description

Given a category $ C $ and an index type $ J $ with exactly one term (i.e., `Unique J`), there is a canonical isomorphism between the biproduct $ \bigoplus f $ of a family of objects $ f : J \to C $ and the object $ f(\text{default}) $, where $\text{default}$ is the unique term of $ J $. This isomorphism arises because the biproduct over a singleton index type is essentially just the object itself.

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Notation

Implementation notes