Mathlib.CategoryTheory.Preadditive.Biproducts

CategoryTheory.Limits.isBilimitOfTotal definition

{f : J → C} (b : Bicone f) (total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt) : b.IsBilimit

Full source

/-- In a preadditive category, we can construct a biproduct for `f : J → C` from
any bicone `b` for `f` satisfying `total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
-/
def isBilimitOfTotal {f : J → C} (b : Bicone f) (total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt) :
    b.IsBilimit where
  isLimit :=
    { lift := fun s => ∑ j : J, s.π.app ⟨j⟩ ≫ b.ι j
      uniq := fun s m h => by
        erw [← Category.comp_id m, ← total, comp_sum]
        apply Finset.sum_congr rfl
        intro j _
        have reassoced : m ≫ Bicone.π b j ≫ Bicone.ι b j = s.π.app ⟨j⟩ ≫ Bicone.ι b j := by
          erw [← Category.assoc, eq_whisker (h ⟨j⟩)]
        rw [reassoced]
      fac := fun s j => by
        classical
        cases j
        simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]
        -- See note [dsimp, simp].
        dsimp
        simp }
  isColimit :=
    { desc := fun s => ∑ j : J, b.π j ≫ s.ι.app ⟨j⟩
      uniq := fun s m h => by
        erw [← Category.id_comp m, ← total, sum_comp]
        apply Finset.sum_congr rfl
        intro j _
        erw [Category.assoc, h ⟨j⟩]
      fac := fun s j => by
        classical
        cases j
        simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
        dsimp; simp }

Bilimit bicone from total condition

Informal description

Given a bicone $b$ over a family of objects $f : J \to C$ in a preadditive category $C$, if the condition $\sum_{j \in J} b.\pi_j \circ b.\iota_j = \mathrm{id}_{b.\mathrm{pt}}$ holds, then $b$ is a bilimit bicone. This means that $b$ simultaneously satisfies the universal properties of both a limit cone and a colimit cocone for the family $f$.

CategoryTheory.Limits.IsBilimit.total theorem

{f : J → C} {b : Bicone f} (i : b.IsBilimit) : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt

Full source

theorem IsBilimit.total {f : J → C} {b : Bicone f} (i : b.IsBilimit) :
    ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt :=
  i.isLimit.hom_ext fun j => by
    classical
    cases j
    simp [sum_comp, b.ι_π, comp_dite]

Biproduct Total Morphism Identity in Preadditive Categories

Informal description

Let $\mathcal{C}$ be a preadditive category, $J$ a finite index set, and $f : J \to \mathcal{C}$ 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 sum of the compositions of the projection and inclusion morphisms equals the identity morphism on the biproduct object: \[ \sum_{j \in J} \pi_j \circ \iota_j = \mathrm{id}_{\bigoplus f} \] where $\pi_j : \bigoplus f \to f_j$ are the projections and $\iota_j : f_j \to \bigoplus f$ are the inclusions.

CategoryTheory.Limits.hasBiproduct_of_total theorem

{f : J → C} (b : Bicone f) (total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt) : HasBiproduct f

Full source

/-- In a preadditive category, we can construct a biproduct for `f : J → C` from
any bicone `b` for `f` satisfying `total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
-/
theorem hasBiproduct_of_total {f : J → C} (b : Bicone f)
    (total : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt) : HasBiproduct f :=
  HasBiproduct.mk
    { bicone := b
      isBilimit := isBilimitOfTotal b total }

Existence of Biproduct from Total Morphism Condition

Informal description

Let $\mathcal{C}$ be a preadditive category, $J$ a finite index set, and $f : J \to \mathcal{C}$ a family of objects in $\mathcal{C}$. Given a bicone $b$ over $f$ such that the sum of the compositions of the projection and inclusion morphisms satisfies \[ \sum_{j \in J} b.\pi_j \circ b.\iota_j = \mathrm{id}_{b.\mathrm{pt}}, \] then $f$ has a biproduct in $\mathcal{C}$.

CategoryTheory.Limits.isBilimitOfIsLimit definition

{f : J → C} (t : Bicone f) (ht : IsLimit t.toCone) : t.IsBilimit

Full source

/-- In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit
    bicone. -/
def isBilimitOfIsLimit {f : J → C} (t : Bicone f) (ht : IsLimit t.toCone) : t.IsBilimit :=
  isBilimitOfTotal _ <|
    ht.hom_ext fun j => by
      classical
      cases j
      simp [sum_comp, t.ι_π, dite_comp, comp_dite]

Bilimit bicone from limit cone in preadditive categories

Informal description

Given a bicone $t$ over a finite family of objects $f : J \to C$ in a preadditive category $C$, if the underlying cone of $t$ is a limit cone, then $t$ is a bilimit bicone. This means that $t$ simultaneously satisfies the universal properties of both a limit cone and a colimit cocone for the family $f$.

CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit definition

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

Full source

/-- We can turn any limit cone over a pair into a bilimit bicone. -/
def biconeIsBilimitOfLimitConeOfIsLimit {f : J → C} {t : Cone (Discrete.functor f)}
    (ht : IsLimit t) : (Bicone.ofLimitCone ht).IsBilimit :=
  isBilimitOfIsLimit _ <| IsLimit.ofIsoLimit ht <| Cones.ext (Iso.refl _) (by simp)

Bilimit bicone from limit cone in preadditive categories

Informal description

Given a limit cone `t` over a discrete diagram of objects `f : J → C` in a preadditive category `C`, the bicone constructed from this limit cone is a bilimit bicone. That is, it satisfies both the universal properties of a limit cone and a colimit cocone for the family `f`.

CategoryTheory.Limits.isBilimitOfIsColimit definition

{f : J → C} (t : Bicone f) (ht : IsColimit t.toCocone) : t.IsBilimit

Full source

/-- In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit
    bicone. -/
def isBilimitOfIsColimit {f : J → C} (t : Bicone f) (ht : IsColimit t.toCocone) : t.IsBilimit :=
  isBilimitOfTotal _ <|
    ht.hom_ext fun j => by
      classical
      cases j
      simp_rw [Bicone.toCocone_ι_app, comp_sum, ← Category.assoc, t.ι_π, dite_comp]
      simp

Bilimit bicone from colimit cocone

Informal description

Given a bicone $t$ over a family of objects $f : J \to C$ in a preadditive category $C$, if the cocone associated to $t$ is a colimit cocone, then $t$ is a bilimit bicone. This means that $t$ simultaneously satisfies the universal properties of both a limit cone and a colimit cocone for the family $f$.

CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit definition

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

Full source

/-- We can turn any limit cone over a pair into a bilimit bicone. -/
def biconeIsBilimitOfColimitCoconeOfIsColimit {f : J → C} {t : Cocone (Discrete.functor f)}
    (ht : IsColimit t) : (Bicone.ofColimitCocone ht).IsBilimit :=
  isBilimitOfIsColimit _ <| IsColimit.ofIsoColimit ht <| Cocones.ext (Iso.refl _) <| by
    rintro ⟨j⟩; simp

Bilimit bicone from colimit cocone

Informal description

Given a colimit cocone `t` over a discrete diagram of objects `f : J → C` in a preadditive category `C`, the bicone constructed from this colimit cocone is a bilimit bicone. That is, the bicone simultaneously satisfies the universal properties of both a limit cone and a colimit cocone for the family `f`.

CategoryTheory.Limits.HasBiproduct.of_hasProduct theorem

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

Full source

/-- In a preadditive category, if the product over `f : J → C` exists,
    then the biproduct over `f` exists. -/
theorem HasBiproduct.of_hasProduct (f : J → C) [HasProduct f] : HasBiproduct f := by
  cases nonempty_fintype J
  exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

Existence of Biproducts from Products in Preadditive Categories

Informal description

In a preadditive category, if a product exists for a family of objects $f : J \to C$, then the biproduct of $f$ also exists.

CategoryTheory.Limits.HasBiproduct.of_hasCoproduct theorem

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

Full source

/-- In a preadditive category, if the coproduct over `f : J → C` exists,
    then the biproduct over `f` exists. -/
theorem HasBiproduct.of_hasCoproduct (f : J → C) [HasCoproduct f] : HasBiproduct f := by
  cases nonempty_fintype J
  exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

Existence of Biproduct from Coproduct in Preadditive Categories

Informal description

Let $\mathcal{C}$ be a preadditive category and $f \colon J \to \mathcal{C}$ a family of objects in $\mathcal{C}$. If the coproduct $\coprod_{j \in J} f(j)$ exists in $\mathcal{C}$, then the biproduct $\bigoplus_{j \in J} f(j)$ exists as well.

CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts theorem

[HasFiniteProducts C] : HasFiniteBiproducts C

Full source

/-- A preadditive category with finite products has finite biproducts. -/
theorem HasFiniteBiproducts.of_hasFiniteProducts [HasFiniteProducts C] : HasFiniteBiproducts C :=
  ⟨fun _ => { has_biproduct := fun _ => HasBiproduct.of_hasProduct _ }⟩

Finite Biproducts from Finite Products in Preadditive Categories

Informal description

In a preadditive category $\mathcal{C}$ with finite products, $\mathcal{C}$ also has finite biproducts.

CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts theorem

[HasFiniteCoproducts C] : HasFiniteBiproducts C

Full source

/-- A preadditive category with finite coproducts has finite biproducts. -/
theorem HasFiniteBiproducts.of_hasFiniteCoproducts [HasFiniteCoproducts C] :
    HasFiniteBiproducts C :=
  ⟨fun _ => { has_biproduct := fun _ => HasBiproduct.of_hasCoproduct _ }⟩

Finite Biproducts from Finite Coproducts in Preadditive Categories

Informal description

In a preadditive category $\mathcal{C}$ with finite coproducts, $\mathcal{C}$ has finite biproducts.

CategoryTheory.Limits.biproduct.total theorem

: ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)

Full source

/-- In any preadditive category, any biproduct satisfies
`∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)`
-/
@[simp]
theorem biproduct.total : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f) :=
  IsBilimit.total (biproduct.isBilimit _)

Biproduct Total Morphism Identity in Preadditive Categories

Informal description

In a preadditive category $\mathcal{C}$ with a finite index set $J$ and a family of objects $f : J \to \mathcal{C}$, the sum over $j \in J$ of the compositions of the projection $\pi_j : \bigoplus f \to f_j$ and inclusion $\iota_j : f_j \to \bigoplus f$ morphisms equals the identity morphism on the biproduct object: \[ \sum_{j \in J} \pi_j \circ \iota_j = \mathrm{id}_{\bigoplus f}. \]

CategoryTheory.Limits.biproduct.lift_eq theorem

{T : C} {g : ∀ j, T ⟶ f j} : biproduct.lift g = ∑ j, g j ≫ biproduct.ι f j

Full source

theorem biproduct.lift_eq {T : C} {g : ∀ j, T ⟶ f j} :
    biproduct.lift g = ∑ j, g j ≫ biproduct.ι f j := by
  classical
  ext j
  simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]

Biproduct Lift as Sum of Compositions with Inclusions

Informal description

Let $\mathcal{C}$ be a preadditive category with a family of objects $f : J \to \mathcal{C}$ that has a biproduct $\bigoplus f$. For any object $T$ in $\mathcal{C}$ and any family of morphisms $g_j : T \to f(j)$ for each $j \in J$, the morphism $\text{biproduct.lift}\, g : T \to \bigoplus f$ is equal to the sum over $j$ of the compositions $g_j \circ \iota_j$, where $\iota_j : f(j) \to \bigoplus f$ is the inclusion morphism. That is, \[ \text{biproduct.lift}\, g = \sum_{j \in J} g_j \circ \iota_j. \]

CategoryTheory.Limits.biproduct.desc_eq theorem

{T : C} {g : ∀ j, f j ⟶ T} : biproduct.desc g = ∑ j, biproduct.π f j ≫ g j

Full source

theorem biproduct.desc_eq {T : C} {g : ∀ j, f j ⟶ T} :
    biproduct.desc g = ∑ j, biproduct.π f j ≫ g j := by
  classical
  ext j
  simp [comp_sum, biproduct.ι_π_assoc, dite_comp]

Decomposition of Biproduct Descending Morphism into Component Projections

Informal description

Let $\mathcal{C}$ be a preadditive category with biproducts, and let $f : J \to \mathcal{C}$ be a family of objects indexed by a finite set $J$. For any object $T$ in $\mathcal{C}$ and any collection of morphisms $g_j : f(j) \to T$ for $j \in J$, the descending morphism $\text{desc } g : \bigoplus f \to T$ satisfies the equality: \[ \text{desc } g = \sum_{j \in J} \pi_j \circ g_j, \] where $\pi_j : \bigoplus f \to f(j)$ is the projection morphism from the biproduct to its $j$-th component.

CategoryTheory.Limits.biproduct.lift_desc theorem

 {T U : C} {g : ∀ j, T ⟶ f j} {h : ∀ j, f j ⟶ U} : biproduct.lift g ≫ biproduct.desc h = ∑ j : J, g j ≫ h j

Full source

@[reassoc]
theorem biproduct.lift_desc {T U : C} {g : ∀ j, T ⟶ f j} {h : ∀ j, f j ⟶ U} :
    biproduct.liftbiproduct.lift g ≫ biproduct.desc h = ∑ j : J, g j ≫ h j := by
  classical
  simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
    dite_comp]

Composition of Biproduct Lift and Descend Equals Sum of Component Compositions

Informal description

Let $\mathcal{C}$ be a preadditive category with biproducts, and let $f : J \to \mathcal{C}$ be a family of objects indexed by a finite set $J$. For any objects $T, U$ in $\mathcal{C}$ and families of morphisms $g_j : T \to f(j)$ and $h_j : f(j) \to U$ for each $j \in J$, the composition of the lifted morphism $\text{lift}\, g : T \to \bigoplus f$ with the descending morphism $\text{desc}\, h : \bigoplus f \to U$ equals the sum over $j \in J$ of the compositions $g_j \circ h_j$. That is, \[ \text{lift}\, g \circ \text{desc}\, h = \sum_{j \in J} g_j \circ h_j. \]

