Basic facts about biproducts in preadditive categories.

In (or between) preadditive categories,

• Any biproduct satisfies the equality total : ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f), or, in the binary case, total : fst ≫ inl + snd ≫ inr = 𝟙 X.

• Any (binary) product or (binary) coproduct is a (binary) biproduct.

• In any category (with zero morphisms), if biprod.map f g is an isomorphism, then both f and g are isomorphisms.

• 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.

• As a corollary of the previous two facts, if we have an isomorphism X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂ whose X₁ ⟶ Y₁ entry is an isomorphism, we can construct an isomorphism X₂ ≅ Y₂.

• If f : W ⊞ X ⟶ Y ⊞ Z is an isomorphism, either 𝟙 W = 0, or at least one of the component maps W ⟶ Y and W ⟶ Z is nonzero.

• If f : ⨁ S ⟶ ⨁ T is an isomorphism, then every column (corresponding to a nonzero summand in the domain) has some nonzero matrix entry.

• A functor preserves a biproduct if and only if it preserves the corresponding product if and only if it preserves the corresponding coproduct.

There are connections between this material and the special case of the category whose morphisms are matrices over a ring, in particular the Schur complement (see Mathlib.LinearAlgebra.Matrix.SchurComplement). In particular, the declarations CategoryTheory.Biprod.isoElim, CategoryTheory.Biprod.gaussian and Matrix.invertibleOfFromBlocks₁₁Invertible are all closely related.

def CategoryTheory.Limits.isBilimitOfTotal {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} (b : Bicone f) (total : ∑ j : J, CategoryStruct.comp (b.π j) (b.ι j) = CategoryStruct.id b.pt) : b.IsBilimit

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.)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.IsBilimit.total {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} {b : Bicone f} (i : b.IsBilimit) : ∑ j : J, CategoryStruct.comp (b.π j) (b.ι j) = CategoryStruct.id b.pt

theorem CategoryTheory.Limits.hasBiproduct_of_total {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} (b : Bicone f) (total : ∑ j : J, CategoryStruct.comp (b.π j) (b.ι j) = CategoryStruct.id b.pt) : HasBiproduct f

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 CategoryTheory.Limits.isBilimitOfIsLimit {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} (t : Bicone f) (ht : IsLimit t.toCone) : t.IsBilimit

In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.

Equations

• CategoryTheory.Limits.isBilimitOfIsLimit t ht = CategoryTheory.Limits.isBilimitOfTotal t ⋯

def CategoryTheory.Limits.biconeIsBilimitOfLimitConeOfIsLimit {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} {t : Cone (Discrete.functor f)} (ht : IsLimit t) : (Bicone.ofLimitCone ht).IsBilimit

We can turn any limit cone over a pair into a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.isBilimitOfIsColimit {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} (t : Bicone f) (ht : IsColimit t.toCocone) : t.IsBilimit

In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.

Equations

• CategoryTheory.Limits.isBilimitOfIsColimit t ht = CategoryTheory.Limits.isBilimitOfTotal t ⋯

def CategoryTheory.Limits.biconeIsBilimitOfColimitCoconeOfIsColimit {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} {t : Cocone (Discrete.functor f)} (ht : IsColimit t) : (Bicone.ofColimitCocone ht).IsBilimit

We can turn any limit cone over a pair into a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.HasBiproduct.of_hasProduct {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Finite J] (f : J → C) [HasProduct f] : HasBiproduct f

In a preadditive category, if the product over f : J → C exists, then the biproduct over f exists.

theorem CategoryTheory.Limits.HasBiproduct.of_hasCoproduct {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Finite J] (f : J → C) [HasCoproduct f] : HasBiproduct f

In a preadditive category, if the coproduct over f : J → C exists, then the biproduct over f exists.

theorem CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts {C : Type u} [Category.{v, u} C] [Preadditive C] [HasFiniteProducts C] : HasFiniteBiproducts C

A preadditive category with finite products has finite biproducts.

theorem CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts {C : Type u} [Category.{v, u} C] [Preadditive C] [HasFiniteCoproducts C] : HasFiniteBiproducts C

