Binary biproduct squares

This file records generic categorical properties of binary biproducts. A biproduct map factors through the maps obtained by changing one summand at a time, and the squares obtained by adjoining an identity summand are pushouts or pullbacks. The biproduct of two cokernels is the cokernel of the biproduct of the two morphisms (CategoryTheory.Limits.CokernelCofork.isColimitBiprod); this is the biproduct analogue of Mathlib's CategoryTheory.Limits.CokernelCofork.isColimitTensor. For functors preserving zero morphisms, biproduct preservation is stable under composition and follows from preservation of products and coproducts of the same shape. The short complex of a mapped commutative square agrees with the mapped short complex through the canonical biproduct comparison.

In a preadditive category, a zero object and binary biproducts already give all finite biproducts (TauCeti.hasFiniteBiproducts_of_hasBinaryBiproducts), and a finite biproduct indexed by Option J splits off its none summand (TauCeti.biproductOptionIso); the latter is the inductive step for computing additive invariants of finite biproducts. An additive functor which kills one summand of a binary biproduct inverts the projection onto the other (CategoryTheory.Functor.isIso_map_biprod_fst_of_isZero).

noncomputable def CategoryTheory.CommSq.shortComplexMapIso {C₁ : Type u} {D : Type u'} [Category.{v, u} C₁] [Preadditive C₁] [Category.{w, u'} D] [Preadditive D] {F : Functor C₁ D} [F.Additive] {W X Y Z : C₁} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] (sq : CommSq f g h i) : sq.shortComplex.map F ≅ ⋯.shortComplex

Mapping the short complex of a commutative square agrees, up to the canonical biproduct comparison, with the short complex of the mapped square.

Equations

• sq.shortComplexMapIso = CategoryTheory.ShortComplex.isoMk (CategoryTheory.Iso.refl (sq.shortComplex.map F).X₁) (F.mapBiprod X Y) (CategoryTheory.Iso.refl (sq.shortComplex.map F).X₃) ⋯ ⋯

theorem TauCeti.biprod_map_factor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] [CategoryTheory.Limits.HasBinaryBiproduct Y₁ X₂] [CategoryTheory.Limits.HasBinaryBiproduct Y₁ Y₂] : CategoryTheory.Limits.biprod.map f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.CategoryStruct.id X₂)) (CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id Y₁) g)

A binary biproduct map factors by changing its first and second summands in succession.

theorem TauCeti.isPushout_biprod_inl_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] : CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inl f (CategoryTheory.Limits.biprod.map f (CategoryTheory.CategoryStruct.id Z)) CategoryTheory.Limits.biprod.inl

The square formed by a morphism and the corresponding biproduct inclusions is a pushout.

theorem TauCeti.isPullback_biprod_map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasBinaryBiproduct X Z] [CategoryTheory.Limits.HasBinaryBiproduct Y Z] : CategoryTheory.IsPullback CategoryTheory.Limits.biprod.fst (CategoryTheory.Limits.biprod.map f (CategoryTheory.CategoryStruct.id Z)) f CategoryTheory.Limits.biprod.fst

The square formed by a morphism and the corresponding biproduct projections is a pullback.

theorem TauCeti.hasFiniteBiproducts_of_hasBinaryBiproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.Limits.HasFiniteBiproducts C

A preadditive category with a zero object and binary biproducts has all finite biproducts. Like Mathlib's CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts, this is a theorem rather than an instance, so that a concrete category may keep finite biproducts with better definitional properties.

noncomputable def TauCeti.biproductOptionIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type} [Fintype J] (f : Option J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct fun (j : J) => f (some j)] [CategoryTheory.Limits.HasBinaryBiproduct (f none) (⨁ fun (j : J) => f (some j))] : ⨁ f ≅ f none ⊞ ⨁ fun (j : J) => f (some j)

A biproduct indexed by Option J is the binary biproduct of its none summand and the biproduct of the remaining summands.

Equations

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

@[simp]

theorem TauCeti.biproductOptionIso_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type} [Fintype J] (f : Option J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct fun (j : J) => f (some j)] [CategoryTheory.Limits.HasBinaryBiproduct (f none) (⨁ fun (j : J) => f (some j))] : CategoryTheory.CategoryStruct.comp (biproductOptionIso f).hom CategoryTheory.Limits.biprod.fst = CategoryTheory.Limits.biproduct.π f none

@[simp]

theorem TauCeti.biproductOptionIso_hom_snd_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {J : Type} [Fintype J] (f : Option J → C) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct fun (j : J) => f (some j)] [CategoryTheory.Limits.HasBinaryBiproduct (f none) (⨁ fun (j : J) => f (some j))] (j : J) : CategoryTheory.CategoryStruct.comp (biproductOptionIso f).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.Limits.biproduct.π (fun (j : J) => f (some j)) j)) = CategoryTheory.Limits.biproduct.π f (some j)

@[instance 100]

instance CategoryTheory.Limits.preservesBiproductsOfShape_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {D : Type u'} [Category.{w', u'} D] [HasZeroMorphisms D] {E : Type u_1} [Category.{v_1, u_1} E] [HasZeroMorphisms E] (J : Type w) (F : Functor C D) (G : Functor D E) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [PreservesBiproductsOfShape J F] [PreservesBiproductsOfShape J G] : PreservesBiproductsOfShape J (F.comp G)

The composite of functors preserving biproducts of shape J preserves them.

@[instance 100]

instance CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesLimits_and_colimits {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {D : Type u'} [Category.{w', u'} D] [HasZeroMorphisms D] (J : Type w) (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesLimitsOfShape (Discrete J) F] [PreservesColimitsOfShape (Discrete J) F] : PreservesBiproductsOfShape J F

A functor preserving zero morphisms, products and coproducts of shape J preserves biproducts of that shape.

theorem CategoryTheory.Functor.isIso_map_biprod_fst_of_isZero {C : Type u} {D : Type v} [Category.{w, u} C] [Category.{w', v} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] (X Y : C) [Limits.HasBinaryBiproduct X Y] (hY : Limits.IsZero (F.obj Y)) : IsIso (F.map Limits.biprod.fst)

An additive functor which sends the second summand of a binary biproduct to a zero object sends the first projection to an isomorphism, with inverse the image of the first inclusion.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.CokernelCofork.biprod {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} (c₁ : CokernelCofork f₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} (c₂ : CokernelCofork f₂) [HasBinaryBiproduct X₁ X₂] [HasBinaryBiproduct Y₁ Y₂] [HasBinaryBiproduct c₁.pt c₂.pt] : CokernelCofork (biprod.map f₁ f₂)

Given cokernel coforks c₁ and c₂ for f₁ : X₁ ⟶ Y₁ and f₂ : X₂ ⟶ Y₂, this is the cokernel cofork for biprod.map f₁ f₂ : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂ with point c₁.pt ⊞ c₂.pt.

Equations

• c₁.biprod c₂ = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.Cofork.π c₁) (CategoryTheory.Limits.Cofork.π c₂)) ⋯

noncomputable def CategoryTheory.Limits.CokernelCofork.isColimitBiprod {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} {c₁ : CokernelCofork f₁} {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} {c₂ : CokernelCofork f₂} [HasBinaryBiproduct X₁ X₂] [HasBinaryBiproduct Y₁ Y₂] [HasBinaryBiproduct c₁.pt c₂.pt] (hc₁ : IsColimit c₁) (hc₂ : IsColimit c₂) : IsColimit (c₁.biprod c₂)

The biproduct of two colimit cokernel coforks is a colimit: c₁.pt ⊞ c₂.pt is the cokernel of biprod.map f₁ f₂.

Equations

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