CategoryTheory.Limits.biproduct.map_eq theorem

 [HasFiniteBiproducts C] {f g : J → C} {h : ∀ j, f j ⟶ g j} :
  biproduct.map h = ∑ j : J, biproduct.π f j ≫ h j ≫ biproduct.ι g j

Full source

theorem biproduct.map_eq [HasFiniteBiproducts C] {f g : J → C} {h : ∀ j, f j ⟶ g j} :
    biproduct.map h = ∑ j : J, biproduct.π f j ≫ h j ≫ biproduct.ι g j := by
  classical
  ext
  simp [biproduct.ι_π, biproduct.ι_π_assoc, comp_sum, sum_comp, comp_dite, dite_comp]

Decomposition of Biproduct Map via Projections and Inclusions

Informal description

Let $\mathcal{C}$ be a preadditive category with finite biproducts, and let $f, g : J \to \mathcal{C}$ be two families of objects indexed by a finite set $J$. For any collection of morphisms $h_j : f(j) \to g(j)$, the induced morphism $\text{biproduct.map } h : \bigoplus f \to \bigoplus g$ can be expressed as the sum over $j \in J$ of the compositions $\pi_j \circ h_j \circ \iota_j$, where $\pi_j : \bigoplus f \to f(j)$ is the projection and $\iota_j : g(j) \to \bigoplus g$ is the inclusion. That is, \[ \text{biproduct.map } h = \sum_{j \in J} \pi_j \circ h_j \circ \iota_j. \]

CategoryTheory.Limits.biproduct.lift_matrix theorem

 {K : Type} [Finite K] [HasFiniteBiproducts C] {f : J → C} {g : K → C} {P} (x : ∀ j, P ⟶ f j) (m : ∀ j k, f j ⟶ g k) :
  biproduct.lift x ≫ biproduct.matrix m = biproduct.lift fun k => ∑ j, x j ≫ m j k

Full source

@[reassoc]
theorem biproduct.lift_matrix {K : Type} [Finite K] [HasFiniteBiproducts C] {f : J → C} {g : K → C}
    {P} (x : ∀ j, P ⟶ f j) (m : ∀ j k, f j ⟶ g k) :
    biproduct.liftbiproduct.lift x ≫ biproduct.matrix m = biproduct.lift fun k => ∑ j, x j ≫ m j k := by
  ext
  simp [biproduct.lift_desc]

Composition of Biproduct Lift and Matrix Morphism Equals Lift of Summed Compositions

Informal description

Let $\mathcal{C}$ be a preadditive category with finite biproducts, and let $f : J \to \mathcal{C}$ and $g : K \to \mathcal{C}$ be families of objects indexed by finite sets $J$ and $K$. For any object $P$ in $\mathcal{C}$, any family of morphisms $x_j : P \to f(j)$, and any matrix of morphisms $m_{j,k} : f(j) \to g(k)$, the composition of the lifted morphism $\text{lift}\, x : P \to \bigoplus f$ with the matrix-induced morphism $\text{matrix}\, m : \bigoplus f \to \bigoplus g$ equals the lifted morphism $\text{lift}\, \left(\sum_j x_j \circ m_{j,k}\right)_k : P \to \bigoplus g$. That is, \[ \text{lift}\, x \circ \text{matrix}\, m = \text{lift}\, \left(\sum_j x_j \circ m_{j,k}\right)_k. \]

CategoryTheory.Limits.biproduct.matrix_desc theorem

 [Fintype K] {f : J → C} {g : K → C} (m : ∀ j k, f j ⟶ g k) {P} (x : ∀ k, g k ⟶ P) :
  biproduct.matrix m ≫ biproduct.desc x = biproduct.desc fun j => ∑ k, m j k ≫ x k

Full source

@[reassoc]
theorem biproduct.matrix_desc [Fintype K] {f : J → C} {g : K → C}
    (m : ∀ j k, f j ⟶ g k) {P} (x : ∀ k, g k ⟶ P) :
    biproduct.matrixbiproduct.matrix m ≫ biproduct.desc x = biproduct.desc fun j => ∑ k, m j k ≫ x k := by
  ext
  simp [lift_desc]

Composition of Matrix-Induced Morphism with Descending Morphism in Biproducts

Informal description

Let $\mathcal{C}$ be a preadditive category with biproducts, and let $f : J \to \mathcal{C}$ and $g : K \to \mathcal{C}$ be families of objects indexed by finite sets $J$ and $K$ respectively. Given a matrix of morphisms $m_{jk} : f(j) \to g(k)$ for each $j \in J$ and $k \in K$, and a family of morphisms $x_k : g(k) \to P$ for some object $P$ in $\mathcal{C}$, the composition of the matrix-induced morphism $\text{biproduct.matrix}\, m : \bigoplus f \to \bigoplus g$ with the descending morphism $\text{biproduct.desc}\, x : \bigoplus g \to P$ equals the descending morphism induced by the family of morphisms $\sum_k m_{jk} \circ x_k : f(j) \to P$ for each $j \in J$. That is, \[ \text{biproduct.matrix}\, m \circ \text{biproduct.desc}\, x = \text{biproduct.desc}\, \left(\lambda j. \sum_k m_{jk} \circ x_k\right). \]

CategoryTheory.Limits.biproduct.matrix_map theorem

 {f : J → C} {g : K → C} {h : K → C} (m : ∀ j k, f j ⟶ g k) (n : ∀ k, g k ⟶ h k) :
  biproduct.matrix m ≫ biproduct.map n = biproduct.matrix fun j k => m j k ≫ n k

Full source

@[reassoc]
theorem biproduct.matrix_map {f : J → C} {g : K → C} {h : K → C} (m : ∀ j k, f j ⟶ g k)
    (n : ∀ k, g k ⟶ h k) :
    biproduct.matrixbiproduct.matrix m ≫ biproduct.map n = biproduct.matrix fun j k => m j k ≫ n k := by
  ext
  simp

Composition of Matrix-Induced Morphism with Component-Wise Morphism

Informal description

Let $C$ be a preadditive category with biproducts, and let $f : J \to C$, $g : K \to C$, and $h : K \to C$ be families of objects in $C$. Given a matrix of morphisms $m_{j,k} : f(j) \to g(k)$ for each $j \in J$ and $k \in K$, and a family of morphisms $n_k : g(k) \to h(k)$ for each $k \in K$, the composition of the matrix-induced morphism $\text{biproduct.matrix}\, m : \bigoplus f \to \bigoplus g$ with the component-wise morphism $\text{biproduct.map}\, n : \bigoplus g \to \bigoplus h$ equals the matrix-induced morphism $\text{biproduct.matrix}\, (m_{j,k} \circ n_k) : \bigoplus f \to \bigoplus h$. In symbols: \[ \text{biproduct.matrix}\, m \circ \text{biproduct.map}\, n = \text{biproduct.matrix}\, (m_{j,k} \circ n_k). \]

CategoryTheory.Limits.biproduct.map_matrix theorem

 {f : J → C} {g : J → C} {h : K → C} (m : ∀ k, f k ⟶ g k) (n : ∀ j k, g j ⟶ h k) :
  biproduct.map m ≫ biproduct.matrix n = biproduct.matrix fun j k => m j ≫ n j k

Full source

@[reassoc]
theorem biproduct.map_matrix {f : J → C} {g : J → C} {h : K → C} (m : ∀ k, f k ⟶ g k)
    (n : ∀ j k, g j ⟶ h k) :
    biproduct.mapbiproduct.map m ≫ biproduct.matrix n = biproduct.matrix fun j k => m j ≫ n j k := by
  ext
  simp

Composition of Biproduct Map with Matrix Morphism Equals Matrix of Compositions

Informal description

Let $C$ be a preadditive category with biproducts, and let $f, g : J \to C$ and $h : K \to C$ be families of objects in $C$. Given a family of morphisms $m_k : f(k) \to g(k)$ for each $k \in J$ and a matrix of morphisms $n_{j,k} : g(j) \to h(k)$ for each $j \in J$ and $k \in K$, the composition of the induced morphism $\bigoplus f \to \bigoplus g$ with the matrix-induced morphism $\bigoplus g \to \bigoplus h$ equals the matrix-induced morphism $\bigoplus f \to \bigoplus h$ whose $(j,k)$-entry is $m_j \circ n_{j,k}$. In symbols: \[ \text{biproduct.map } m \circ \text{biproduct.matrix } n = \text{biproduct.matrix } (m_j \circ n_{j,k})_{j,k} \]

CategoryTheory.Limits.biproduct.reindex definition

 {β γ : Type} [Finite β] (ε : β ≃ γ) (f : γ → C) [HasBiproduct f] [HasBiproduct (f ∘ ε)] : ⨁ f ∘ ε ≅ ⨁ f

Full source

/-- Reindex a categorical biproduct via an equivalence of the index types. -/
@[simps]
def biproduct.reindex {β γ : Type} [Finite β] (ε : β ≃ γ)
    (f : γ → C) [HasBiproduct f] [HasBiproduct (f ∘ ε)] : ⨁ f ∘ ε⨁ f ∘ ε ≅ ⨁ f where
  hom := biproduct.desc fun b => biproduct.ι f (ε b)
  inv := biproduct.lift fun b => biproduct.π f (ε b)
  hom_inv_id := by
    ext b b'
    by_cases h : b' = b
    · subst h; simp
    · have : ε b' ≠ ε b := by simp [h]
      simp [biproduct.ι_π_ne _ h, biproduct.ι_π_ne _ this]
  inv_hom_id := by
    classical
    cases nonempty_fintype β
    ext g g'
    by_cases h : g' = g <;>
      simp [Preadditive.sum_comp, Preadditive.comp_sum, biproduct.lift_desc,
        biproduct.ι_π, biproduct.ι_π_assoc, comp_dite, Equiv.apply_eq_iff_eq_symm_apply,
        Finset.sum_dite_eq' Finset.univ (ε.symm g') _, h]

Reindexing isomorphism for biproducts via type equivalence

Informal description

Given a finite index type $\beta$ and an equivalence $\varepsilon : \beta \simeq \gamma$ between $\beta$ and another type $\gamma$, and a family of objects $f : \gamma \to C$ in a preadditive category $C$ with biproducts, there is an isomorphism between the biproduct $\bigoplus (f \circ \varepsilon)$ indexed by $\beta$ and the biproduct $\bigoplus f$ indexed by $\gamma$. The isomorphism is constructed using the universal properties of the biproducts: the forward morphism is induced by the inclusions $\iota_{\varepsilon(b)} : f(\varepsilon(b)) \to \bigoplus f$ for each $b \in \beta$, and the inverse morphism is induced by the projections $\pi_{\varepsilon(b)} : \bigoplus f \to f(\varepsilon(b))$ for each $b \in \beta$.

CategoryTheory.Limits.isBinaryBilimitOfTotal definition

{X Y : C} (b : BinaryBicone X Y) (total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt) : b.IsBilimit

Full source