A preadditive category with finite coproducts has finite biproducts.

@[simp]

theorem CategoryTheory.Limits.biproduct.total {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} [HasBiproduct f] : ∑ j : J, CategoryStruct.comp (π f j) (ι f j) = CategoryStruct.id (⨁ f)

In any preadditive category, any biproduct satisfies ∑ j : J, biproduct.π f j ≫ biproduct.ι f j = 𝟙 (⨁ f)

theorem CategoryTheory.Limits.biproduct.lift_eq {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} [HasBiproduct f] {T : C} {g : (j : J) → T ⟶ f j} : lift g = ∑ j : J, CategoryStruct.comp (g j) (ι f j)

theorem CategoryTheory.Limits.biproduct.desc_eq {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} [HasBiproduct f] {T : C} {g : (j : J) → f j ⟶ T} : desc g = ∑ j : J, CategoryStruct.comp (π f j) (g j)

theorem CategoryTheory.Limits.biproduct.lift_desc {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} [HasBiproduct f] {T U : C} {g : (j : J) → T ⟶ f j} {h : (j : J) → f j ⟶ U} : CategoryStruct.comp (lift g) (desc h) = ∑ j : J, CategoryStruct.comp (g j) (h j)

theorem CategoryTheory.Limits.biproduct.lift_desc_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {f : J → C} [HasBiproduct f] {T U : C} {g : (j : J) → T ⟶ f j} {h : (j : J) → f j ⟶ U} {Z : C} (h✝ : U ⟶ Z) : CategoryStruct.comp (lift g) (CategoryStruct.comp (desc h) h✝) = CategoryStruct.comp (∑ j : J, CategoryStruct.comp (g j) (h j)) h✝

theorem CategoryTheory.Limits.biproduct.map_eq {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] [HasFiniteBiproducts C] {f g : J → C} {h : (j : J) → f j ⟶ g j} : map h = ∑ j : J, CategoryStruct.comp (π f j) (CategoryStruct.comp (h j) (ι g j))

theorem CategoryTheory.Limits.biproduct.lift_matrix {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {K : Type} [Finite K] [HasFiniteBiproducts C] {f : J → C} {g : K → C} {P : C} (x : (j : J) → P ⟶ f j) (m : (j : J) → (k : K) → f j ⟶ g k) : CategoryStruct.comp (lift x) (matrix m) = lift fun (k : K) => ∑ j : J, CategoryStruct.comp (x j) (m j k)

theorem CategoryTheory.Limits.biproduct.lift_matrix_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {J : Type} [Fintype J] {K : Type} [Finite K] [HasFiniteBiproducts C] {f : J → C} {g : K → C} {P : C} (x : (j : J) → P ⟶ f j) (m : (j : J) → (k : K) → f j ⟶ g k) {Z : C} (h : ⨁ g ⟶ Z) : CategoryStruct.comp (lift x) (CategoryStruct.comp (matrix m) h) = CategoryStruct.comp (lift fun (k : K) => ∑ j : J, CategoryStruct.comp (x j) (m j k)) h

theorem CategoryTheory.Limits.biproduct.matrix_desc {C : Type u} [Category.{v, u} C] [Preadditive C] {J K : Type} [Finite J] [HasFiniteBiproducts C] [Fintype K] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) {P : C} (x : (k : K) → g k ⟶ P) : CategoryStruct.comp (matrix m) (desc x) = desc fun (j : J) => ∑ k : K, CategoryStruct.comp (m j k) (x k)

theorem CategoryTheory.Limits.biproduct.matrix_desc_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {J K : Type} [Finite J] [HasFiniteBiproducts C] [Fintype K] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) {P : C} (x : (k : K) → g k ⟶ P) {Z : C} (h : P ⟶ Z) : CategoryStruct.comp (matrix m) (CategoryStruct.comp (desc x) h) = CategoryStruct.comp (desc fun (j : J) => ∑ k : K, CategoryStruct.comp (m j k) (x k)) h