/-- In a preadditive category, we can construct a binary biproduct for `X Y : C` from
any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
-/
def isBinaryBilimitOfTotal {X Y : C} (b : BinaryBicone X Y)
    (total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt) : b.IsBilimit where
  isLimit :=
    { lift := fun s =>
      (BinaryFan.fstBinaryFan.fst s ≫ b.inl : s.pt ⟶ b.pt) + (BinaryFan.sndBinaryFan.snd s ≫ b.inr : s.pt ⟶ b.pt)
      uniq := fun s m h => by
        have reassoced (j : WalkingPair) {W : C} (h' : _ ⟶ W) :
          m ≫ b.toCone.π.app ⟨j⟩ ≫ h' = s.π.app ⟨j⟩ ≫ h' := by
            rw [← Category.assoc, eq_whisker (h ⟨j⟩)]
        erw [← Category.comp_id m, ← total, comp_add, reassoced WalkingPair.left,
          reassoced WalkingPair.right]
      fac := fun s j => by rcases j with ⟨⟨⟩⟩ <;> simp }
  isColimit :=
    { desc := fun s =>
        (b.fst ≫ BinaryCofan.inl s : b.pt ⟶ s.pt) + (b.snd ≫ BinaryCofan.inr s : b.pt ⟶ s.pt)
      uniq := fun s m h => by
        erw [← Category.id_comp m, ← total, add_comp, Category.assoc, Category.assoc,
          h ⟨WalkingPair.left⟩, h ⟨WalkingPair.right⟩]
      fac := fun s j => by rcases j with ⟨⟨⟩⟩ <;> simp }

Bilimit bicone from total morphism condition

Informal description

Given a binary bicone $b$ for objects $X$ and $Y$ in a preadditive category $C$, if the morphisms satisfy the equation $b.\text{fst} \circ b.\text{inl} + b.\text{snd} \circ b.\text{inr} = \mathbb{1}_{b.X}$, then $b$ is a bilimit bicone. This means that $b$ is both a limit cone and a colimit cocone for the pair $(X, Y)$.

CategoryTheory.Limits.IsBilimit.binary_total theorem

{X Y : C} {b : BinaryBicone X Y} (i : b.IsBilimit) : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt

Full source

theorem IsBilimit.binary_total {X Y : C} {b : BinaryBicone X Y} (i : b.IsBilimit) :
    b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt :=
  i.isLimit.hom_ext fun j => by rcases j with ⟨⟨⟩⟩ <;> simp

Biproduct Total Morphism Identity for Binary Bilimits

Informal description

For any binary bicone $b$ of objects $X$ and $Y$ in a preadditive category $C$, if $b$ is a bilimit bicone, then the composition of the first projection with the first inclusion plus the composition of the second projection with the second inclusion equals the identity morphism on the biproduct object, i.e., $$ b_{\text{fst}} \circ b_{\text{inl}} + b_{\text{snd}} \circ b_{\text{inr}} = \mathbb{1}_{b_{\text{pt}}}. $$

CategoryTheory.Limits.hasBinaryBiproduct_of_total theorem

{X Y : C} (b : BinaryBicone X Y) (total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt) : HasBinaryBiproduct X Y

Full source

/-- In a preadditive category, we can construct a binary biproduct for `X Y : C` from
any binary bicone `b` satisfying `total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.X`.

(That is, such a bicone is a limit cone and a colimit cocone.)
-/
theorem hasBinaryBiproduct_of_total {X Y : C} (b : BinaryBicone X Y)
    (total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt) : HasBinaryBiproduct X Y :=
  HasBinaryBiproduct.mk
    { bicone := b
      isBilimit := isBinaryBilimitOfTotal b total }

Existence of Binary Biproduct from Total Morphism Condition in Preadditive Categories

Informal description

Let $C$ be a preadditive category, and let $X, Y$ be objects in $C$. Given a binary bicone $b$ for $X$ and $Y$ such that the morphisms satisfy the equation $b_{\text{fst}} \circ b_{\text{inl}} + b_{\text{snd}} \circ b_{\text{inr}} = \mathbb{1}_{b_{\text{pt}}}$, then $X$ and $Y$ have a binary biproduct.

CategoryTheory.Limits.BinaryBicone.ofLimitCone definition

{X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : BinaryBicone X Y

Full source

/-- We can turn any limit cone over a pair into a bicone. -/
@[simps]
def BinaryBicone.ofLimitCone {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) :
    BinaryBicone X Y where
  pt := t.pt
  fst := t.π.app ⟨WalkingPair.left⟩
  snd := t.π.app ⟨WalkingPair.right⟩
  inl := ht.lift (BinaryFan.mk (𝟙 X) 0)
  inr := ht.lift (BinaryFan.mk 0 (𝟙 Y))

Binary bicone from a limit cone

Informal description

Given a limit cone $ t $ over the pair of objects $ X $ and $ Y $ in a preadditive category $ C $, the function constructs a binary bicone with: - The cone point $ t.\mathrm{pt} $, - The projection maps $ t.\pi.\mathrm{left} $ and $ t.\pi.\mathrm{right} $ as the first and second projections, - The inclusion maps obtained by lifting the identity morphisms on $ X $ and $ Y $ through the limit property of $ t $.

CategoryTheory.Limits.inl_of_isLimit theorem

{X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) : t.inl = ht.lift (BinaryFan.mk (𝟙 X) 0)

Full source

theorem inl_of_isLimit {X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) :
    t.inl = ht.lift (BinaryFan.mk (𝟙 X) 0) := by
  apply ht.uniq (BinaryFan.mk (𝟙 X) 0); rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

Characterization of Left Inclusion in Limit Binary Bicone

Informal description

Let $X$ and $Y$ be objects in a preadditive category $C$, and let $t$ be a binary bicone for $X$ and $Y$. If the cone structure of $t$ is a limit cone, then the left inclusion morphism $t.\mathrm{inl}$ is equal to the lift of the binary fan $(1_X, 0)$, where $1_X$ is the identity morphism on $X$ and $0$ is the zero morphism from $X$ to $Y$.

CategoryTheory.Limits.inr_of_isLimit theorem

{X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) : t.inr = ht.lift (BinaryFan.mk 0 (𝟙 Y))

Full source

theorem inr_of_isLimit {X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) :
    t.inr = ht.lift (BinaryFan.mk 0 (𝟙 Y)) := by
  apply ht.uniq (BinaryFan.mk 0 (𝟙 Y)); rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

Right Inclusion Morphism in Limit Binary Bicone Equals Lift of Zero-Identity Fan

Informal description

Let $C$ be a preadditive category, and let $X$ and $Y$ be objects in $C$. Given a binary bicone $t$ for $X$ and $Y$ such that the underlying cone $t.\text{toCone}$ is a limit cone, the right inclusion morphism $t.\text{inr}$ is equal to the unique morphism induced by the limit property of $t.\text{toCone}$ applied to the binary fan $(0, \text{id}_Y)$. That is, $t.\text{inr} = \text{ht.lift} (\text{BinaryFan.mk}\,0\,\text{id}_Y)$.

CategoryTheory.Limits.isBinaryBilimitOfIsLimit definition

{X Y : C} (t : BinaryBicone X Y) (ht : IsLimit t.toCone) : t.IsBilimit

Full source

/-- In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit
    bicone. -/
def isBinaryBilimitOfIsLimit {X Y : C} (t : BinaryBicone X Y) (ht : IsLimit t.toCone) :
    t.IsBilimit :=
  isBinaryBilimitOfTotal _ (by refine BinaryFan.IsLimit.hom_ext ht ?_ ?_ <;> simp)

Limit cone implies bilimit bicone in preadditive categories

Informal description

Given a binary bicone $ t $ for objects $ X $ and $ Y $ in a preadditive category $ C $, if the underlying cone $ t.\text{toCone} $ is a limit cone, then $ t $ is a bilimit bicone. This means that $ t $ is both a limit cone and a colimit cocone for the pair $ (X, Y) $.

CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit definition

{X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : (BinaryBicone.ofLimitCone ht).IsBilimit

Full source

/-- We can turn any limit cone over a pair into a bilimit bicone. -/
def binaryBiconeIsBilimitOfLimitConeOfIsLimit {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) :
    (BinaryBicone.ofLimitCone ht).IsBilimit :=
  isBinaryBilimitOfTotal _ <| BinaryFan.IsLimit.hom_ext ht (by simp) (by simp)

Bilimit bicone from limit cone

Informal description

Given a limit cone $ t $ over the pair of objects $ X $ and $ Y $ in a preadditive category $ C $, the binary bicone constructed from $ t $ is a bilimit bicone. This means that the bicone is both a limit cone and a colimit cocone for the pair $ (X, Y) $.

CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct theorem

(X Y : C) [HasBinaryProduct X Y] : HasBinaryBiproduct X Y

Full source

/-- In a preadditive category, if the product of `X` and `Y` exists, then the
    binary biproduct of `X` and `Y` exists. -/
theorem HasBinaryBiproduct.of_hasBinaryProduct (X Y : C) [HasBinaryProduct X Y] :
    HasBinaryBiproduct X Y :=
  HasBinaryBiproduct.mk
    { bicone := _
      isBilimit := binaryBiconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

Existence of Binary Biproduct from Binary Product in Preadditive Categories

Informal description

In a preadditive category, if the binary product of objects $X$ and $Y$ exists, then the binary biproduct of $X$ and $Y$ also exists.

CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts theorem

[HasBinaryProducts C] : HasBinaryBiproducts C

Full source

/-- In a preadditive category, if all binary products exist, then all binary biproducts exist. -/
theorem HasBinaryBiproducts.of_hasBinaryProducts [HasBinaryProducts C] : HasBinaryBiproducts C :=
  { has_binary_biproduct := fun X Y => HasBinaryBiproduct.of_hasBinaryProduct X Y }

Existence of Binary Biproducts from Binary Products in Preadditive Categories

Informal description

In a preadditive category $\mathcal{C}$, if all binary products exist, then all binary biproducts exist.

CategoryTheory.Limits.BinaryBicone.ofColimitCocone definition

{X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : BinaryBicone X Y

Full source

/-- We can turn any colimit cocone over a pair into a bicone. -/
@[simps]
def BinaryBicone.ofColimitCocone {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) :
    BinaryBicone X Y where
  pt := t.pt
  fst := ht.desc (BinaryCofan.mk (𝟙 X) 0)
  snd := ht.desc (BinaryCofan.mk 0 (𝟙 Y))
  inl := t.ι.app ⟨WalkingPair.left⟩
  inr := t.ι.app ⟨WalkingPair.right⟩

Binary bicone from a colimit cocone

Informal description

Given a colimit cocone `t` over the pair `(X, Y)` in a preadditive category `C`, the function constructs a binary bicone with: - The point `t.pt` as the biproduct object - The projections `fst` and `snd` defined via the universal property of the colimit - The inclusions `inl` and `inr` given by the cocone's natural transformation components

CategoryTheory.Limits.fst_of_isColimit theorem

{X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) : t.fst = ht.desc (BinaryCofan.mk (𝟙 X) 0)

Full source

theorem fst_of_isColimit {X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) :
    t.fst = ht.desc (BinaryCofan.mk (𝟙 X) 0) := by
  apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)
  rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

First Projection of a Biproduct from Colimit Universal Property

Informal description

Let $C$ be a preadditive category, and let $X, Y$ be objects in $C$. Given a binary biproduct bicone $t$ for $X$ and $Y$, if the cocone associated to $t$ is a colimit cocone, then the first projection morphism $t_{\text{fst}}$ satisfies \[ t_{\text{fst}} = \text{ht.desc}(\text{BinaryCofan.mk}(1_X, 0)), \] where $\text{ht.desc}$ is the unique morphism induced by the universal property of the colimit, and $\text{BinaryCofan.mk}(1_X, 0)$ is the binary cofan with the identity morphism on $X$ and the zero morphism from $X$ to $Y$.

CategoryTheory.Limits.snd_of_isColimit theorem

{X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) : t.snd = ht.desc (BinaryCofan.mk 0 (𝟙 Y))

Full source

theorem snd_of_isColimit {X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) :
    t.snd = ht.desc (BinaryCofan.mk 0 (𝟙 Y)) := by
  apply ht.uniq (BinaryCofan.mk 0 (𝟙 Y))
  rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

Second Projection of Biproduct via Colimit Property

Informal description

Let $C$ be a preadditive category, and let $X$ and $Y$ be objects in $C$. Given a binary bicone $t$ for $X$ and $Y$ such that the cocone $t.\text{toCocone}$ is a colimit cocone, the second projection morphism $t.\text{snd}$ is equal to the unique morphism induced by the colimit property, applied to the binary cofan with morphisms $0 \colon X \to Y$ and $\text{id}_Y \colon Y \to Y$.

CategoryTheory.Limits.isBinaryBilimitOfIsColimit definition

{X Y : C} (t : BinaryBicone X Y) (ht : IsColimit t.toCocone) : t.IsBilimit

Full source

/-- In a preadditive category, any binary bicone which is a colimit cocone is in fact a
    bilimit bicone. -/
def isBinaryBilimitOfIsColimit {X Y : C} (t : BinaryBicone X Y) (ht : IsColimit t.toCocone) :
    t.IsBilimit :=
  isBinaryBilimitOfTotal _ <| by
    refine BinaryCofan.IsColimit.hom_ext ht ?_ ?_ <;> simp

Bilimit bicone from colimit cocone condition

Informal description

Given a binary bicone $t$ for objects $X$ and $Y$ in a preadditive category $C$, if the cocone associated to $t$ is a colimit cocone, then $t$ is a bilimit bicone. This means that $t$ is both a limit cone and a colimit cocone for the pair $(X, Y)$.

CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimit definition

{X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : (BinaryBicone.ofColimitCocone ht).IsBilimit

Full source

/-- We can turn any colimit cocone over a pair into a bilimit bicone. -/
def binaryBiconeIsBilimitOfColimitCoconeOfIsColimit {X Y : C} {t : Cocone (pair X Y)}
    (ht : IsColimit t) : (BinaryBicone.ofColimitCocone ht).IsBilimit :=
  isBinaryBilimitOfIsColimit (BinaryBicone.ofColimitCocone ht) <|
    IsColimit.ofIsoColimit ht <|
      Cocones.ext (Iso.refl _) fun j => by
        rcases j with ⟨⟨⟩⟩ <;> simp

Bilimit bicone from colimit cocone

Informal description

Given a colimit cocone $ t $ over the pair of objects $ (X, Y) $ in a preadditive category $ C $, the binary bicone constructed from $ t $ is a bilimit bicone. This means that the bicone is both a limit cone and a colimit cocone for $ (X, Y) $.

CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct theorem

(X Y : C) [HasBinaryCoproduct X Y] : HasBinaryBiproduct X Y

Full source

/-- In a preadditive category, if the coproduct of `X` and `Y` exists, then the
    binary biproduct of `X` and `Y` exists. -/
theorem HasBinaryBiproduct.of_hasBinaryCoproduct (X Y : C) [HasBinaryCoproduct X Y] :
    HasBinaryBiproduct X Y :=
  HasBinaryBiproduct.mk
    { bicone := _
      isBilimit := binaryBiconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

Existence of Binary Biproduct from Binary Coproduct in Preadditive Categories

Informal description

In a preadditive category $C$, if the binary coproduct of objects $X$ and $Y$ exists, then the binary biproduct of $X$ and $Y$ also exists.

CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts theorem

[HasBinaryCoproducts C] : HasBinaryBiproducts C

Full source

/-- In a preadditive category, if all binary coproducts exist, then all binary biproducts exist. -/
theorem HasBinaryBiproducts.of_hasBinaryCoproducts [HasBinaryCoproducts C] :
    HasBinaryBiproducts C :=
  { has_binary_biproduct := fun X Y => HasBinaryBiproduct.of_hasBinaryCoproduct X Y }

Existence of Binary Biproducts from Binary Coproducts in Preadditive Categories

Informal description

In a preadditive category $C$, if all binary coproducts exist, then all binary biproducts exist.

CategoryTheory.Limits.biprod.total theorem

: biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)

Full source

/-- In any preadditive category, any binary biproduct satisfies
`biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)`.
-/
@[simp]
theorem biprod.total : biprod.fstbiprod.fst ≫ biprod.inl + biprod.sndbiprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y) := by
  ext <;> simp [add_comp]

Biproduct Total Morphism Identity in Preadditive Categories

Informal description

In any preadditive category with binary biproducts, for objects $X$ and $Y$, the composition of the first projection with the first inclusion plus the composition of the second projection with the second inclusion equals the identity morphism on the biproduct $X \oplus Y$. That is, \[ \pi_1 \circ \iota_1 + \pi_2 \circ \iota_2 = \text{id}_{X \oplus Y}, \] where $\pi_1$ and $\pi_2$ are the projections from $X \oplus Y$ to $X$ and $Y$ respectively, and $\iota_1$ and $\iota_2$ are the inclusions from $X$ and $Y$ to $X \oplus Y$ respectively.

CategoryTheory.Limits.biprod.lift_eq theorem

{T : C} {f : T ⟶ X} {g : T ⟶ Y} : biprod.lift f g = f ≫ biprod.inl + g ≫ biprod.inr

Full source

theorem biprod.lift_eq {T : C} {f : T ⟶ X} {g : T ⟶ Y} :
    biprod.lift f g = f ≫ biprod.inl + g ≫ biprod.inr := by ext <;> simp [add_comp]

Decomposition of Biproduct Lift Morphism in Preadditive Categories

Informal description

In a preadditive category $C$ with binary biproducts, for any object $T$ and morphisms $f \colon T \to X$ and $g \colon T \to Y$, the biproduct morphism $\text{biprod.lift}\, f\, g$ is equal to the sum of the compositions $f \circ \text{biprod.inl}$ and $g \circ \text{biprod.inr}$, i.e., \[ \text{biprod.lift}\, f\, g = f \circ \iota_1 + g \circ \iota_2, \] where $\iota_1 \colon X \to X \oplus Y$ and $\iota_2 \colon Y \to X \oplus Y$ are the inclusion morphisms into the biproduct $X \oplus Y$.

CategoryTheory.Limits.biprod.desc_eq theorem

{T : C} {f : X ⟶ T} {g : Y ⟶ T} : biprod.desc f g = biprod.fst ≫ f + biprod.snd ≫ g

Full source

theorem biprod.desc_eq {T : C} {f : X ⟶ T} {g : Y ⟶ T} :
    biprod.desc f g = biprod.fstbiprod.fst ≫ f + biprod.sndbiprod.snd ≫ g := by ext <;> simp [add_comp]

Biproduct Descend Morphism Decomposition in Preadditive Categories

Informal description

In a preadditive category $C$ with binary biproducts, for any object $T$ and morphisms $f \colon X \to T$ and $g \colon Y \to T$, the biproduct morphism $\text{biprod.desc}\, f\, g$ is equal to the sum of the compositions $\text{biprod.fst} \circ f$ and $\text{biprod.snd} \circ g$, i.e., \[ \text{biprod.desc}\, f\, g = \text{biprod.fst} \circ f + \text{biprod.snd} \circ g. \]

CategoryTheory.Limits.biprod.lift_desc theorem

 {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U} : biprod.lift f g ≫ biprod.desc h i = f ≫ h + g ≫ i

Full source

@[reassoc (attr := simp)]
theorem biprod.lift_desc {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U} :
    biprod.liftbiprod.lift f g ≫ biprod.desc h i = f ≫ h + g ≫ i := by simp [biprod.lift_eq, biprod.desc_eq]

Composition of Biproduct Lift and Descend Morphisms Equals Sum of Compositions

Informal description

In a preadditive category $C$ with binary biproducts, for any objects $T, U, X, Y$ and morphisms $f \colon T \to X$, $g \colon T \to Y$, $h \colon X \to U$, and $i \colon Y \to U$, the composition of the biproduct lift morphism $\text{biprod.lift}\, f\, g$ with the biproduct descend morphism $\text{biprod.desc}\, h\, i$ equals the sum of the compositions $f \circ h$ and $g \circ i$, i.e., \[ \text{biprod.lift}\, f\, g \circ \text{biprod.desc}\, h\, i = f \circ h + g \circ i. \]

CategoryTheory.Limits.biprod.map_eq theorem

 [HasBinaryBiproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z} :
  biprod.map f g = biprod.fst ≫ f ≫ biprod.inl + biprod.snd ≫ g ≫ biprod.inr

Full source

theorem biprod.map_eq [HasBinaryBiproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z} :
    biprod.map f g = biprod.fstbiprod.fst ≫ f ≫ biprod.inl + biprod.sndbiprod.snd ≫ g ≫ biprod.inr := by
  ext <;> simp

Decomposition of Biproduct Map via Projections and Inclusions

Informal description

In a preadditive category $C$ with binary biproducts, for any objects $W, X, Y, Z$ and morphisms $f \colon W \to Y$ and $g \colon X \to Z$, the biproduct morphism $\text{biprod.map}\, f\, g$ can be expressed as: \[ \text{biprod.map}\, f\, g = \pi_1 \circ f \circ \iota_1 + \pi_2 \circ g \circ \iota_2, \] where $\pi_1 \colon W \oplus X \to W$ and $\pi_2 \colon W \oplus X \to X$ are the canonical projections, and $\iota_1 \colon Y \to Y \oplus Z$ and $\iota_2 \colon Z \to Y \oplus Z$ are the canonical inclusions.

CategoryTheory.Limits.biprod.decomp_hom_to theorem

(f : Z ⟶ X ⊞ Y) : ∃ f₁ f₂, f = f₁ ≫ biprod.inl + f₂ ≫ biprod.inr

Full source

lemma biprod.decomp_hom_to (f : Z ⟶ X ⊞ Y) :
    ∃ f₁ f₂, f = f₁ ≫ biprod.inl + f₂ ≫ biprod.inr :=
  ⟨f ≫ biprod.fst, f ≫ biprod.snd, by aesop⟩

Decomposition of Morphisms into a Biproduct in Preadditive Categories

Informal description

For any morphism $f \colon Z \to X \oplus Y$ in a preadditive category with biproducts, there exist morphisms $f_1 \colon Z \to X$ and $f_2 \colon Z \to Y$ such that $f$ can be decomposed as $f = f_1 \circ \iota_1 + f_2 \circ \iota_2$, where $\iota_1 \colon X \to X \oplus Y$ and $\iota_2 \colon Y \to X \oplus Y$ are the canonical inclusions.

CategoryTheory.Limits.biprod.ext_to_iff theorem

{f g : Z ⟶ X ⊞ Y} : f = g ↔ f ≫ biprod.fst = g ≫ biprod.fst ∧ f ≫ biprod.snd = g ≫ biprod.snd

Full source

lemma biprod.ext_to_iff {f g : Z ⟶ X ⊞ Y} :
    f = g ↔ f ≫ biprod.fst = g ≫ biprod.fst ∧ f ≫ biprod.snd = g ≫ biprod.snd := by
  aesop

Equality of Morphisms into Biproduct via Projections

Informal description

For any two morphisms $f, g \colon Z \to X \oplus Y$ in a preadditive category with biproducts, $f = g$ if and only if both $f \circ \pi_1 = g \circ \pi_1$ and $f \circ \pi_2 = g \circ \pi_2$, where $\pi_1 \colon X \oplus Y \to X$ and $\pi_2 \colon X \oplus Y \to Y$ are the canonical projections.

CategoryTheory.Limits.biprod.decomp_hom_from theorem

(f : X ⊞ Y ⟶ Z) : ∃ f₁ f₂, f = biprod.fst ≫ f₁ + biprod.snd ≫ f₂

Full source

lemma biprod.decomp_hom_from (f : X ⊞ YX ⊞ Y ⟶ Z) :
    ∃ f₁ f₂, f = biprod.fst ≫ f₁ + biprod.snd ≫ f₂ :=
  ⟨biprod.inl ≫ f, biprod.inr ≫ f, by aesop⟩

Decomposition of Morphisms from a Biproduct in Preadditive Categories

Informal description

For any morphism $f \colon X \oplus Y \to Z$ in a preadditive category with biproducts, there exist morphisms $f_1 \colon X \to Z$ and $f_2 \colon Y \to Z$ such that $f$ can be decomposed as $f = \pi_1 \circ f_1 + \pi_2 \circ f_2$, where $\pi_1 \colon X \oplus Y \to X$ and $\pi_2 \colon X \oplus Y \to Y$ are the canonical projections.

CategoryTheory.Limits.biprod.ext_from_iff theorem

{f g : X ⊞ Y ⟶ Z} : f = g ↔ biprod.inl ≫ f = biprod.inl ≫ g ∧ biprod.inr ≫ f = biprod.inr ≫ g

Full source

lemma biprod.ext_from_iff {f g : X ⊞ YX ⊞ Y ⟶ Z} :
    f = g ↔ biprod.inl ≫ f = biprod.inl ≫ g ∧ biprod.inr ≫ f = biprod.inr ≫ g := by
  aesop

Equality of Morphisms from Biproduct via Injections

Informal description

For any two morphisms $f, g \colon X \oplus Y \to Z$ in a preadditive category with biproducts, $f = g$ if and only if both $f \circ \iota_1 = g \circ \iota_1$ and $f \circ \iota_2 = g \circ \iota_2$, where $\iota_1 \colon X \to X \oplus Y$ and $\iota_2 \colon Y \to X \oplus Y$ are the canonical injections.

CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel definition

{X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : BinaryBicone X c.pt

Full source

/-- Every split mono `f` with a cokernel induces a binary bicone with `f` as its `inl` and
the cokernel map as its `snd`.
We will show in `is_bilimit_binary_bicone_of_split_mono_of_cokernel` that this binary bicone is in
fact already a biproduct. -/
@[simps]
def binaryBiconeOfIsSplitMonoOfCokernel {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f}
    (i : IsColimit c) : BinaryBicone X c.pt where
  pt := Y
  fst := retraction f
  snd := c.π
  inl := f
  inr :=
    let c' : CokernelCofork (𝟙 Y - (𝟙 Y - retractionretraction f ≫ f)) :=
      CokernelCofork.ofπ (Cofork.π c) (by simp)
    let i' : IsColimit c' := isCokernelEpiComp i (retraction f) (by simp)
    let i'' := isColimitCoforkOfCokernelCofork i'
    (splitEpiOfIdempotentOfIsColimitCofork C (by simp) i'').section_
  inl_fst := by simp
  inl_snd := by simp
  inr_fst := by
    dsimp only
    rw [splitEpiOfIdempotentOfIsColimitCofork_section_,
      isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]
    dsimp only [cokernelCoforkOfCofork_ofπ]
    letI := epi_of_isColimit_cofork i
    apply zero_of_epi_comp c.π
    simp only [sub_comp, comp_sub, Category.comp_id, Category.assoc, IsSplitMono.id, sub_self,
      Cofork.IsColimit.π_desc_assoc, CokernelCofork.π_ofπ, IsSplitMono.id_assoc]
    apply sub_eq_zero_of_eq
    apply Category.id_comp
  inr_snd := by apply SplitEpi.id

Binary bicone from split monomorphism and cokernel cofork

Informal description

Given a split monomorphism $ f \colon X \to Y $ in a preadditive category $ \mathcal{C} $, and a cokernel cofork $ c $ of $ f $ that is a colimit, the binary bicone constructed has: - $ Y $ as its apex, - the retraction of $ f $ as its first projection, - the cofork projection $ \pi_c \colon Y \to c.\mathrm{pt} $ as its second projection, - $ f $ as its first inclusion, and - a section of the split epimorphism induced by the idempotent $ \mathrm{id}_Y - f \circ \mathrm{retraction}(f) $ as its second inclusion. This bicone satisfies the necessary identities for being a biproduct diagram.

CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel definition

 {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) :
  (binaryBiconeOfIsSplitMonoOfCokernel i).IsBilimit

Full source

/-- The bicone constructed in `binaryBiconeOfSplitMonoOfCokernel` is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories. -/
def isBilimitBinaryBiconeOfIsSplitMonoOfCokernel {X Y : C} {f : X ⟶ Y} [IsSplitMono f]
    {c : CokernelCofork f} (i : IsColimit c) : (binaryBiconeOfIsSplitMonoOfCokernel i).IsBilimit :=
  isBinaryBilimitOfTotal _
    (by
      simp only [binaryBiconeOfIsSplitMonoOfCokernel_fst,
        binaryBiconeOfIsSplitMonoOfCokernel_inr,
        binaryBiconeOfIsSplitMonoOfCokernel_snd,
        splitEpiOfIdempotentOfIsColimitCofork_section_]
      dsimp only [binaryBiconeOfIsSplitMonoOfCokernel_pt]
      rw [isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]
      simp only [binaryBiconeOfIsSplitMonoOfCokernel_inl, Cofork.IsColimit.π_desc,
        cokernelCoforkOfCofork_π, Cofork.π_ofπ, add_sub_cancel])

Bilimit property of the bicone from a split monomorphism and its cokernel

Informal description

Given a split monomorphism $ f \colon X \to Y $ in a preadditive category $ \mathcal{C} $, and a cokernel cofork $ c $ of $ f $ that is a colimit, the binary bicone constructed via `binaryBiconeOfIsSplitMonoOfCokernel` is a bilimit bicone. This means it is both a limit cone and a colimit cocone for the pair $ (X, c.\mathrm{pt}) $.

CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl definition

{X Y : C} (b : BinaryBicone X Y) (hb : IsLimit b.sndKernelFork) : b.IsBilimit

Full source

/-- If `b` is a binary bicone such that `b.inl` is a kernel of `b.snd`, then `b` is a bilimit
    bicone. -/
def BinaryBicone.isBilimitOfKernelInl {X Y : C} (b : BinaryBicone X Y)
    (hb : IsLimit b.sndKernelFork) : b.IsBilimit :=
  isBinaryBilimitOfIsLimit _ <|
    BinaryFan.IsLimit.mk _ (fun f g => f ≫ b.inl + g ≫ b.inr) (fun f g => by simp)
      (fun f g => by simp) fun {T} f g m h₁ h₂ => by
      dsimp at m
      have h₁' : ((m : T ⟶ b.pt) - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0 := by
        simpa using sub_eq_zero.2 h₁
      have h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : T ⟶ X, hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' hb _ h₂'
      rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]

Bilimit bicone from kernel condition

Informal description

Given a binary bicone $ b $ for objects $ X $ and $ Y $ in a preadditive category $ C $, if the kernel fork of $ b.\text{snd} $ is a limit cone, then $ b $ is a bilimit bicone. This means that $ b $ is both a limit cone and a colimit cocone for the pair $ (X, Y) $.

CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInr definition

{X Y : C} (b : BinaryBicone X Y) (hb : IsLimit b.fstKernelFork) : b.IsBilimit

Full source

/-- If `b` is a binary bicone such that `b.inr` is a kernel of `b.fst`, then `b` is a bilimit
    bicone. -/
def BinaryBicone.isBilimitOfKernelInr {X Y : C} (b : BinaryBicone X Y)
    (hb : IsLimit b.fstKernelFork) : b.IsBilimit :=
  isBinaryBilimitOfIsLimit _ <|
    BinaryFan.IsLimit.mk _ (fun f g => f ≫ b.inl + g ≫ b.inr) (fun f g => by simp)
    (fun f g => by simp) fun {T} f g m h₁ h₂ => by
      dsimp at m
      have h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0 := by simpa using sub_eq_zero.2 h₁
      have h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : T ⟶ Y, hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' hb _ h₁'
      rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]

Bilimit bicone condition via kernel of first projection

Informal description

Given a binary bicone $ b $ for objects $ X $ and $ Y $ in a preadditive category $ C $, if the kernel fork of the first projection $ b.\text{fst} $ is a limit cone, then $ b $ is a bilimit bicone. This means that $ b $ is both a limit cone and a colimit cocone for the pair $ (X, Y) $.

CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst definition

{X Y : C} (b : BinaryBicone X Y) (hb : IsColimit b.inrCokernelCofork) : b.IsBilimit

Full source

/-- If `b` is a binary bicone such that `b.fst` is a cokernel of `b.inr`, then `b` is a bilimit
    bicone. -/
def BinaryBicone.isBilimitOfCokernelFst {X Y : C} (b : BinaryBicone X Y)
    (hb : IsColimit b.inrCokernelCofork) : b.IsBilimit :=
  isBinaryBilimitOfIsColimit _ <|
    BinaryCofan.IsColimit.mk _ (fun f g => b.fst ≫ f + b.snd ≫ g) (fun f g => by simp)
      (fun f g => by simp) fun {T} f g m h₁ h₂ => by
      dsimp at m
      have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁
      have h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : X ⟶ T, hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₂'
      rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]

Bilimit bicone from cokernel condition on first projection

Informal description

Given a binary bicone $b$ for objects $X$ and $Y$ in a preadditive category $C$, if the cokernel cofork of the first projection $b.\text{fst}$ is a colimit cofork, then $b$ is a bilimit bicone. This means that $b$ is both a limit cone and a colimit cocone for the pair $(X, Y)$.

CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnd definition

{X Y : C} (b : BinaryBicone X Y) (hb : IsColimit b.inlCokernelCofork) : b.IsBilimit

Full source

/-- If `b` is a binary bicone such that `b.snd` is a cokernel of `b.inl`, then `b` is a bilimit
    bicone. -/
def BinaryBicone.isBilimitOfCokernelSnd {X Y : C} (b : BinaryBicone X Y)
    (hb : IsColimit b.inlCokernelCofork) : b.IsBilimit :=
  isBinaryBilimitOfIsColimit _ <|
    BinaryCofan.IsColimit.mk _ (fun f g => b.fst ≫ f + b.snd ≫ g) (fun f g => by simp)
      (fun f g => by simp) fun {T} f g m h₁ h₂ => by
      dsimp at m
      have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁
      have h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : Y ⟶ T, hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₁'
      rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]

Bilimit bicone from cokernel condition on second projection

Informal description

Given a binary bicone $b$ for objects $X$ and $Y$ in a preadditive category $C$, if the cokernel cofork of the second projection $b.\text{snd}$ is a colimit cofork, then $b$ is a bilimit bicone. This means that $b$ is both a limit cone and a colimit cocone for the pair $(X, Y)$.

CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel definition

{X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : BinaryBicone c.pt Y

Full source

/-- Every split epi `f` with a kernel induces a binary bicone with `f` as its `snd` and
the kernel map as its `inl`.
We will show in `binary_bicone_of_is_split_mono_of_cokernel` that this binary bicone is in fact
already a biproduct. -/
@[simps]
def binaryBiconeOfIsSplitEpiOfKernel {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f}
    (i : IsLimit c) : BinaryBicone c.pt Y :=
  { pt := X
    fst :=
      let c' : KernelFork (𝟙 X - (𝟙 X - f ≫ section_ f)) := KernelFork.ofι (Fork.ι c) (by simp)
      let i' : IsLimit c' := isKernelCompMono i (section_ f) (by simp)
      let i'' := isLimitForkOfKernelFork i'
      (splitMonoOfIdempotentOfIsLimitFork C (by simp) i'').retraction
    snd := f
    inl := c.ι
    inr := section_ f
    inl_fst := by apply SplitMono.id
    inl_snd := by simp
    inr_fst := by
      dsimp only
      rw [splitMonoOfIdempotentOfIsLimitFork_retraction, isLimitForkOfKernelFork_lift,
        isKernelCompMono_lift]
      dsimp only [kernelForkOfFork_ι]
      letI := mono_of_isLimit_fork i
      apply zero_of_comp_mono c.ι
      simp only [comp_sub, Category.comp_id, Category.assoc, sub_self, Fork.IsLimit.lift_ι,
        Fork.ι_ofι, IsSplitEpi.id_assoc]
    inr_snd := by simp }

Binary bicone from a split epimorphism and its kernel

Informal description

Given a split epimorphism $ f : X \to Y $ in a preadditive category $ C $ and a kernel fork $ c $ of $ f $ that is a limit cone, the function constructs a binary bicone with $ c.\text{pt} $ and $ Y $ as its objects. The bicone has: - $ f $ as its second projection, - the kernel map $ c.\iota $ as its first inclusion, - a section of $ f $ as its second inclusion, and - a retraction of the idempotent $ \text{id}_X - f \circ \text{section}_f $ as its first projection.

CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel definition

 {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) :
  (binaryBiconeOfIsSplitEpiOfKernel i).IsBilimit

Full source

/-- The bicone constructed in `binaryBiconeOfIsSplitEpiOfKernel` is a bilimit.
This is a version of the splitting lemma that holds in all preadditive categories. -/
def isBilimitBinaryBiconeOfIsSplitEpiOfKernel {X Y : C} {f : X ⟶ Y} [IsSplitEpi f]
    {c : KernelFork f} (i : IsLimit c) : (binaryBiconeOfIsSplitEpiOfKernel i).IsBilimit :=
  BinaryBicone.isBilimitOfKernelInl _ <| i.ofIsoLimit <| Fork.ext (Iso.refl _) (by simp)

Bilimit property of the binary bicone from a split epimorphism and its kernel

Informal description

Given a split epimorphism $ f : X \to Y $ in a preadditive category $ C $ and a kernel fork $ c $ of $ f $ that is a limit cone, the binary bicone constructed from $ c $ and $ Y $ is a bilimit bicone. This means it is both a limit cone and a colimit cocone for the pair $ (c.\text{pt}, Y) $.

CategoryTheory.Limits.biprod.add_eq_lift_id_desc theorem

[HasBinaryBiproduct X X] : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g

Full source

/-- The existence of binary biproducts implies that there is at most one preadditive structure. -/
theorem biprod.add_eq_lift_id_desc [HasBinaryBiproduct X X] :
    f + g = biprod.liftbiprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g := by simp

Sum of Morphisms as Biproduct Lift and Descend Composition

Informal description

In a preadditive category $C$ with binary biproducts, for any object $X$ and morphisms $f, g \colon X \to Y$, the sum of $f$ and $g$ is equal to the composition of the biproduct lift morphism $\text{biprod.lift}\, \text{id}_X\, \text{id}_X$ with the biproduct descend morphism $\text{biprod.desc}\, f\, g$, i.e., \[ f + g = \text{biprod.lift}\, \text{id}_X\, \text{id}_X \circ \text{biprod.desc}\, f\, g. \]

CategoryTheory.Limits.biprod.add_eq_lift_desc_id theorem

[HasBinaryBiproduct Y Y] : f + g = biprod.lift f g ≫ biprod.desc (𝟙 Y) (𝟙 Y)

Full source

/-- The existence of binary biproducts implies that there is at most one preadditive structure. -/
theorem biprod.add_eq_lift_desc_id [HasBinaryBiproduct Y Y] :
    f + g = biprod.liftbiprod.lift f g ≫ biprod.desc (𝟙 Y) (𝟙 Y) := by simp

Sum of Morphisms as Biproduct Lift and Descend Composition with Identities

Informal description

In a preadditive category with binary biproducts, for any object $Y$ and morphisms $f, g \colon X \to Y$, the sum of $f$ and $g$ is equal to the composition of the biproduct lift morphism $\text{biprod.lift}\, f\, g$ with the biproduct descend morphism $\text{biprod.desc}\, \text{id}_Y\, \text{id}_Y$, i.e., \[ f + g = \text{biprod.lift}\, f\, g \circ \text{biprod.desc}\, \text{id}_Y\, \text{id}_Y. \]

CategoryTheory.subsingleton_preadditive_of_hasBinaryBiproducts instance

{C : Type u} [Category.{v} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] : Subsingleton (Preadditive C)

Full source

/-- The existence of binary biproducts implies that there is at most one preadditive structure. -/
instance subsingleton_preadditive_of_hasBinaryBiproducts {C : Type u} [Category.{v} C]
    [HasZeroMorphisms C] [HasBinaryBiproducts C] : Subsingleton (Preadditive C) where
  allEq := fun a b => by
    apply Preadditive.ext; funext X Y; apply AddCommGroup.ext; funext f g
    have h₁ := @biprod.add_eq_lift_id_desc _ _ a _ _ f g
      (by convert (inferInstance : HasBinaryBiproduct X X); subsingleton)
    have h₂ := @biprod.add_eq_lift_id_desc _ _ b _ _ f g
      (by convert (inferInstance : HasBinaryBiproduct X X); subsingleton)
    refine h₁.trans (Eq.trans ?_ h₂.symm)
    congr! 2 <;> subsingleton

Uniqueness of Preadditive Structure in Categories with Binary Biproducts

Informal description

In a category $C$ with zero morphisms and binary biproducts, there is at most one preadditive structure on $C$.

CategoryTheory.Biprod.ofComponents definition

: X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂

Full source

/-- The "matrix" morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` with specified components.
-/
def Biprod.ofComponents : X₁ ⊞ X₂X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ :=
  biprod.fstbiprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fstbiprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.sndbiprod.snd ≫ f₂₁ ≫ biprod.inl +
    biprod.sndbiprod.snd ≫ f₂₂ ≫ biprod.inr

Matrix morphism between biproducts

Informal description

The morphism $X_1 \oplus X_2 \to Y_1 \oplus Y_2$ defined by the "matrix" of components $f_{11} : X_1 \to Y_1$, $f_{12} : X_1 \to Y_2$, $f_{21} : X_2 \to Y_1$, and $f_{22} : X_2 \to Y_2$ is given by the sum: \[ \text{biprod.fst} \circ f_{11} \circ \text{biprod.inl} + \text{biprod.fst} \circ f_{12} \circ \text{biprod.inr} + \text{biprod.snd} \circ f_{21} \circ \text{biprod.inl} + \text{biprod.snd} \circ f_{22} \circ \text{biprod.inr} \]

CategoryTheory.Biprod.inl_ofComponents theorem

: biprod.inl ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ biprod.inl + f₁₂ ≫ biprod.inr

Full source

@[simp]
theorem Biprod.inl_ofComponents :
    biprod.inlbiprod.inl ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ biprod.inl + f₁₂ ≫ biprod.inr := by
  simp [Biprod.ofComponents]

Composition of Left Inclusion with Matrix Morphism Equals Sum of Components

Informal description

Let $X_1 \oplus X_2$ and $Y_1 \oplus Y_2$ be biproducts in a preadditive category, and let $f_{11} : X_1 \to Y_1$, $f_{12} : X_1 \to Y_2$, $f_{21} : X_2 \to Y_1$, and $f_{22} : X_2 \to Y_2$ be morphisms. Then the composition of the inclusion $\text{inl} : X_1 \to X_1 \oplus X_2$ with the matrix morphism $\text{Biprod.ofComponents}\, f_{11}\, f_{12}\, f_{21}\, f_{22} : X_1 \oplus X_2 \to Y_1 \oplus Y_2$ equals the sum $f_{11} \circ \text{inl} + f_{12} \circ \text{inr}$, where $\text{inr} : X_2 \to X_1 \oplus X_2$ is the other inclusion map.

CategoryTheory.Biprod.inr_ofComponents theorem

: biprod.inr ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₂₁ ≫ biprod.inl + f₂₂ ≫ biprod.inr

Full source

@[simp]
theorem Biprod.inr_ofComponents :
    biprod.inrbiprod.inr ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₂₁ ≫ biprod.inl + f₂₂ ≫ biprod.inr := by
  simp [Biprod.ofComponents]

Right Inclusion Composition with Matrix Morphism Equals Sum of Component Compositions

Informal description

For any morphisms $f_{11} : X_1 \to Y_1$, $f_{12} : X_1 \to Y_2$, $f_{21} : X_2 \to Y_1$, and $f_{22} : X_2 \to Y_2$ in a preadditive category, the composition of the right inclusion $\text{inr} : X_2 \to X_1 \oplus X_2$ with the matrix morphism $\text{Biprod.ofComponents}(f_{11}, f_{12}, f_{21}, f_{22})$ equals the sum of the compositions $f_{21} \circ \text{inl}$ and $f_{22} \circ \text{inr}$, where $\text{inl} : X_1 \to X_1 \oplus X_2$ and $\text{inr} : X_2 \to X_1 \oplus X_2$ are the left and right inclusions, respectively. That is, \[ \text{inr} \circ \text{Biprod.ofComponents}(f_{11}, f_{12}, f_{21}, f_{22}) = f_{21} \circ \text{inl} + f_{22} \circ \text{inr}. \]

CategoryTheory.Biprod.ofComponents_fst theorem

: Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.fst = biprod.fst ≫ f₁₁ + biprod.snd ≫ f₂₁

Full source

@[simp]
theorem Biprod.ofComponents_fst :
    Biprod.ofComponentsBiprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.fst = biprod.fstbiprod.fst ≫ f₁₁ + biprod.sndbiprod.snd ≫ f₂₁ := by
  simp [Biprod.ofComponents]

First Projection of Biproduct Matrix Morphism

Informal description

For any morphisms $f_{11} \colon X_1 \to Y_1$, $f_{12} \colon X_1 \to Y_2$, $f_{21} \colon X_2 \to Y_1$, and $f_{22} \colon X_2 \to Y_2$ in a preadditive category, the composition of the biproduct morphism $\text{Biprod.ofComponents}(f_{11}, f_{12}, f_{21}, f_{22}) \colon X_1 \oplus X_2 \to Y_1 \oplus Y_2$ with the first projection $\text{biprod.fst} \colon Y_1 \oplus Y_2 \to Y_1$ satisfies: \[ \text{Biprod.ofComponents}(f_{11}, f_{12}, f_{21}, f_{22}) \circ \text{biprod.fst} = \text{biprod.fst} \circ f_{11} + \text{biprod.snd} \circ f_{21}. \]

CategoryTheory.Biprod.ofComponents_snd theorem

: Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.snd = biprod.fst ≫ f₁₂ + biprod.snd ≫ f₂₂

Full source

@[simp]
theorem Biprod.ofComponents_snd :
    Biprod.ofComponentsBiprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.snd = biprod.fstbiprod.fst ≫ f₁₂ + biprod.sndbiprod.snd ≫ f₂₂ := by
  simp [Biprod.ofComponents]

Second Projection of Matrix Morphism Between Biproducts

Informal description

For any morphism $f \colon X_1 \oplus X_2 \to Y_1 \oplus Y_2$ in a preadditive category, represented by components $f_{11} \colon X_1 \to Y_1$, $f_{12} \colon X_1 \to Y_2$, $f_{21} \colon X_2 \to Y_1$, and $f_{22} \colon X_2 \to Y_2$, the composition of $f$ with the second projection $\text{snd} \colon Y_1 \oplus Y_2 \to Y_2$ satisfies: \[ f \circ \text{snd} = \text{fst} \circ f_{12} + \text{snd} \circ f_{22} \] where $\text{fst} \colon X_1 \oplus X_2 \to X_1$ and $\text{snd} \colon X_1 \oplus X_2 \to X_2$ are the first and second projections, respectively.

CategoryTheory.Biprod.ofComponents_eq theorem

 (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) :
  Biprod.ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f

Full source

@[simp]
theorem Biprod.ofComponents_eq (f : X₁ ⊞ X₂X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) :
    Biprod.ofComponents (biprod.inlbiprod.inl ≫ f ≫ biprod.fst) (biprod.inlbiprod.inl ≫ f ≫ biprod.snd)
        (biprod.inrbiprod.inr ≫ f ≫ biprod.fst) (biprod.inrbiprod.inr ≫ f ≫ biprod.snd) =
      f := by
  ext <;>
    simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
      Biprod.inl_ofComponents, Biprod.inr_ofComponents, eq_self_iff_true, Category.assoc,
      comp_zero, biprod.inl_fst, Preadditive.add_comp]

Matrix Representation of Biproduct Morphism Equals Original Morphism

Informal description

For any morphism $f \colon X_1 \oplus X_2 \to Y_1 \oplus Y_2$ in a preadditive category, the matrix morphism constructed from its components via $\text{Biprod.ofComponents}$ equals $f$ itself. Specifically, the components are given by: \[ \text{inl} \circ f \circ \text{fst}, \quad \text{inl} \circ f \circ \text{snd}, \quad \text{inr} \circ f \circ \text{fst}, \quad \text{inr} \circ f \circ \text{snd}, \] where $\text{inl} \colon X_1 \to X_1 \oplus X_2$ and $\text{inr} \colon X_2 \to X_1 \oplus X_2$ are the inclusion maps, and $\text{fst} \colon Y_1 \oplus Y_2 \to Y_1$ and $\text{snd} \colon Y_1 \oplus Y_2 \to Y_2$ are the projection maps.

CategoryTheory.Biprod.ofComponents_comp theorem

 {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) (g₁₁ : Y₁ ⟶ Z₁) (g₁₂ : Y₁ ⟶ Z₂)
  (g₂₁ : Y₂ ⟶ Z₁) (g₂₂ : Y₂ ⟶ Z₂) :
  Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ Biprod.ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
    Biprod.ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂)

Full source

@[simp]
theorem Biprod.ofComponents_comp {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
    (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) (g₁₁ : Y₁ ⟶ Z₁) (g₁₂ : Y₁ ⟶ Z₂) (g₂₁ : Y₂ ⟶ Z₁)
    (g₂₂ : Y₂ ⟶ Z₂) :
    Biprod.ofComponentsBiprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ Biprod.ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
      Biprod.ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁)
        (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) := by
  dsimp [Biprod.ofComponents]
  ext <;>
    simp only [add_comp, comp_add, add_comp_assoc, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Matrix Composition in Biproduct Categories

Informal description

Let $X_1, X_2, Y_1, Y_2, Z_1, Z_2$ be objects in a preadditive category $C$. Given morphisms $f_{11} : X_1 \to Y_1$, $f_{12} : X_1 \to Y_2$, $f_{21} : X_2 \to Y_1$, $f_{22} : X_2 \to Y_2$, $g_{11} : Y_1 \to Z_1$, $g_{12} : Y_1 \to Z_2$, $g_{21} : Y_2 \to Z_1$, and $g_{22} : Y_2 \to Z_2$, the composition of the matrix morphisms $Biprod.ofComponents(f_{11}, f_{12}, f_{21}, f_{22})$ and $Biprod.ofComponents(g_{11}, g_{12}, g_{21}, g_{22})$ is equal to the matrix morphism defined by the components: \[ (f_{11} \circ g_{11} + f_{12} \circ g_{21}, f_{11} \circ g_{12} + f_{12} \circ g_{22}, f_{21} \circ g_{11} + f_{22} \circ g_{21}, f_{21} \circ g_{12} + f_{22} \circ g_{22}). \]

CategoryTheory.Biprod.unipotentUpper definition

{X₁ X₂ : C} (r : X₁ ⟶ X₂) : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂

Full source

/-- The unipotent upper triangular matrix
```
(1 r)
(0 1)
```
as an isomorphism.
-/
@[simps]
def Biprod.unipotentUpper {X₁ X₂ : C} (r : X₁ ⟶ X₂) : X₁ ⊞ X₂X₁ ⊞ X₂ ≅ X₁ ⊞ X₂ where
  hom := Biprod.ofComponents (𝟙 _) r 0 (𝟙 _)
  inv := Biprod.ofComponents (𝟙 _) (-r) 0 (𝟙 _)

Unipotent upper triangular isomorphism of biproducts

Informal description

Given two objects $X_1$ and $X_2$ in a preadditive category $\mathcal{C}$ and a morphism $r : X_1 \to X_2$, the isomorphism $X_1 \oplus X_2 \cong X_1 \oplus X_2$ is defined by the upper triangular matrix \[ \begin{pmatrix} 1 & r \\ 0 & 1 \end{pmatrix}, \] with its inverse given by the matrix \[ \begin{pmatrix} 1 & -r \\ 0 & 1 \end{pmatrix}. \]

CategoryTheory.Biprod.unipotentLower definition

{X₁ X₂ : C} (r : X₂ ⟶ X₁) : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂

Full source

/-- The unipotent lower triangular matrix
```
(1 0)
(r 1)
```
as an isomorphism.
-/
@[simps]
def Biprod.unipotentLower {X₁ X₂ : C} (r : X₂ ⟶ X₁) : X₁ ⊞ X₂X₁ ⊞ X₂ ≅ X₁ ⊞ X₂ where
  hom := Biprod.ofComponents (𝟙 _) 0 r (𝟙 _)
  inv := Biprod.ofComponents (𝟙 _) 0 (-r) (𝟙 _)

Lower triangular unipotent isomorphism between biproducts

Informal description

For objects $X_1$ and $X_2$ in a preadditive category $\mathcal{C}$, and a morphism $r : X_2 \to X_1$, the isomorphism $X_1 \oplus X_2 \cong X_1 \oplus X_2$ is given by the lower triangular matrix \[ \begin{pmatrix} 1 & 0 \\ r & 1 \end{pmatrix}, \] with inverse given by the matrix \[ \begin{pmatrix} 1 & 0 \\ -r & 1 \end{pmatrix}. \]

CategoryTheory.Biprod.gaussian' definition

 [IsIso f₁₁] :
  Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂),
    L.hom ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g₂₂

Full source

/-- If `f` is a morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct isomorphisms `L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂` and `R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂`
so that `L.hom ≫ g ≫ R.hom` is diagonal (with `X₁ ⟶ Y₁` component still `f`),
via Gaussian elimination.

(This is the version of `Biprod.gaussian` written in terms of components.)
-/
def Biprod.gaussian' [IsIso f₁₁] :
    Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂),
      L.hom ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g₂₂ :=
  ⟨Biprod.unipotentLower (-f₂₁ ≫ inv f₁₁), Biprod.unipotentUpper (-inv f₁₁ ≫ f₁₂),
    f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂, by ext <;> simp; abel⟩

Gaussian elimination for biproducts in preadditive categories

Informal description

Given a morphism $ f : X_1 \oplus X_2 \to Y_1 \oplus Y_2 $ in a preadditive category, represented by the matrix components $ f_{11} : X_1 \to Y_1 $, $ f_{12} : X_1 \to Y_2 $, $ f_{21} : X_2 \to Y_1 $, and $ f_{22} : X_2 \to Y_2 $, where $ f_{11} $ is an isomorphism, there exist isomorphisms $ L : X_1 \oplus X_2 \cong X_1 \oplus X_2 $ and $ R : Y_1 \oplus Y_2 \cong Y_1 \oplus Y_2 $, and a morphism $ g_{22} : X_2 \to Y_2 $, such that the composition $ L \circ f \circ R $ is the diagonal morphism $ \text{biprod.map}(f_{11}, g_{22}) $.

CategoryTheory.Biprod.gaussian definition

 (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) [IsIso (biprod.inl ≫ f ≫ biprod.fst)] :
  Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂),
    L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂

Full source

/-- If `f` is a morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct isomorphisms `L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂` and `R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂`
so that `L.hom ≫ g ≫ R.hom` is diagonal (with `X₁ ⟶ Y₁` component still `f`),
via Gaussian elimination.
-/
def Biprod.gaussian (f : X₁ ⊞ X₂X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) [IsIso (biprod.inlbiprod.inl ≫ f ≫ biprod.fst)] :
    Σ' (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) (g₂₂ : X₂ ⟶ Y₂),
      L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂ := by
  let this :=
    Biprod.gaussian' (biprod.inlbiprod.inl ≫ f ≫ biprod.fst) (biprod.inlbiprod.inl ≫ f ≫ biprod.snd)
      (biprod.inrbiprod.inr ≫ f ≫ biprod.fst) (biprod.inrbiprod.inr ≫ f ≫ biprod.snd)
  rwa [Biprod.ofComponents_eq] at this

Gaussian elimination for biproduct morphisms with invertible diagonal component

Informal description

Given a morphism $ f : X_1 \oplus X_2 \to Y_1 \oplus Y_2 $ in a preadditive category such that the component $ \text{biprod.inl} \circ f \circ \text{biprod.fst} : X_1 \to Y_1 $ is an isomorphism, there exist isomorphisms $ L : X_1 \oplus X_2 \cong X_1 \oplus X_2 $ and $ R : Y_1 \oplus Y_2 \cong Y_1 \oplus Y_2 $, and a morphism $ g_{22} : X_2 \to Y_2 $, such that the composition $ L \circ f \circ R $ equals the diagonal morphism $ \text{biprod.map}(f_{11}, g_{22}) $, where $ f_{11} = \text{biprod.inl} \circ f \circ \text{biprod.fst} $.

CategoryTheory.Biprod.isoElim' definition

[IsIso f₁₁] [IsIso (Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)] : X₂ ≅ Y₂

Full source

/-- If `X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂` via a two-by-two matrix whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct an isomorphism `X₂ ≅ Y₂`, via Gaussian elimination.
-/
def Biprod.isoElim' [IsIso f₁₁] [IsIso (Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)] : X₂ ≅ Y₂ := by
  obtain ⟨L, R, g, w⟩ := Biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂
  letI : IsIso (biprod.map f₁₁ g) := by
    rw [← w]
    infer_instance
  letI : IsIso g := isIso_right_of_isIso_biprod_map f₁₁ g
  exact asIso g

Isomorphism elimination for biproducts via Gaussian elimination

Informal description

Given a morphism $ f : X_1 \oplus X_2 \to Y_1 \oplus Y_2 $ in a preadditive category, represented by the matrix components $ f_{11} : X_1 \to Y_1 $, $ f_{12} : X_1 \to Y_2 $, $ f_{21} : X_2 \to Y_1 $, and $ f_{22} : X_2 \to Y_2 $, where both $ f_{11} $ and the entire morphism $ f $ are isomorphisms, there exists an isomorphism $ X_2 \cong Y_2 $. This is constructed via Gaussian elimination on the matrix representation of $ f $.

CategoryTheory.Biprod.isoElim definition

(f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂) [IsIso (biprod.inl ≫ f.hom ≫ biprod.fst)] : X₂ ≅ Y₂

Full source

/-- If `f` is an isomorphism `X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct an isomorphism `X₂ ≅ Y₂`, via Gaussian elimination.
-/
def Biprod.isoElim (f : X₁ ⊞ X₂X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂) [IsIso (biprod.inlbiprod.inl ≫ f.hom ≫ biprod.fst)] : X₂ ≅ Y₂ :=
  letI :
    IsIso
      (Biprod.ofComponents (biprod.inlbiprod.inl ≫ f.hom ≫ biprod.fst) (biprod.inlbiprod.inl ≫ f.hom ≫ biprod.snd)
        (biprod.inrbiprod.inr ≫ f.hom ≫ biprod.fst) (biprod.inrbiprod.inr ≫ f.hom ≫ biprod.snd)) := by
    simp only [Biprod.ofComponents_eq]
    infer_instance
  Biprod.isoElim' (biprod.inlbiprod.inl ≫ f.hom ≫ biprod.fst) (biprod.inlbiprod.inl ≫ f.hom ≫ biprod.snd)
    (biprod.inrbiprod.inr ≫ f.hom ≫ biprod.fst) (biprod.inrbiprod.inr ≫ f.hom ≫ biprod.snd)

Isomorphism elimination for biproducts via Gaussian elimination

Informal description

Given an isomorphism $ f : X_1 \oplus X_2 \cong Y_1 \oplus Y_2 $ in a preadditive category such that the component $ \text{biprod.inl} \circ f \circ \text{biprod.fst} : X_1 \to Y_1 $ is an isomorphism, there exists an isomorphism $ X_2 \cong Y_2 $. This is constructed via Gaussian elimination on the matrix representation of $ f $.

CategoryTheory.Biprod.column_nonzero_of_iso theorem

 {W X Y Z : C} (f : W ⊞ X ⟶ Y ⊞ Z) [IsIso f] :
  𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0

Full source

theorem Biprod.column_nonzero_of_iso {W X Y Z : C} (f : W ⊞ XW ⊞ X ⟶ Y ⊞ Z) [IsIso f] :
    𝟙𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0 := by
  by_contra! h
  rcases h with ⟨nz, a₁, a₂⟩
  set x := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
  have h₁ : x = 𝟙 W := by simp [x]
  have h₀ : x = 0 := by
    dsimp [x]
    rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]
    conv_lhs =>
      slice 2 3
      rw [comp_add]
    simp only [Category.assoc]
    rw [comp_add_assoc, add_comp]
    conv_lhs =>
      congr
      next => skip
      slice 1 3
      rw [a₂]
    simp only [zero_comp, add_zero]
    conv_lhs =>
      slice 1 3
      rw [a₁]
    simp only [zero_comp]
  exact nz (h₁.symm.trans h₀)

Nonzero Component Condition for Isomorphisms of Biproducts

Informal description

Let $C$ be a preadditive category with zero morphisms and binary biproducts. For any objects $W, X, Y, Z$ in $C$ and any isomorphism $f : W \oplus X \to Y \oplus Z$, either the identity morphism on $W$ is zero, or at least one of the component morphisms $W \to Y$ or $W \to Z$ is nonzero. In other words, if $f$ is an isomorphism, then either $\text{id}_W = 0$ or there exists a nonzero morphism from $W$ to either $Y$ or $Z$ via the decomposition of $f$.

CategoryTheory.Biproduct.column_nonzero_of_iso' theorem

 {σ τ : Type} [Finite τ] {S : σ → C} [HasBiproduct S] {T : τ → C} [HasBiproduct T] (s : σ) (f : ⨁ S ⟶ ⨁ T) [IsIso f] :
  (∀ t : τ, biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0

Full source

theorem Biproduct.column_nonzero_of_iso' {σ τ : Type} [Finite τ] {S : σ → C} [HasBiproduct S]
    {T : τ → C} [HasBiproduct T] (s : σ) (f : ⨁ S⨁ S ⟶ ⨁ T) [IsIso f] :
    (∀ t : τ, biproduct.ιbiproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0 := by
  cases nonempty_fintype τ
  intro z
  have reassoced {t : τ} {W : C} (h : _ ⟶ W) :
    biproduct.ιbiproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h := by
    simp only [← Category.assoc]
    apply eq_whisker
    simp only [Category.assoc]
    apply z
  set x := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
  have h₁ : x = 𝟙 (S s) := by simp [x]
  have h₀ : x = 0 := by
    dsimp [x]
    rw [← Category.id_comp (inv f), Category.assoc, ← biproduct.total]
    simp only [comp_sum_assoc]
    conv_lhs =>
      congr
      congr
      next => skip
      intro j; simp only [reassoced]
    simp
  exact h₁.symm.trans h₀

Triviality of Object from Vanishing Column in Biproduct Isomorphism

Informal description

Let $C$ be a preadditive category with finite biproducts, and let $S : \sigma \to C$ and $T : \tau \to C$ be families of objects in $C$ with $\tau$ finite. Given an isomorphism $f : \bigoplus S \to \bigoplus T$ and a summand $s \in \sigma$, if for every $t \in \tau$ the composition $\iota_s \circ f \circ \pi_t$ is zero, then the identity morphism on $S(s)$ must be zero. In other words, if all matrix entries in the $s$-th column of $f$ are zero, then the object $S(s)$ is trivial (i.e., $\text{id}_{S(s)} = 0$).

CategoryTheory.Biproduct.columnNonzeroOfIso definition

 {σ τ : Type} [Fintype τ] {S : σ → C} [HasBiproduct S] {T : τ → C} [HasBiproduct T] (s : σ) (nz : 𝟙 (S s) ≠ 0)
  (f : ⨁ S ⟶ ⨁ T) [IsIso f] : Trunc (Σ' t : τ, biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)

Full source

/-- If `f : ⨁ S ⟶ ⨁ T` is an isomorphism, and `s` is a non-trivial summand of the source,
then there is some `t` in the target so that the `s, t` matrix entry of `f` is nonzero.
-/
def Biproduct.columnNonzeroOfIso {σ τ : Type} [Fintype τ] {S : σ → C} [HasBiproduct S] {T : τ → C}
    [HasBiproduct T] (s : σ) (nz : 𝟙𝟙 (S s) ≠ 0) (f : ⨁ S⨁ S ⟶ ⨁ T) [IsIso f] :
    Trunc (Σ't : τ, biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0) := by
  classical
    apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t h)

Nonzero matrix entry condition for isomorphisms of biproducts

Informal description

Let $C$ be a preadditive category with finite biproducts, and let $S : \sigma \to C$ and $T : \tau \to C$ be families of objects in $C$ with $\tau$ finite. Given an isomorphism $f : \bigoplus S \to \bigoplus T$ and a summand $s \in \sigma$ such that the identity morphism on $S(s)$ is nonzero, there exists some $t \in \tau$ such that the $(s, t)$-entry of $f$ (given by the composition $\iota_s \circ f \circ \pi_t$) is nonzero.

CategoryTheory.Limits.preservesProduct_of_preservesBiproduct theorem

{f : J → C} [PreservesBiproduct f F] : PreservesLimit (Discrete.functor f) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
    preserves finite products. -/
lemma preservesProduct_of_preservesBiproduct {f : J → C} [PreservesBiproduct f F] :
    PreservesLimit (Discrete.functor f) F where
  preserves hc :=
    let ⟨_⟩ := nonempty_fintype J
    ⟨IsLimit.ofIsoLimit
        ((IsLimit.postcomposeInvEquiv (Discrete.compNatIsoDiscrete _ _) _).symm
          (isBilimitOfPreserves F (biconeIsBilimitOfLimitConeOfIsLimit hc)).isLimit) <|
      Cones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Biproduct-Preserving Functors Preserve Products in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves the biproduct of a family of objects $f \colon J \to C$, then $F$ preserves the product of $f$. In other words, given that $F$ maps any bilimit bicone over $f$ to a bilimit bicone over $F \circ f$, it follows that $F$ maps any limit cone over the discrete diagram of $f$ to a limit cone in $D$.

CategoryTheory.Limits.preservesProductsOfShape_of_preservesBiproductsOfShape theorem

[PreservesBiproductsOfShape J F] : PreservesLimitsOfShape (Discrete J) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
    preserves finite products. -/
lemma preservesProductsOfShape_of_preservesBiproductsOfShape [PreservesBiproductsOfShape J F] :
    PreservesLimitsOfShape (Discrete J) F where
  preservesLimit {_} := preservesLimit_of_iso_diagram _ Discrete.natIsoFunctor.symm

Preservation of Products by Biproduct-Preserving Functors in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves all biproducts of shape $J$ in $C$, then $F$ preserves all products of shape $J$ in $C$.

CategoryTheory.Limits.preservesBiproduct_of_preservesProduct theorem

{f : J → C} [PreservesLimit (Discrete.functor f) F] : PreservesBiproduct f F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite products
    preserves finite biproducts. -/
lemma preservesBiproduct_of_preservesProduct {f : J → C} [PreservesLimit (Discrete.functor f) F] :
    PreservesBiproduct f F where
  preserves {b} hb :=
    let ⟨_⟩ := nonempty_fintype J
    ⟨isBilimitOfIsLimit _ <|
      IsLimit.ofIsoLimit
          ((IsLimit.postcomposeHomEquiv (Discrete.compNatIsoDiscrete _ _) (F.mapCone b.toCone)).symm
            (isLimitOfPreserves F hb.isLimit)) <|
        Cones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Preservation of Biproducts by Product-Preserving Functors in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms and finite products. If $F$ preserves the product of a finite family of objects $f \colon J \to C$, then $F$ preserves the biproduct of $f$.

CategoryTheory.Limits.preservesBiproduct_of_mono_biproductComparison theorem

{f : J → C} [HasBiproduct f] [HasBiproduct (F.obj ∘ f)] [Mono (biproductComparison F f)] : PreservesBiproduct f F

Full source

/-- If the (product-like) biproduct comparison for `F` and `f` is a monomorphism, then `F`
    preserves the biproduct of `f`. For the converse, see `mapBiproduct`. -/
lemma preservesBiproduct_of_mono_biproductComparison {f : J → C} [HasBiproduct f]
    [HasBiproduct (F.obj ∘ f)] [Mono (biproductComparison F f)] : PreservesBiproduct f F := by
  haveI : HasProduct fun b => F.obj (f b) := by
    change HasProduct (F.obj ∘ f)
    infer_instance
  have that : piComparison F f =
      (F.mapIso (biproduct.isoProduct f)).inv ≫
        biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
    ext j
    convert piComparison_comp_π F f j; simp [← Function.comp_def, ← Functor.map_comp]
  haveI : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _
  haveI : IsIso (piComparison F f) := by
    rw [that]
    infer_instance
  haveI := PreservesProduct.of_iso_comparison F f
  apply preservesBiproduct_of_preservesProduct

Preservation of Biproducts by Functors with Monomorphic Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be preadditive categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor that preserves zero morphisms. Given a family of objects $f \colon J \to \mathcal{C}$ with biproduct $\bigoplus f$ in $\mathcal{C}$ and biproduct $\bigoplus (F \circ f)$ in $\mathcal{D}$, if the biproduct comparison morphism $\text{biproductComparison}\, F\, f \colon F(\bigoplus f) \to \bigoplus (F \circ f)$ is a monomorphism, then $F$ preserves the biproduct of $f$.

CategoryTheory.Limits.preservesBiproduct_of_epi_biproductComparison' theorem

{f : J → C} [HasBiproduct f] [HasBiproduct (F.obj ∘ f)] [Epi (biproductComparison' F f)] : PreservesBiproduct f F

Full source

/-- If the (coproduct-like) biproduct comparison for `F` and `f` is an epimorphism, then `F`
    preserves the biproduct of `F` and `f`. For the converse, see `mapBiproduct`. -/
lemma preservesBiproduct_of_epi_biproductComparison' {f : J → C} [HasBiproduct f]
    [HasBiproduct (F.obj ∘ f)] [Epi (biproductComparison' F f)] : PreservesBiproduct f F := by
  haveI : Epi (splitEpiBiproductComparison F f).section_ := by simpa
  haveI : IsIso (biproductComparison F f) :=
    IsIso.of_epi_section' (splitEpiBiproductComparison F f)
  apply preservesBiproduct_of_mono_biproductComparison

Biproduct Preservation via Epimorphic Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be preadditive categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor that preserves zero morphisms. Given a family of objects $f \colon J \to \mathcal{C}$ with biproduct $\bigoplus f$ in $\mathcal{C}$ and biproduct $\bigoplus (F \circ f)$ in $\mathcal{D}$, if the comparison morphism $\bigoplus (F \circ f) \to F(\bigoplus f)$ is an epimorphism, then $F$ preserves the biproduct of $f$.

CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesProductsOfShape theorem

[PreservesLimitsOfShape (Discrete J) F] : PreservesBiproductsOfShape J F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite products
    preserves finite biproducts. -/
lemma preservesBiproductsOfShape_of_preservesProductsOfShape
    [PreservesLimitsOfShape (Discrete J) F] :
    PreservesBiproductsOfShape J F where
  preserves {_} := preservesBiproduct_of_preservesProduct F

Preservation of Biproducts by Product-Preserving Functors in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves all products of shape $J$ (where $J$ is a finite discrete category), then $F$ preserves all biproducts of shape $J$.

CategoryTheory.Limits.preservesCoproduct_of_preservesBiproduct theorem

{f : J → C} [PreservesBiproduct f F] : PreservesColimit (Discrete.functor f) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
    preserves finite coproducts. -/
lemma preservesCoproduct_of_preservesBiproduct {f : J → C} [PreservesBiproduct f F] :
    PreservesColimit (Discrete.functor f) F where
  preserves {c} hc :=
    let ⟨_⟩ := nonempty_fintype J
    ⟨IsColimit.ofIsoColimit
        ((IsColimit.precomposeHomEquiv (Discrete.compNatIsoDiscrete _ _) _).symm
          (isBilimitOfPreserves F (biconeIsBilimitOfColimitCoconeOfIsColimit hc)).isColimit) <|
      Cocones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Preservation of Coproducts by Biproduct-Preserving Functors in Preadditive Categories

Informal description

Let $ C $ and $ D $ be preadditive categories, and let $ F \colon C \to D $ be a functor that preserves zero morphisms. If $ F $ preserves the biproduct of a family of objects $ f \colon J \to C $, then $ F $ preserves the coproduct of $ f $.

CategoryTheory.Limits.preservesCoproductsOfShape_of_preservesBiproductsOfShape theorem

[PreservesBiproductsOfShape J F] : PreservesColimitsOfShape (Discrete J) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
    preserves finite coproducts. -/
lemma preservesCoproductsOfShape_of_preservesBiproductsOfShape [PreservesBiproductsOfShape J F] :
    PreservesColimitsOfShape (Discrete J) F where
  preservesColimit {_} := preservesColimit_of_iso_diagram _ Discrete.natIsoFunctor.symm

Preservation of Coproducts by Biproduct-Preserving Functors in Preadditive Categories

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be preadditive categories, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor that preserves zero morphisms. If $F$ preserves all biproducts of shape $J$ (where $J$ is a finite discrete category), then $F$ preserves all coproducts of shape $J$.

CategoryTheory.Limits.preservesBiproduct_of_preservesCoproduct theorem

{f : J → C} [PreservesColimit (Discrete.functor f) F] : PreservesBiproduct f F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
    preserves finite biproducts. -/
lemma preservesBiproduct_of_preservesCoproduct {f : J → C}
    [PreservesColimit (Discrete.functor f) F] :
    PreservesBiproduct f F where
  preserves {b} hb :=
    let ⟨_⟩ := nonempty_fintype J
    ⟨isBilimitOfIsColimit _ <|
      IsColimit.ofIsoColimit
          ((IsColimit.precomposeInvEquiv (Discrete.compNatIsoDiscrete _ _)
                (F.mapCocone b.toCocone)).symm
            (isColimitOfPreserves F hb.isColimit)) <|
        Cocones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Preservation of biproducts by coproduct-preserving functors in preadditive categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves the coproduct of a family of objects $f \colon J \to C$, then $F$ preserves the biproduct of $f$.

CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape theorem

[PreservesColimitsOfShape (Discrete J) F] : PreservesBiproductsOfShape J F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
    preserves finite biproducts. -/
lemma preservesBiproductsOfShape_of_preservesCoproductsOfShape
    [PreservesColimitsOfShape (Discrete J) F] : PreservesBiproductsOfShape J F where
  preserves {_} := preservesBiproduct_of_preservesCoproduct F

Preservation of Biproducts via Coproduct Preservation in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves all coproducts of shape $J$ (where $J$ is a discrete category), then $F$ preserves all biproducts of shape $J$.

CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct theorem

{X Y : C} [PreservesBinaryBiproduct X Y F] : PreservesLimit (pair X Y) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
    preserves binary products. -/
lemma preservesBinaryProduct_of_preservesBinaryBiproduct {X Y : C}
    [PreservesBinaryBiproduct X Y F] :
    PreservesLimit (pair X Y) F where
  preserves {c} hc := ⟨IsLimit.ofIsoLimit
        ((IsLimit.postcomposeInvEquiv (diagramIsoPair _) _).symm
          (isBinaryBilimitOfPreserves F (binaryBiconeIsBilimitOfLimitConeOfIsLimit hc)).isLimit) <|
      Cones.ext (by dsimp; rfl) fun j => by
        rcases j with ⟨⟨⟩⟩ <;> simp⟩

Preservation of Binary Products via Binary Biproduct Preservation in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves the binary biproduct of two objects $X$ and $Y$ in $C$, then $F$ also preserves their binary product.

CategoryTheory.Limits.preservesBinaryProducts_of_preservesBinaryBiproducts theorem

[PreservesBinaryBiproducts F] : PreservesLimitsOfShape (Discrete WalkingPair) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
    preserves binary products. -/
lemma preservesBinaryProducts_of_preservesBinaryBiproducts [PreservesBinaryBiproducts F] :
    PreservesLimitsOfShape (Discrete WalkingPair) F where
  preservesLimit {_} := preservesLimit_of_iso_diagram _ (diagramIsoPair _).symm

Preservation of Binary Products via Binary Biproduct Preservation in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves all binary biproducts, then $F$ preserves all binary products. That is, $F$ preserves limits of shape `Discrete WalkingPair`.

CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct theorem

{X Y : C} [PreservesLimit (pair X Y) F] : PreservesBinaryBiproduct X Y F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
    preserves binary biproducts. -/
lemma preservesBinaryBiproduct_of_preservesBinaryProduct {X Y : C} [PreservesLimit (pair X Y) F] :
    PreservesBinaryBiproduct X Y F where
  preserves {b} hb := ⟨isBinaryBilimitOfIsLimit _ <| IsLimit.ofIsoLimit
          ((IsLimit.postcomposeHomEquiv (diagramIsoPair _) (F.mapCone b.toCone)).symm
            (isLimitOfPreserves F hb.isLimit)) <|
        Cones.ext (by dsimp; rfl) fun j => by
          rcases j with ⟨⟨⟩⟩ <;> simp⟩

Preservation of Binary Biproducts via Binary Product Preservation in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves the binary product of two objects $X$ and $Y$ in $C$, then $F$ also preserves their binary biproduct.

CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison theorem

 {X Y : C} [HasBinaryBiproduct X Y] [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Mono (biprodComparison F X Y)] :
  PreservesBinaryBiproduct X Y F

Full source

/-- If the (product-like) biproduct comparison for `F`, `X` and `Y` is a monomorphism, then
    `F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`. -/
lemma preservesBinaryBiproduct_of_mono_biprodComparison {X Y : C} [HasBinaryBiproduct X Y]
    [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Mono (biprodComparison F X Y)] :
    PreservesBinaryBiproduct X Y F := by
  have that :
    prodComparison F X Y =
      (F.mapIso (biprod.isoProd X Y)).inv ≫ biprodComparison F X Y ≫ (biprod.isoProd _ _).hom := by
    ext <;> simp [← Functor.map_comp]
  haveI : IsIso (biprodComparison F X Y) := isIso_of_mono_of_isSplitEpi _
  haveI : IsIso (prodComparison F X Y) := by
    rw [that]
    infer_instance
  haveI := PreservesLimitPair.of_iso_prod_comparison F X Y
  apply preservesBinaryBiproduct_of_preservesBinaryProduct

Preservation of Binary Biproducts via Monomorphic Biproduct Comparison

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be preadditive categories with binary biproducts, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor that preserves zero morphisms. For objects $X$ and $Y$ in $\mathcal{C}$, if the biproduct comparison morphism $F(X \oplus Y) \to F(X) \oplus F(Y)$ is a monomorphism, then $F$ preserves the binary biproduct of $X$ and $Y$.

CategoryTheory.Limits.preservesBinaryBiproduct_of_epi_biprodComparison' theorem

 {X Y : C} [HasBinaryBiproduct X Y] [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Epi (biprodComparison' F X Y)] :
  PreservesBinaryBiproduct X Y F

Full source

/-- If the (coproduct-like) biproduct comparison for `F`, `X` and `Y` is an epimorphism, then
    `F` preserves the biproduct of `X` and `Y`. For the converse, see `mapBiprod`. -/
lemma preservesBinaryBiproduct_of_epi_biprodComparison' {X Y : C} [HasBinaryBiproduct X Y]
    [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Epi (biprodComparison' F X Y)] :
    PreservesBinaryBiproduct X Y F := by
  haveI : Epi (splitEpiBiprodComparison F X Y).section_ := by simpa
  haveI : IsIso (biprodComparison F X Y) :=
    IsIso.of_epi_section' (splitEpiBiprodComparison F X Y)
  apply preservesBinaryBiproduct_of_mono_biprodComparison

Preservation of Binary Biproducts via Epimorphic Biproduct Comparison Morphism

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be preadditive categories with binary biproducts, and let $F \colon \mathcal{C} \to \mathcal{D}$ be a functor that preserves zero morphisms. For objects $X$ and $Y$ in $\mathcal{C}$, if the biproduct comparison morphism $F(X) \oplus F(Y) \to F(X \oplus Y)$ is an epimorphism, then $F$ preserves the binary biproduct of $X$ and $Y$.

CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts theorem

[PreservesLimitsOfShape (Discrete WalkingPair) F] : PreservesBinaryBiproducts F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
    preserves binary biproducts. -/
lemma preservesBinaryBiproducts_of_preservesBinaryProducts
    [PreservesLimitsOfShape (Discrete WalkingPair) F] : PreservesBinaryBiproducts F where
  preserves {_} {_} := preservesBinaryBiproduct_of_preservesBinaryProduct F

Preservation of Binary Biproducts via Binary Product Preservation in Preadditive Categories

Informal description

Let $C$ and $D$ be preadditive categories, and let $F \colon C \to D$ be a functor that preserves zero morphisms. If $F$ preserves all binary products (i.e., it preserves limits of shape `Discrete WalkingPair`), then $F$ preserves all binary biproducts.

CategoryTheory.Limits.preservesBinaryCoproduct_of_preservesBinaryBiproduct theorem

{X Y : C} [PreservesBinaryBiproduct X Y F] : PreservesColimit (pair X Y) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
    preserves binary coproducts. -/
lemma preservesBinaryCoproduct_of_preservesBinaryBiproduct {X Y : C}
    [PreservesBinaryBiproduct X Y F] :
    PreservesColimit (pair X Y) F where
  preserves {c} hc :=
    ⟨IsColimit.ofIsoColimit
        ((IsColimit.precomposeHomEquiv (diagramIsoPair _) _).symm
          (isBinaryBilimitOfPreserves F
              (binaryBiconeIsBilimitOfColimitCoconeOfIsColimit hc)).isColimit) <|
      Cocones.ext (by dsimp; rfl) fun j => by
        rcases j with ⟨⟨⟩⟩ <;> simp⟩

Preservation of Binary Coproducts by a Biproduct-Preserving Functor

Informal description

Let $F \colon C \to D$ be a functor between preadditive categories that preserves zero morphisms and binary biproducts. Then for any objects $X$ and $Y$ in $C$, the functor $F$ preserves the binary coproduct of $X$ and $Y$. That is, if $F$ preserves the biproduct $X \oplus Y$, then it also preserves the coproduct $X \sqcup Y$.

CategoryTheory.Limits.preservesBinaryCoproducts_of_preservesBinaryBiproducts theorem

[PreservesBinaryBiproducts F] : PreservesColimitsOfShape (Discrete WalkingPair) F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
    preserves binary coproducts. -/
lemma preservesBinaryCoproducts_of_preservesBinaryBiproducts [PreservesBinaryBiproducts F] :
    PreservesColimitsOfShape (Discrete WalkingPair) F where
  preservesColimit {_} := preservesColimit_of_iso_diagram _ (diagramIsoPair _).symm

Preservation of Binary Coproducts by a Biproduct-Preserving Functor

Informal description

Let $F \colon C \to D$ be a functor between preadditive categories that preserves zero morphisms and binary biproducts. Then $F$ preserves all binary coproducts. That is, for any pair of objects $X$ and $Y$ in $C$, the functor $F$ preserves their coproduct $X \sqcup Y$.

CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryCoproduct theorem

{X Y : C} [PreservesColimit (pair X Y) F] : PreservesBinaryBiproduct X Y F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary coproducts
    preserves binary biproducts. -/
lemma preservesBinaryBiproduct_of_preservesBinaryCoproduct {X Y : C}
    [PreservesColimit (pair X Y) F] :
    PreservesBinaryBiproduct X Y F where
  preserves {b} hb :=
    ⟨isBinaryBilimitOfIsColimit _ <|
      IsColimit.ofIsoColimit
          ((IsColimit.precomposeInvEquiv (diagramIsoPair _) (F.mapCocone b.toCocone)).symm
            (isColimitOfPreserves F hb.isColimit)) <|
        Cocones.ext (Iso.refl _) fun j => by
          rcases j with ⟨⟨⟩⟩ <;> simp⟩

Preservation of Binary Biproducts by Coproduct-Preserving Functors

Informal description

Let $F \colon C \to D$ be a functor between preadditive categories that preserves zero morphisms. If $F$ preserves the binary coproduct of objects $X$ and $Y$ in $C$, then it also preserves their binary biproduct.

CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts theorem

[PreservesColimitsOfShape (Discrete WalkingPair) F] : PreservesBinaryBiproducts F

Full source

/-- A functor between preadditive categories that preserves (zero morphisms and) binary coproducts
    preserves binary biproducts. -/
lemma preservesBinaryBiproducts_of_preservesBinaryCoproducts
    [PreservesColimitsOfShape (Discrete WalkingPair) F] : PreservesBinaryBiproducts F where
  preserves {_} {_} := preservesBinaryBiproduct_of_preservesBinaryCoproduct F

Preservation of Binary Biproducts by Coproduct-Preserving Functors in Preadditive Categories

Informal description

Let $F \colon C \to D$ be a functor between preadditive categories that preserves zero morphisms. If $F$ preserves all binary coproducts (i.e., it preserves colimits of shape $\mathrm{Discrete}\,\mathrm{WalkingPair}$), then $F$ preserves all binary biproducts.