theorem CategoryTheory.Limits.biproduct.matrix_map {C : Type u} [Category.{v, u} C] [Preadditive C] {J K : Type} [Finite J] [HasFiniteBiproducts C] [Finite K] {f : J → C} {g h : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (n : (k : K) → g k ⟶ h k) : CategoryStruct.comp (matrix m) (map n) = matrix fun (j : J) (k : K) => CategoryStruct.comp (m j k) (n k)

theorem CategoryTheory.Limits.biproduct.matrix_map_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {J K : Type} [Finite J] [HasFiniteBiproducts C] [Finite K] {f : J → C} {g h : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (n : (k : K) → g k ⟶ h k) {Z : C} (h✝ : ⨁ h ⟶ Z) : CategoryStruct.comp (matrix m) (CategoryStruct.comp (map n) h✝) = CategoryStruct.comp (matrix fun (j : J) (k : K) => CategoryStruct.comp (m j k) (n k)) h✝

theorem CategoryTheory.Limits.biproduct.map_matrix {C : Type u} [Category.{v, u} C] [Preadditive C] {J K : Type} [Finite J] [HasFiniteBiproducts C] [Finite K] {f g : J → C} {h : K → C} (m : (k : J) → f k ⟶ g k) (n : (j : J) → (k : K) → g j ⟶ h k) : CategoryStruct.comp (map m) (matrix n) = matrix fun (j : J) (k : K) => CategoryStruct.comp (m j) (n j k)

theorem CategoryTheory.Limits.biproduct.map_matrix_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {J K : Type} [Finite J] [HasFiniteBiproducts C] [Finite K] {f g : J → C} {h : K → C} (m : (k : J) → f k ⟶ g k) (n : (j : J) → (k : K) → g j ⟶ h k) {Z : C} (h✝ : ⨁ h ⟶ Z) : CategoryStruct.comp (map m) (CategoryStruct.comp (matrix n) h✝) = CategoryStruct.comp (matrix fun (j : J) (k : K) => CategoryStruct.comp (m j) (n j k)) h✝

def CategoryTheory.Limits.biproduct.reindex {C : Type u} [Category.{v, u} C] [Preadditive C] {β γ : Type} [Finite β] (ε : β ≃ γ) (f : γ → C) [HasBiproduct f] [HasBiproduct (f ∘ ⇑ε)] : ⨁ f ∘ ⇑ε ≅ ⨁ f

Reindex a categorical biproduct via an equivalence of the index types.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.biproduct.reindex_hom {C : Type u} [Category.{v, u} C] [Preadditive C] {β γ : Type} [Finite β] (ε : β ≃ γ) (f : γ → C) [HasBiproduct f] [HasBiproduct (f ∘ ⇑ε)] : (reindex ε f).hom = desc fun (b : β) => ι f (ε b)

@[simp]

theorem CategoryTheory.Limits.biproduct.reindex_inv {C : Type u} [Category.{v, u} C] [Preadditive C] {β γ : Type} [Finite β] (ε : β ≃ γ) (f : γ → C) [HasBiproduct f] [HasBiproduct (f ∘ ⇑ε)] : (reindex ε f).inv = lift fun (b : β) => π f (ε b)

def CategoryTheory.Limits.isBinaryBilimitOfTotal {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (b : BinaryBicone X Y) (total : CategoryStruct.comp b.fst b.inl + CategoryStruct.comp b.snd b.inr = CategoryStruct.id b.pt) : b.IsBilimit

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.)

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.IsBilimit.binary_total {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {b : BinaryBicone X Y} (i : b.IsBilimit) : CategoryStruct.comp b.fst b.inl + CategoryStruct.comp b.snd b.inr = CategoryStruct.id b.pt

theorem CategoryTheory.Limits.hasBinaryBiproduct_of_total {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (b : BinaryBicone X Y) (total : CategoryStruct.comp b.fst b.inl + CategoryStruct.comp b.snd b.inr = CategoryStruct.id b.pt) : HasBinaryBiproduct X Y

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 CategoryTheory.Limits.BinaryBicone.ofLimitCone {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : BinaryBicone X Y

We can turn any limit cone over a pair into a bicone.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofLimitCone_pt {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : (ofLimitCone ht).pt = t.pt

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofLimitCone_inl {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : (ofLimitCone ht).inl = ht.lift (BinaryFan.mk (CategoryStruct.id X) 0)

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofLimitCone_inr {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : (ofLimitCone ht).inr = ht.lift (BinaryFan.mk 0 (CategoryStruct.id Y))

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofLimitCone_snd {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : (ofLimitCone ht).snd = t.π.app { as := WalkingPair.right }

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofLimitCone_fst {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : (ofLimitCone ht).fst = t.π.app { as := WalkingPair.left }

theorem CategoryTheory.Limits.inl_of_isLimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) : t.inl = ht.lift (BinaryFan.mk (CategoryStruct.id X) 0)

theorem CategoryTheory.Limits.inr_of_isLimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) : t.inr = ht.lift (BinaryFan.mk 0 (CategoryStruct.id Y))

def CategoryTheory.Limits.isBinaryBilimitOfIsLimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (t : BinaryBicone X Y) (ht : IsLimit t.toCone) : t.IsBilimit

In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.

Equations

• CategoryTheory.Limits.isBinaryBilimitOfIsLimit t ht = CategoryTheory.Limits.isBinaryBilimitOfTotal t ⋯

def CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cone (pair X Y)} (ht : IsLimit t) : (BinaryBicone.ofLimitCone ht).IsBilimit

We can turn any limit cone over a pair into a bilimit bicone.

Equations

• CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit ht = CategoryTheory.Limits.isBinaryBilimitOfTotal (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht) ⋯

theorem CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct {C : Type u} [Category.{v, u} C] [Preadditive C] (X Y : C) [HasBinaryProduct X Y] : HasBinaryBiproduct X Y

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

theorem CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts {C : Type u} [Category.{v, u} C] [Preadditive C] [HasBinaryProducts C] : HasBinaryBiproducts C

In a preadditive category, if all binary products exist, then all binary biproducts exist.

def CategoryTheory.Limits.BinaryBicone.ofColimitCocone {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : BinaryBicone X Y

We can turn any colimit cocone over a pair into a bicone.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inr {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : (ofColimitCocone ht).inr = t.ι.app { as := WalkingPair.right }

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofColimitCocone_pt {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : (ofColimitCocone ht).pt = t.pt

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inl {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : (ofColimitCocone ht).inl = t.ι.app { as := WalkingPair.left }

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofColimitCocone_fst {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : (ofColimitCocone ht).fst = ht.desc (BinaryCofan.mk (CategoryStruct.id X) 0)

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.ofColimitCocone_snd {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : (ofColimitCocone ht).snd = ht.desc (BinaryCofan.mk 0 (CategoryStruct.id Y))

theorem CategoryTheory.Limits.fst_of_isColimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) : t.fst = ht.desc (BinaryCofan.mk (CategoryStruct.id X) 0)

theorem CategoryTheory.Limits.snd_of_isColimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) : t.snd = ht.desc (BinaryCofan.mk 0 (CategoryStruct.id Y))

def CategoryTheory.Limits.isBinaryBilimitOfIsColimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (t : BinaryBicone X Y) (ht : IsColimit t.toCocone) : t.IsBilimit

In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.

Equations

• CategoryTheory.Limits.isBinaryBilimitOfIsColimit t ht = CategoryTheory.Limits.isBinaryBilimitOfTotal t ⋯

def CategoryTheory.Limits.binaryBiconeIsBilimitOfColimitCoconeOfIsColimit {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {t : Cocone (pair X Y)} (ht : IsColimit t) : (BinaryBicone.ofColimitCocone ht).IsBilimit

We can turn any colimit cocone over a pair into a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct {C : Type u} [Category.{v, u} C] [Preadditive C] (X Y : C) [HasBinaryCoproduct X Y] : HasBinaryBiproduct X Y

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

theorem CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts {C : Type u} [Category.{v, u} C] [Preadditive C] [HasBinaryCoproducts C] : HasBinaryBiproducts C

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

@[simp]

theorem CategoryTheory.Limits.biprod.total {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] : CategoryStruct.comp fst inl + CategoryStruct.comp snd inr = CategoryStruct.id (X ⊞ Y)

In any preadditive category, any binary biproduct satisfies biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y).

theorem CategoryTheory.Limits.biprod.lift_eq {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {T : C} {f : T ⟶ X} {g : T ⟶ Y} : lift f g = CategoryStruct.comp f inl + CategoryStruct.comp g inr

theorem CategoryTheory.Limits.biprod.desc_eq {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {T : C} {f : X ⟶ T} {g : Y ⟶ T} : desc f g = CategoryStruct.comp fst f + CategoryStruct.comp snd g

@[simp]

theorem CategoryTheory.Limits.biprod.lift_desc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U} : CategoryStruct.comp (lift f g) (desc h i) = CategoryStruct.comp f h + CategoryStruct.comp g i

@[simp]

theorem CategoryTheory.Limits.biprod.lift_desc_assoc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U} {Z : C} (h✝ : U ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (desc h i) h✝) = CategoryStruct.comp (CategoryStruct.comp f h + CategoryStruct.comp g i) h✝

theorem CategoryTheory.Limits.biprod.map_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [HasBinaryBiproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z} : map f g = CategoryStruct.comp fst (CategoryStruct.comp f inl) + CategoryStruct.comp snd (CategoryStruct.comp g inr)

theorem CategoryTheory.Limits.biprod.decomp_hom_to {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} (f : Z ⟶ X ⊞ Y) : ∃ (f₁ : Z ⟶ X) (f₂ : Z ⟶ Y), f = CategoryStruct.comp f₁ inl + CategoryStruct.comp f₂ inr

theorem CategoryTheory.Limits.biprod.ext_to_iff {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} {f g : Z ⟶ X ⊞ Y} : f = g ↔ CategoryStruct.comp f fst = CategoryStruct.comp g fst ∧ CategoryStruct.comp f snd = CategoryStruct.comp g snd

theorem CategoryTheory.Limits.biprod.decomp_hom_from {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} (f : X ⊞ Y ⟶ Z) : ∃ (f₁ : X ⟶ Z) (f₂ : Y ⟶ Z), f = CategoryStruct.comp fst f₁ + CategoryStruct.comp snd f₂

theorem CategoryTheory.Limits.biprod.ext_from_iff {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} {f g : X ⊞ Y ⟶ Z} : f = g ↔ CategoryStruct.comp inl f = CategoryStruct.comp inl g ∧ CategoryStruct.comp inr f = CategoryStruct.comp inr g

def CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : BinaryBicone X c.pt

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : (binaryBiconeOfIsSplitMonoOfCokernel i).pt = Y

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : (binaryBiconeOfIsSplitMonoOfCokernel i).snd = Cofork.π c

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : (binaryBiconeOfIsSplitMonoOfCokernel i).inr = let c' := CokernelCofork.ofπ (Cofork.π c) ⋯; let i' := isCokernelEpiComp i (retraction f) ⋯; let i'' := Preadditive.isColimitCoforkOfCokernelCofork i'; (splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : (binaryBiconeOfIsSplitMonoOfCokernel i).inl = f

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : (binaryBiconeOfIsSplitMonoOfCokernel i).fst = retraction f

def CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitMono f] {c : CokernelCofork f} (i : IsColimit c) : (binaryBiconeOfIsSplitMonoOfCokernel i).IsBilimit

The bicone constructed in binaryBiconeOfSplitMonoOfCokernel is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories.

Equations

• CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel i = CategoryTheory.Limits.isBinaryBilimitOfTotal (CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel i) ⋯

def CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInl {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (b : BinaryBicone X Y) (hb : IsLimit b.sndKernelFork) : b.IsBilimit

If b is a binary bicone such that b.inl is a kernel of b.snd, then b is a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryBicone.isBilimitOfKernelInr {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (b : BinaryBicone X Y) (hb : IsLimit b.fstKernelFork) : b.IsBilimit

If b is a binary bicone such that b.inr is a kernel of b.fst, then b is a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (b : BinaryBicone X Y) (hb : IsColimit b.inrCokernelCofork) : b.IsBilimit

If b is a binary bicone such that b.fst is a cokernel of b.inr, then b is a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelSnd {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (b : BinaryBicone X Y) (hb : IsColimit b.inlCokernelCofork) : b.IsBilimit

If b is a binary bicone such that b.snd is a cokernel of b.inl, then b is a bilimit bicone.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : BinaryBicone c.pt Y

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : (binaryBiconeOfIsSplitEpiOfKernel i).inl = Fork.ι c

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_pt {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : (binaryBiconeOfIsSplitEpiOfKernel i).pt = X

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_snd {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : (binaryBiconeOfIsSplitEpiOfKernel i).snd = f

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inr {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : (binaryBiconeOfIsSplitEpiOfKernel i).inr = section_ f

@[simp]

theorem CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fst {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : (binaryBiconeOfIsSplitEpiOfKernel i).fst = let c' := KernelFork.ofι (Fork.ι c) ⋯; let i' := isKernelCompMono i (section_ f) ⋯; let i'' := Preadditive.isLimitForkOfKernelFork i'; (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction

def CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} {f : X ⟶ Y} [IsSplitEpi f] {c : KernelFork f} (i : IsLimit c) : (binaryBiconeOfIsSplitEpiOfKernel i).IsBilimit

The bicone constructed in binaryBiconeOfIsSplitEpiOfKernel is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.biprod.add_eq_lift_id_desc {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [HasBinaryBiproduct X X] : f + g = CategoryStruct.comp (lift (CategoryStruct.id X) (CategoryStruct.id X)) (desc f g)

The existence of binary biproducts implies that there is at most one preadditive structure.

theorem CategoryTheory.Limits.biprod.add_eq_lift_desc_id {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (f g : X ⟶ Y) [HasBinaryBiproduct Y Y] : f + g = CategoryStruct.comp (lift f g) (desc (CategoryStruct.id Y) (CategoryStruct.id Y))

The existence of binary biproducts implies that there is at most one preadditive structure.

theorem CategoryTheory.Preadditive.ext {C : Type u} {inst✝ : Category.{v, u} C} {x y : Preadditive C} (homGroup : homGroup = homGroup) : x = y

theorem CategoryTheory.Preadditive.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {x y : Preadditive C} : x = y ↔ homGroup = homGroup

instance CategoryTheory.subsingleton_preadditive_of_hasBinaryBiproducts {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] : Subsingleton (Preadditive C)

The existence of binary biproducts implies that there is at most one preadditive structure.

def CategoryTheory.Biprod.ofComponents {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂

The "matrix" morphism X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ with specified components.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Biprod.inl_ofComponents {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) : CategoryStruct.comp Limits.biprod.inl (ofComponents f₁₁ f₁₂ f₂₁ f₂₂) = CategoryStruct.comp f₁₁ Limits.biprod.inl + CategoryStruct.comp f₁₂ Limits.biprod.inr

@[simp]

theorem CategoryTheory.Biprod.inr_ofComponents {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) : CategoryStruct.comp Limits.biprod.inr (ofComponents f₁₁ f₁₂ f₂₁ f₂₂) = CategoryStruct.comp f₂₁ Limits.biprod.inl + CategoryStruct.comp f₂₂ Limits.biprod.inr

@[simp]

theorem CategoryTheory.Biprod.ofComponents_fst {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) : CategoryStruct.comp (ofComponents f₁₁ f₁₂ f₂₁ f₂₂) Limits.biprod.fst = CategoryStruct.comp Limits.biprod.fst f₁₁ + CategoryStruct.comp Limits.biprod.snd f₂₁

@[simp]

theorem CategoryTheory.Biprod.ofComponents_snd {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) : CategoryStruct.comp (ofComponents f₁₁ f₁₂ f₂₁ f₂₂) Limits.biprod.snd = CategoryStruct.comp Limits.biprod.fst f₁₂ + CategoryStruct.comp Limits.biprod.snd f₂₂

@[simp]

theorem CategoryTheory.Biprod.ofComponents_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) : ofComponents (CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp f Limits.biprod.fst)) (CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp f Limits.biprod.snd)) (CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp f Limits.biprod.fst)) (CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp f Limits.biprod.snd)) = f

@[simp]

theorem CategoryTheory.Biprod.ofComponents_comp {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {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₂) : CategoryStruct.comp (ofComponents f₁₁ f₁₂ f₂₁ f₂₂) (ofComponents g₁₁ g₁₂ g₂₁ g₂₂) = ofComponents (CategoryStruct.comp f₁₁ g₁₁ + CategoryStruct.comp f₁₂ g₂₁) (CategoryStruct.comp f₁₁ g₁₂ + CategoryStruct.comp f₁₂ g₂₂) (CategoryStruct.comp f₂₁ g₁₁ + CategoryStruct.comp f₂₂ g₂₁) (CategoryStruct.comp f₂₁ g₁₂ + CategoryStruct.comp f₂₂ g₂₂)

def CategoryTheory.Biprod.unipotentUpper {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₁ ⟶ X₂) : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂

The unipotent upper triangular matrix

(1 r)
(0 1)

as an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Biprod.unipotentUpper_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₁ ⟶ X₂) : (unipotentUpper r).hom = ofComponents (CategoryStruct.id X₁) r 0 (CategoryStruct.id X₂)

@[simp]

theorem CategoryTheory.Biprod.unipotentUpper_inv {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₁ ⟶ X₂) : (unipotentUpper r).inv = ofComponents (CategoryStruct.id X₁) (-r) 0 (CategoryStruct.id X₂)

def CategoryTheory.Biprod.unipotentLower {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₂ ⟶ X₁) : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂

The unipotent lower triangular matrix

(1 0)
(r 1)

as an isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Biprod.unipotentLower_hom {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₂ ⟶ X₁) : (unipotentLower r).hom = ofComponents (CategoryStruct.id X₁) 0 r (CategoryStruct.id X₂)

@[simp]

theorem CategoryTheory.Biprod.unipotentLower_inv {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ : C} (r : X₂ ⟶ X₁) : (unipotentLower r).inv = ofComponents (CategoryStruct.id X₁) 0 (-r) (CategoryStruct.id X₂)

def CategoryTheory.Biprod.gaussian' {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) [IsIso f₁₁] : (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×' (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' CategoryStruct.comp L.hom (CategoryStruct.comp (ofComponents f₁₁ f₁₂ f₂₁ f₂₂) R.hom) = Limits.biprod.map f₁₁ g₂₂

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.)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Biprod.gaussian {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) [IsIso (CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp f Limits.biprod.fst))] : (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×' (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' CategoryStruct.comp L.hom (CategoryStruct.comp f R.hom) = Limits.biprod.map (CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp f Limits.biprod.fst)) g₂₂

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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Biprod.isoElim' {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂) (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) [IsIso f₁₁] [IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)] : X₂ ≅ Y₂

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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Biprod.isoElim {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂) [IsIso (CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp f.hom Limits.biprod.fst))] : X₂ ≅ Y₂

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.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Biprod.column_nonzero_of_iso {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⊞ X ⟶ Y ⊞ Z) [IsIso f] : CategoryStruct.id W = 0 ∨ CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp f Limits.biprod.fst) ≠ 0 ∨ CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp f Limits.biprod.snd) ≠ 0

theorem CategoryTheory.Biproduct.column_nonzero_of_iso' {C : Type u} [Category.{v, u} C] [Preadditive C] {σ τ : Type} [Finite τ] {S : σ → C} [Limits.HasBiproduct S] {T : τ → C} [Limits.HasBiproduct T] (s : σ) (f : ⨁ S ⟶ ⨁ T) [IsIso f] : (∀ (t : τ), CategoryStruct.comp (Limits.biproduct.ι S s) (CategoryStruct.comp f (Limits.biproduct.π T t)) = 0) → CategoryStruct.id (S s) = 0

def CategoryTheory.Biproduct.columnNonzeroOfIso {C : Type u} [Category.{v, u} C] [Preadditive C] {σ τ : Type} [Fintype τ] {S : σ → C} [Limits.HasBiproduct S] {T : τ → C} [Limits.HasBiproduct T] (s : σ) (nz : CategoryStruct.id (S s) ≠ 0) (f : ⨁ S ⟶ ⨁ T) [IsIso f] : Trunc ((t : τ) ×' CategoryStruct.comp (Limits.biproduct.ι S s) (CategoryStruct.comp f (Limits.biproduct.π T t)) ≠ 0)

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.

Equations

• CategoryTheory.Biproduct.columnNonzeroOfIso s nz f = truncSigmaOfExists ⋯

theorem CategoryTheory.Limits.preservesProduct_of_preservesBiproduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] {f : J → C} [PreservesBiproduct f F] : PreservesLimit (Discrete.functor f) F

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

theorem CategoryTheory.Limits.preservesProductsOfShape_of_preservesBiproductsOfShape {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] [PreservesBiproductsOfShape J F] : PreservesLimitsOfShape (Discrete J) F

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

theorem CategoryTheory.Limits.preservesBiproduct_of_preservesProduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] {f : J → C} [PreservesLimit (Discrete.functor f) F] : PreservesBiproduct f F

A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.

theorem CategoryTheory.Limits.preservesBiproduct_of_mono_biproductComparison {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] {f : J → C} [HasBiproduct f] [HasBiproduct (F.obj ∘ f)] [Mono (F.biproductComparison f)] : PreservesBiproduct f F

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.

theorem CategoryTheory.Limits.preservesBiproduct_of_epi_biproductComparison' {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] {f : J → C} [HasBiproduct f] [HasBiproduct (F.obj ∘ f)] [Epi (F.biproductComparison' f)] : PreservesBiproduct f F

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.

theorem CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesProductsOfShape {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] [PreservesLimitsOfShape (Discrete J) F] : PreservesBiproductsOfShape J F

A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.

theorem CategoryTheory.Limits.preservesCoproduct_of_preservesBiproduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] {f : J → C} [PreservesBiproduct f F] : PreservesColimit (Discrete.functor f) F

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

theorem CategoryTheory.Limits.preservesCoproductsOfShape_of_preservesBiproductsOfShape {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] [PreservesBiproductsOfShape J F] : PreservesColimitsOfShape (Discrete J) F

A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

theorem CategoryTheory.Limits.preservesBiproduct_of_preservesCoproduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] {f : J → C} [PreservesColimit (Discrete.functor f) F] : PreservesBiproduct f F

A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.

theorem CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type} [Fintype J] [PreservesColimitsOfShape (Discrete J) F] : PreservesBiproductsOfShape J F

A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.

theorem CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} [PreservesBinaryBiproduct X Y F] : PreservesLimit (pair X Y) F

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

theorem CategoryTheory.Limits.preservesBinaryProducts_of_preservesBinaryBiproducts {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBinaryBiproducts F] : PreservesLimitsOfShape (Discrete WalkingPair) F

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} [PreservesLimit (pair X Y) F] : PreservesBinaryBiproduct X Y F

A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.

theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} [HasBinaryBiproduct X Y] [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Mono (F.biprodComparison X Y)] : PreservesBinaryBiproduct X Y F

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.

theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_epi_biprodComparison' {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} [HasBinaryBiproduct X Y] [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Epi (F.biprodComparison' X Y)] : PreservesBinaryBiproduct X Y F

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.

theorem CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesLimitsOfShape (Discrete WalkingPair) F] : PreservesBinaryBiproducts F

A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.

theorem CategoryTheory.Limits.preservesBinaryCoproduct_of_preservesBinaryBiproduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} [PreservesBinaryBiproduct X Y F] : PreservesColimit (pair X Y) F

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

theorem CategoryTheory.Limits.preservesBinaryCoproducts_of_preservesBinaryBiproducts {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBinaryBiproducts F] : PreservesColimitsOfShape (Discrete WalkingPair) F

A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryCoproduct {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} [PreservesColimit (pair X Y) F] : PreservesBinaryBiproduct X Y F

A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.

theorem CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesColimitsOfShape (Discrete WalkingPair) F] : PreservesBinaryBiproducts F

A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.