Binary biproducts

We introduce the notion of binary biproducts.

These are slightly unusual relative to the other shapes in the library, as they are simultaneously limits and colimits. (Zero objects are similar; they are "biterminal".)

For results about biproducts in preadditive categories see CategoryTheory.Preadditive.Biproducts.

In a category with zero morphisms, we model the (binary) biproduct of P Q : C using a BinaryBicone, which has a cone point X, and morphisms fst : X ⟶ P, snd : X ⟶ Q, inl : P ⟶ X and inr : X ⟶ Q, such that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q. Such a BinaryBicone is a biproduct if the cone is a limit cone, and the cocone is a colimit cocone.

structure CategoryTheory.Limits.BinaryBicone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) : Type (max uC uC')

A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• pt : C

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• fst : self.pt ⟶ P

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• snd : self.pt ⟶ Q

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• inl : P ⟶ self.pt

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• inr : Q ⟶ self.pt

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• inl_fst : CategoryStruct.comp self.inl self.fst = CategoryStruct.id P

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• inl_snd : CategoryStruct.comp self.inl self.snd = 0

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• inr_fst : CategoryStruct.comp self.inr self.fst = 0

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

• inr_snd : CategoryStruct.comp self.inr self.snd = CategoryStruct.id Q

  A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.inl_fst_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (self : BinaryBicone P Q) {Z : C} (h : P ⟶ Z) : CategoryStruct.comp self.inl (CategoryStruct.comp self.fst h) = h

A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.inr_snd_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (self : BinaryBicone P Q) {Z : C} (h : Q ⟶ Z) : CategoryStruct.comp self.inr (CategoryStruct.comp self.snd h) = h

A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.inr_fst_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (self : BinaryBicone P Q) {Z : C} (h : P ⟶ Z) : CategoryStruct.comp self.inr (CategoryStruct.comp self.fst h) = CategoryStruct.comp 0 h

A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.inl_snd_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (self : BinaryBicone P Q) {Z : C} (h : Q ⟶ Z) : CategoryStruct.comp self.inl (CategoryStruct.comp self.snd h) = CategoryStruct.comp 0 h

A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inl ≫ fst = 𝟙 P, inl ≫ snd = 0, inr ≫ fst = 0, and inr ≫ snd = 𝟙 Q

structure CategoryTheory.Limits.BinaryBiconeMorphism {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (A B : BinaryBicone P Q) : Type uC'

A binary bicone morphism between two binary bicones for the same diagram is a morphism of the binary bicone points which commutes with the cone and cocone legs.

• hom : A.pt ⟶ B.pt

  A morphism between the two vertex objects of the bicones

• wfst : CategoryStruct.comp self.hom B.fst = A.fst

  The triangle consisting of the two natural transformations and hom commutes

• wsnd : CategoryStruct.comp self.hom B.snd = A.snd

  The triangle consisting of the two natural transformations and hom commutes

• winl : CategoryStruct.comp A.inl self.hom = B.inl

  The triangle consisting of the two natural transformations and hom commutes

• winr : CategoryStruct.comp A.inr self.hom = B.inr

  The triangle consisting of the two natural transformations and hom commutes

@[simp]

theorem CategoryTheory.Limits.BinaryBiconeMorphism.wsnd_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {A B : BinaryBicone P Q} (self : BinaryBiconeMorphism A B) {Z : C} (h : Q ⟶ Z) : CategoryStruct.comp self.hom (CategoryStruct.comp B.snd h) = CategoryStruct.comp A.snd h

The triangle consisting of the two natural transformations and hom commutes

@[simp]

theorem CategoryTheory.Limits.BinaryBiconeMorphism.wfst_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {A B : BinaryBicone P Q} (self : BinaryBiconeMorphism A B) {Z : C} (h : P ⟶ Z) : CategoryStruct.comp self.hom (CategoryStruct.comp B.fst h) = CategoryStruct.comp A.fst h

The triangle consisting of the two natural transformations and hom commutes

@[simp]

theorem CategoryTheory.Limits.BinaryBiconeMorphism.winl_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {A B : BinaryBicone P Q} (self : BinaryBiconeMorphism A B) {Z : C} (h : B.pt ⟶ Z) : CategoryStruct.comp A.inl (CategoryStruct.comp self.hom h) = CategoryStruct.comp B.inl h

The triangle consisting of the two natural transformations and hom commutes

@[simp]

theorem CategoryTheory.Limits.BinaryBiconeMorphism.winr_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {A B : BinaryBicone P Q} (self : BinaryBiconeMorphism A B) {Z : C} (h : B.pt ⟶ Z) : CategoryStruct.comp A.inr (CategoryStruct.comp self.hom h) = CategoryStruct.comp B.inr h

The triangle consisting of the two natural transformations and hom commutes

@[implicit_reducible]

instance CategoryTheory.Limits.BinaryBicone.category {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} : Category.{uC', max uC uC'} (BinaryBicone P Q)

The category of binary bicones on a given diagram.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.category_id_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (B : BinaryBicone P Q) : (CategoryStruct.id B).hom = CategoryStruct.id B.pt

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.category_comp_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {X✝ Y✝ Z✝ : BinaryBicone P Q} (f : BinaryBiconeMorphism X✝ Y✝) (g : BinaryBiconeMorphism Y✝ Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.Limits.BinaryBiconeMorphism.ext {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {c c' : BinaryBicone P Q} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

theorem CategoryTheory.Limits.BinaryBiconeMorphism.ext_iff {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {c c' : BinaryBicone P Q} {f g : c ⟶ c'} : f = g ↔ f.hom = g.hom

def CategoryTheory.Limits.BinaryBicones.ext {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {c c' : BinaryBicone P Q} (φ : c.pt ≅ c'.pt) (winl : CategoryStruct.comp c.inl φ.hom = c'.inl := by cat_disch) (winr : CategoryStruct.comp c.inr φ.hom = c'.inr := by cat_disch) (wfst : CategoryStruct.comp φ.hom c'.fst = c.fst := by cat_disch) (wsnd : CategoryStruct.comp φ.hom c'.snd = c.snd := by cat_disch) : c ≅ c'

To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.ext_inv_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {c c' : BinaryBicone P Q} (φ : c.pt ≅ c'.pt) (winl : CategoryStruct.comp c.inl φ.hom = c'.inl := by cat_disch) (winr : CategoryStruct.comp c.inr φ.hom = c'.inr := by cat_disch) (wfst : CategoryStruct.comp φ.hom c'.fst = c.fst := by cat_disch) (wsnd : CategoryStruct.comp φ.hom c'.snd = c.snd := by cat_disch) : (ext φ winl winr wfst wsnd).inv.hom = φ.inv

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.ext_hom_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} {c c' : BinaryBicone P Q} (φ : c.pt ≅ c'.pt) (winl : CategoryStruct.comp c.inl φ.hom = c'.inl := by cat_disch) (winr : CategoryStruct.comp c.inr φ.hom = c'.inr := by cat_disch) (wfst : CategoryStruct.comp φ.hom c'.fst = c.fst := by cat_disch) (wsnd : CategoryStruct.comp φ.hom c'.snd = c.snd := by cat_disch) : (ext φ winl winr wfst wsnd).hom.hom = φ.hom

def CategoryTheory.Limits.BinaryBicones.functoriality {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] : Functor (BinaryBicone P Q) (BinaryBicone (F.obj P) (F.obj Q))

A functor F : C ⥤ D sends binary bicones for P and Q to binary bicones for G.obj P and G.obj Q functorially.

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] (A : BinaryBicone P Q) : ((functoriality P Q F).obj A).snd = F.map A.snd

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_pt {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] (A : BinaryBicone P Q) : ((functoriality P Q F).obj A).pt = F.obj A.pt

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_inl {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] (A : BinaryBicone P Q) : ((functoriality P Q F).obj A).inl = F.map A.inl

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] (A : BinaryBicone P Q) : ((functoriality P Q F).obj A).fst = F.map A.fst

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_inr {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] (A : BinaryBicone P Q) : ((functoriality P Q F).obj A).inr = F.map A.inr

@[simp]

theorem CategoryTheory.Limits.BinaryBicones.functoriality_map_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] {X✝ Y✝ : BinaryBicone P Q} (f : X✝ ⟶ Y✝) : ((functoriality P Q F).map f).hom = F.map f.hom

instance CategoryTheory.Limits.BinaryBicones.functoriality_full {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] [F.Full] [F.Faithful] : (functoriality P Q F).Full

instance CategoryTheory.Limits.BinaryBicones.functoriality_faithful {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {D : Type uD} [Category.{uD', uD} D] [HasZeroMorphisms D] (P Q : C) (F : Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] : (functoriality P Q F).Faithful

def CategoryTheory.Limits.BinaryBicone.toCone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : Cone (pair P Q)

Extract the cone from a binary bicone.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toCone_pt {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : c.toCone.pt = c.pt

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toCone_π_app_left {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : c.toCone.π.app { as := WalkingPair.left } = c.fst

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toCone_π_app_right {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : c.toCone.π.app { as := WalkingPair.right } = c.snd

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.binary_fan_fst_toCone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : BinaryFan.fst c.toCone = c.fst

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.binary_fan_snd_toCone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : BinaryFan.snd c.toCone = c.snd

def CategoryTheory.Limits.BinaryBicone.toCocone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : Cocone (pair P Q)

Extract the cocone from a binary bicone.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toCocone_pt {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : c.toCocone.pt = c.pt

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_left {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : c.toCocone.ι.app { as := WalkingPair.left } = c.inl

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_right {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : c.toCocone.ι.app { as := WalkingPair.right } = c.inr

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.binary_cofan_inl_toCocone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : BinaryCofan.inl c.toCocone = c.inl

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.binary_cofan_inr_toCocone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : BinaryCofan.inr c.toCocone = c.inr

def CategoryTheory.Limits.BinaryBicone.retract_left {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : Retract P c.pt

The retract of a binary bicone c given by c.inl and c.fst.

def CategoryTheory.Limits.BinaryBicone.retract_right {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : Retract Q c.pt

The retract of a binary bicone c given by c.inr and c.snd.

instance CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInl {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : IsSplitMono c.inl

instance CategoryTheory.Limits.BinaryBicone.instIsSplitMonoInr {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : IsSplitMono c.inr

instance CategoryTheory.Limits.BinaryBicone.instIsSplitEpiFst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : IsSplitEpi c.fst

instance CategoryTheory.Limits.BinaryBicone.instIsSplitEpiSnd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (c : BinaryBicone P Q) : IsSplitEpi c.snd

def CategoryTheory.Limits.BinaryBicone.toBiconeFunctor {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} : Functor (BinaryBicone X Y) (Bicone (pairFunction X Y))

Convert a BinaryBicone into a Bicone over a pair.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_map_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} {X✝ Y✝ : BinaryBicone X Y} (f : X✝ ⟶ Y✝) : (toBiconeFunctor.map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_π {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : BinaryBicone X Y) (j : WalkingPair) : (toBiconeFunctor.obj b).π j = WalkingPair.casesOn j b.fst b.snd

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_pt {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : BinaryBicone X Y) : (toBiconeFunctor.obj b).pt = b.pt

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_ι {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : BinaryBicone X Y) (j : WalkingPair) : (toBiconeFunctor.obj b).ι j = WalkingPair.casesOn j b.inl b.inr

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryBicone.toBicone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : BinaryBicone X Y) : Bicone (pairFunction X Y)

A shorthand for toBiconeFunctor.obj

def CategoryTheory.Limits.BinaryBicone.toBiconeIsLimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : BinaryBicone X Y) : IsLimit b.toBicone.toCone ≃ IsLimit b.toCone

A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone.

def CategoryTheory.Limits.BinaryBicone.toBiconeIsColimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : BinaryBicone X Y) : IsColimit b.toBicone.toCocone ≃ IsColimit b.toCocone

A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit cocone.

def CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} : Functor (Bicone (pairFunction X Y)) (BinaryBicone X Y)

Convert a Bicone over a function on WalkingPair to a BinaryBicone.

@[simp]

theorem CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_pt {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : (toBinaryBiconeFunctor.obj b).pt = b.pt

@[simp]

theorem CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : (toBinaryBiconeFunctor.obj b).fst = b.π WalkingPair.left

@[simp]

theorem CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : (toBinaryBiconeFunctor.obj b).snd = b.π WalkingPair.right

@[simp]

theorem CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_inl {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : (toBinaryBiconeFunctor.obj b).inl = b.ι WalkingPair.left

@[simp]

theorem CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_inr {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : (toBinaryBiconeFunctor.obj b).inr = b.ι WalkingPair.right

@[simp]

theorem CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_map_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} {X✝ Y✝ : Bicone (pairFunction X Y)} (f : X✝ ⟶ Y✝) : (toBinaryBiconeFunctor.map f).hom = f.hom

@[reducible, inline]

abbrev CategoryTheory.Limits.Bicone.toBinaryBicone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : BinaryBicone X Y

A shorthand for toBinaryBiconeFunctor.obj

def CategoryTheory.Limits.Bicone.toBinaryBiconeIsLimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : IsLimit b.toBinaryBicone.toCone ≃ IsLimit b.toCone

A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit cone.

def CategoryTheory.Limits.Bicone.toBinaryBiconeIsColimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : IsColimit b.toBinaryBicone.toCocone ≃ IsColimit b.toCocone

A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a colimit cocone.

structure CategoryTheory.Limits.BinaryBicone.IsBilimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (b : BinaryBicone P Q) : Type (max uC uC')

Structure witnessing that a binary bicone is a limit cone and a limit cocone.

• isLimit : IsLimit b.toCone

  Structure witnessing that a binary bicone is a limit cone and a limit cocone.

• isColimit : IsColimit b.toCocone

  Structure witnessing that a binary bicone is a limit cone and a limit cocone.

def CategoryTheory.Limits.BinaryBicone.toBiconeIsBilimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : BinaryBicone X Y) : b.toBicone.IsBilimit ≃ b.IsBilimit

A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit.

def CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (b : Bicone (pairFunction X Y)) : b.toBinaryBicone.IsBilimit ≃ b.IsBilimit

A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a bilimit.

structure CategoryTheory.Limits.BinaryBiproductData {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) : Type (max uC uC')

A bicone over P Q : C, which is both a limit cone and a colimit cocone.

• bicone : BinaryBicone P Q

  A bicone over P Q : C, which is both a limit cone and a colimit cocone.

• isBilimit : self.bicone.IsBilimit

  A bicone over P Q : C, which is both a limit cone and a colimit cocone.

class CategoryTheory.Limits.HasBinaryBiproduct {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) : Prop

HasBinaryBiproduct P Q expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram pair P Q.

• mk' :: (
• exists_binary_biproduct : Nonempty (BinaryBiproductData P Q)

  HasBinaryBiproduct P Q expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram pair P Q.

• )

theorem CategoryTheory.Limits.HasBinaryBiproduct.mk {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} (d : BinaryBiproductData P Q) : HasBinaryBiproduct P Q

noncomputable def CategoryTheory.Limits.getBinaryBiproductData {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) [HasBinaryBiproduct P Q] : BinaryBiproductData P Q

Use the axiom of choice to extract explicit BinaryBiproductData F from HasBinaryBiproduct F.

noncomputable def CategoryTheory.Limits.BinaryBiproduct.bicone {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) [HasBinaryBiproduct P Q] : BinaryBicone P Q

A bicone for P Q which is both a limit cone and a colimit cocone.

noncomputable def CategoryTheory.Limits.BinaryBiproduct.isBilimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) [HasBinaryBiproduct P Q] : (bicone P Q).IsBilimit

BinaryBiproduct.bicone P Q is a limit bicone.

noncomputable def CategoryTheory.Limits.BinaryBiproduct.isLimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) [HasBinaryBiproduct P Q] : IsLimit (bicone P Q).toCone

BinaryBiproduct.bicone P Q is a limit cone.

noncomputable def CategoryTheory.Limits.BinaryBiproduct.isColimit {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (P Q : C) [HasBinaryBiproduct P Q] : IsColimit (bicone P Q).toCocone

BinaryBiproduct.bicone P Q is a colimit cocone.

class CategoryTheory.Limits.HasBinaryBiproducts (C : Type uC) [Category.{uC', uC} C] [HasZeroMorphisms C] : Prop

HasBinaryBiproducts C represents the existence of a bicone which is simultaneously a limit and a colimit of the diagram pair P Q, for every P Q : C.

• has_binary_biproduct (P Q : C) : HasBinaryBiproduct P Q

theorem CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts (C : Type uC) [Category.{uC', uC} C] [HasZeroMorphisms C] [HasFiniteBiproducts C] : HasBinaryBiproducts C

A category with finite biproducts has binary biproducts.

This is not an instance as typically in concrete categories there will be an alternative construction with nicer definitional properties.

instance CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} [HasBinaryBiproduct P Q] : HasLimit (pair P Q)

instance CategoryTheory.Limits.HasBinaryBiproduct.hasColimit_pair {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {P Q : C} [HasBinaryBiproduct P Q] : HasColimit (pair P Q)

@[instance 100]

instance CategoryTheory.Limits.hasBinaryProducts_of_hasBinaryBiproducts {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] : HasBinaryProducts C

@[instance 100]

instance CategoryTheory.Limits.hasBinaryCoproducts_of_hasBinaryBiproducts {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] : HasBinaryCoproducts C

noncomputable def CategoryTheory.Limits.biprodIso {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : X ⨯ Y ≅ X ⨿ Y

The isomorphism between the specified binary product and the specified binary coproduct for a pair for a binary biproduct.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : C

An arbitrary choice of biproduct of a pair of objects.

def CategoryTheory.Limits.«term_⊞_» : Lean.TrailingParserDescr

An arbitrary choice of biproduct of a pair of objects.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : X ⊞ Y ⟶ X

The projection onto the first summand of a binary biproduct.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : X ⊞ Y ⟶ Y

The projection onto the second summand of a binary biproduct.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.inl {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : X ⟶ X ⊞ Y

The inclusion into the first summand of a binary biproduct.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.inr {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : Y ⟶ X ⊞ Y

The inclusion into the second summand of a binary biproduct.

@[simp]

theorem CategoryTheory.Limits.BinaryBiproduct.bicone_fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (bicone X Y).fst = biprod.fst

@[simp]

theorem CategoryTheory.Limits.BinaryBiproduct.bicone_snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (bicone X Y).snd = biprod.snd

@[simp]

theorem CategoryTheory.Limits.BinaryBiproduct.bicone_inl {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (bicone X Y).inl = biprod.inl

@[simp]

theorem CategoryTheory.Limits.BinaryBiproduct.bicone_inr {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (bicone X Y).inr = biprod.inr

theorem CategoryTheory.Limits.biprod.inl_fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : CategoryStruct.comp inl fst = CategoryStruct.id X

theorem CategoryTheory.Limits.biprod.inl_fst_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp inl (CategoryStruct.comp fst h) = h

theorem CategoryTheory.Limits.biprod.inl_snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : CategoryStruct.comp inl snd = 0

theorem CategoryTheory.Limits.biprod.inl_snd_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp inl (CategoryStruct.comp snd h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Limits.biprod.inr_fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : CategoryStruct.comp inr fst = 0

theorem CategoryTheory.Limits.biprod.inr_fst_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp inr (CategoryStruct.comp fst h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Limits.biprod.inr_snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : CategoryStruct.comp inr snd = CategoryStruct.id Y

theorem CategoryTheory.Limits.biprod.inr_snd_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp inr (CategoryStruct.comp snd h) = h

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.lift {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⊞ Y

Given a pair of maps into the summands of a binary biproduct, we obtain a map into the binary biproduct.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.desc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⊞ Y ⟶ W

Given a pair of maps out of the summands of a binary biproduct, we obtain a map out of the binary biproduct.

@[simp]

theorem CategoryTheory.Limits.biprod.lift_fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (lift f g) fst = f

@[simp]

theorem CategoryTheory.Limits.biprod.lift_fst_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp fst h) = CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.Limits.biprod.lift_snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (lift f g) snd = g

@[simp]

theorem CategoryTheory.Limits.biprod.lift_snd_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp snd h) = CategoryStruct.comp g h

@[simp]

theorem CategoryTheory.Limits.biprod.inl_desc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp inl (desc f g) = f

@[simp]

theorem CategoryTheory.Limits.biprod.inl_desc_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z) : CategoryStruct.comp inl (CategoryStruct.comp (desc f g) h) = CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.Limits.biprod.inr_desc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp inr (desc f g) = g

@[simp]

theorem CategoryTheory.Limits.biprod.inr_desc_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z) : CategoryStruct.comp inr (CategoryStruct.comp (desc f g) h) = CategoryStruct.comp g h

instance CategoryTheory.Limits.biprod.mono_lift_of_mono_left {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono f] : Mono (lift f g)

instance CategoryTheory.Limits.biprod.mono_lift_of_mono_right {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono g] : Mono (lift f g)

instance CategoryTheory.Limits.biprod.epi_desc_of_epi_left {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi f] : Epi (desc f g)

instance CategoryTheory.Limits.biprod.epi_desc_of_epi_right {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y : C} [HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi g] : Epi (desc f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.map {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⊞ X ⟶ Y ⊞ Z

Given a pair of maps between the summands of a pair of binary biproducts, we obtain a map between the binary biproducts.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.biprod.map' {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⊞ X ⟶ Y ⊞ Z

An alternative to biprod.map constructed via colimits. This construction only exists in order to show it is equal to biprod.map.

theorem CategoryTheory.Limits.biprod.hom_ext {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y Z : C} [HasBinaryBiproduct X Y] (f g : Z ⟶ X ⊞ Y) (h₀ : CategoryStruct.comp f fst = CategoryStruct.comp g fst) (h₁ : CategoryStruct.comp f snd = CategoryStruct.comp g snd) : f = g

theorem CategoryTheory.Limits.biprod.hom_ext_iff {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y Z : C} [HasBinaryBiproduct X Y] {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.hom_ext' {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y Z : C} [HasBinaryBiproduct X Y] (f g : X ⊞ Y ⟶ Z) (h₀ : CategoryStruct.comp inl f = CategoryStruct.comp inl g) (h₁ : CategoryStruct.comp inr f = CategoryStruct.comp inr g) : f = g

theorem CategoryTheory.Limits.biprod.hom_ext'_iff {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y Z : C} [HasBinaryBiproduct X Y] {f g : X ⊞ Y ⟶ Z} : f = g ↔ CategoryStruct.comp inl f = CategoryStruct.comp inl g ∧ CategoryStruct.comp inr f = CategoryStruct.comp inr g

noncomputable def CategoryTheory.Limits.biprod.isoProd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : X ⊞ Y ≅ X ⨯ Y

The canonical isomorphism between the chosen biproduct and the chosen product.

@[simp]

theorem CategoryTheory.Limits.biprod.isoProd_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (isoProd X Y).hom = prod.lift fst snd

@[simp]

theorem CategoryTheory.Limits.biprod.isoProd_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (isoProd X Y).inv = lift prod.fst prod.snd

noncomputable def CategoryTheory.Limits.biprod.isoCoprod {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : X ⊞ Y ≅ X ⨿ Y

The canonical isomorphism between the chosen biproduct and the chosen coproduct.

@[simp]

theorem CategoryTheory.Limits.biprod.isoCoprod_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (isoCoprod X Y).inv = coprod.desc inl inr

@[simp]

theorem CategoryTheory.Limits.biprod_isoCoprod_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : (biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr

theorem CategoryTheory.Limits.biprod.map_eq_map' {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : map f g = map' f g

instance CategoryTheory.Limits.biprod.inl_mono {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : IsSplitMono inl

instance CategoryTheory.Limits.biprod.inr_mono {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : IsSplitMono inr

instance CategoryTheory.Limits.biprod.fst_epi {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : IsSplitEpi fst

instance CategoryTheory.Limits.biprod.snd_epi {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : IsSplitEpi snd

@[simp]

theorem CategoryTheory.Limits.biprod.map_fst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (map f g) fst = CategoryStruct.comp fst f

@[simp]

theorem CategoryTheory.Limits.biprod.map_fst_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (map f g) (CategoryStruct.comp fst h) = CategoryStruct.comp fst (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Limits.biprod.map_snd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (map f g) snd = CategoryStruct.comp snd g

@[simp]

theorem CategoryTheory.Limits.biprod.map_snd_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (map f g) (CategoryStruct.comp snd h) = CategoryStruct.comp snd (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.Limits.biprod.inl_map {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp inl (map f g) = CategoryStruct.comp f inl

@[simp]

theorem CategoryTheory.Limits.biprod.inl_map_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⊞ Z ⟶ Z✝) : CategoryStruct.comp inl (CategoryStruct.comp (map f g) h) = CategoryStruct.comp f (CategoryStruct.comp inl h)

@[simp]

theorem CategoryTheory.Limits.biprod.inr_map {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp inr (map f g) = CategoryStruct.comp g inr

@[simp]

theorem CategoryTheory.Limits.biprod.inr_map_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⊞ Z ⟶ Z✝) : CategoryStruct.comp inr (CategoryStruct.comp (map f g) h) = CategoryStruct.comp g (CategoryStruct.comp inr h)

noncomputable def CategoryTheory.Limits.biprod.mapIso {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⊞ X ≅ Y ⊞ Z

Given a pair of isomorphisms between the summands of a pair of binary biproducts, we obtain an isomorphism between the binary biproducts.

@[simp]

theorem CategoryTheory.Limits.biprod.mapIso_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).inv = map f.inv g.inv

@[simp]

theorem CategoryTheory.Limits.biprod.mapIso_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).hom = map f.hom g.hom

theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).hom = lift b.fst b.snd

Auxiliary lemma for biprod.uniqueUpToIso.

theorem CategoryTheory.Limits.biprod.conePointUniqueUpToIso_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv = desc b.inl b.inr

Auxiliary lemma for biprod.uniqueUpToIso.

noncomputable def CategoryTheory.Limits.biprod.uniqueUpToIso {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) : b.pt ≅ X ⊞ Y

Binary biproducts are unique up to isomorphism. This already follows because bilimits are limits, but in the case of biproducts we can give an isomorphism with particularly nice definitional properties, namely that biprod.lift b.fst b.snd and biprod.desc b.inl b.inr are inverses of each other.

@[simp]

theorem CategoryTheory.Limits.biprod.uniqueUpToIso_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) : (uniqueUpToIso X Y hb).hom = lift b.fst b.snd

@[simp]

theorem CategoryTheory.Limits.biprod.uniqueUpToIso_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] {b : BinaryBicone X Y} (hb : b.IsBilimit) : (uniqueUpToIso X Y hb).inv = desc b.inl b.inr

theorem CategoryTheory.Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : IsIso inl ↔ CategoryStruct.id (X ⊞ Y) = CategoryStruct.comp fst inl

instance CategoryTheory.Limits.biprod.map_epi {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Epi (map f g)

instance CategoryTheory.Limits.prod.map_epi {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f] [Epi g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Epi (map f g)

instance CategoryTheory.Limits.biprod.map_mono {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Mono (map f g)

instance CategoryTheory.Limits.coprod.map_mono {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Mono (map f g)

def CategoryTheory.Limits.BinaryBicone.fstKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : KernelFork c.fst

A kernel fork for the kernel of BinaryBicone.fst. It consists of the morphism BinaryBicone.inr.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.fstKernelFork_ι {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : Fork.ι c.fstKernelFork = c.inr

def CategoryTheory.Limits.BinaryBicone.sndKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : KernelFork c.snd

A kernel fork for the kernel of BinaryBicone.snd. It consists of the morphism BinaryBicone.inl.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.sndKernelFork_ι {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : Fork.ι c.sndKernelFork = c.inl

def CategoryTheory.Limits.BinaryBicone.inlCokernelCofork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : CokernelCofork c.inl

A cokernel cofork for the cokernel of BinaryBicone.inl. It consists of the morphism BinaryBicone.snd.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.inlCokernelCofork_π {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : Cofork.π c.inlCokernelCofork = c.snd

def CategoryTheory.Limits.BinaryBicone.inrCokernelCofork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : CokernelCofork c.inr

A cokernel cofork for the cokernel of BinaryBicone.inr. It consists of the morphism BinaryBicone.fst.

@[simp]

theorem CategoryTheory.Limits.BinaryBicone.inrCokernelCofork_π {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} (c : BinaryBicone X Y) : Cofork.π c.inrCokernelCofork = c.fst

def CategoryTheory.Limits.BinaryBicone.isLimitFstKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} {c : BinaryBicone X Y} (i : IsLimit c.toCone) : IsLimit c.fstKernelFork

The fork defined in BinaryBicone.fstKernelFork is indeed a kernel.

def CategoryTheory.Limits.BinaryBicone.isLimitSndKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} {c : BinaryBicone X Y} (i : IsLimit c.toCone) : IsLimit c.sndKernelFork

The fork defined in BinaryBicone.sndKernelFork is indeed a kernel.

def CategoryTheory.Limits.BinaryBicone.isColimitInlCokernelCofork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} {c : BinaryBicone X Y} (i : IsColimit c.toCocone) : IsColimit c.inlCokernelCofork

The cofork defined in BinaryBicone.inlCokernelCofork is indeed a cokernel.

def CategoryTheory.Limits.BinaryBicone.isColimitInrCokernelCofork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} {c : BinaryBicone X Y} (i : IsColimit c.toCocone) : IsColimit c.inrCokernelCofork

The cofork defined in BinaryBicone.inrCokernelCofork is indeed a cokernel.

noncomputable def CategoryTheory.Limits.biprod.fstKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : KernelFork fst

A kernel fork for the kernel of biprod.fst. It consists of the morphism biprod.inr.

@[simp]

theorem CategoryTheory.Limits.biprod.fstKernelFork_ι {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : Fork.ι (fstKernelFork X Y) = inr

noncomputable def CategoryTheory.Limits.biprod.isKernelFstKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : IsLimit (fstKernelFork X Y)

The fork biprod.fstKernelFork is indeed a limit.

noncomputable def CategoryTheory.Limits.biprod.sndKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : KernelFork snd

A kernel fork for the kernel of biprod.snd. It consists of the morphism biprod.inl.

@[simp]

theorem CategoryTheory.Limits.biprod.sndKernelFork_ι {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : Fork.ι (sndKernelFork X Y) = inl

noncomputable def CategoryTheory.Limits.biprod.isKernelSndKernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : IsLimit (sndKernelFork X Y)

The fork biprod.sndKernelFork is indeed a limit.

noncomputable def CategoryTheory.Limits.biprod.inlCokernelCofork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : CokernelCofork inl

A cokernel cofork for the cokernel of biprod.inl. It consists of the morphism biprod.snd.

@[simp]

theorem CategoryTheory.Limits.biprod.inlCokernelCofork_π {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : Cofork.π (inlCokernelCofork X Y) = snd

noncomputable def CategoryTheory.Limits.biprod.isCokernelInlCokernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : IsColimit (inlCokernelCofork X Y)

The cofork biprod.inlCokernelFork is indeed a colimit.

noncomputable def CategoryTheory.Limits.biprod.inrCokernelCofork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : CokernelCofork inr

A cokernel cofork for the cokernel of biprod.inr. It consists of the morphism biprod.fst.

@[simp]

theorem CategoryTheory.Limits.biprod.inrCokernelCofork_π {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : Cofork.π (inrCokernelCofork X Y) = fst

noncomputable def CategoryTheory.Limits.biprod.isCokernelInrCokernelFork {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryBiproduct X Y] : IsColimit (inrCokernelCofork X Y)

The cofork biprod.inrCokernelFork is indeed a colimit.

instance CategoryTheory.Limits.instHasKernelFst {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : HasKernel biprod.fst

noncomputable def CategoryTheory.Limits.kernelBiprodFstIso {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : kernel biprod.fst ≅ Y

The kernel of biprod.fst : X ⊞ Y ⟶ X is Y.

@[simp]

theorem CategoryTheory.Limits.kernelBiprodFstIso_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : kernelBiprodFstIso.inv = limit.lift (parallelPair biprod.fst 0) (biprod.fstKernelFork X Y)

@[simp]

theorem CategoryTheory.Limits.kernelBiprodFstIso_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : kernelBiprodFstIso.hom = (biprod.isKernelFstKernelFork X Y).lift (limit.cone (parallelPair biprod.fst 0))

instance CategoryTheory.Limits.instHasKernelSnd {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : HasKernel biprod.snd

noncomputable def CategoryTheory.Limits.kernelBiprodSndIso {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : kernel biprod.snd ≅ X

The kernel of biprod.snd : X ⊞ Y ⟶ Y is X.

@[simp]

theorem CategoryTheory.Limits.kernelBiprodSndIso_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : kernelBiprodSndIso.hom = (biprod.isKernelSndKernelFork X Y).lift (limit.cone (parallelPair biprod.snd 0))

@[simp]

theorem CategoryTheory.Limits.kernelBiprodSndIso_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : kernelBiprodSndIso.inv = limit.lift (parallelPair biprod.snd 0) (biprod.sndKernelFork X Y)

instance CategoryTheory.Limits.instHasCokernelInl {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : HasCokernel biprod.inl

noncomputable def CategoryTheory.Limits.cokernelBiprodInlIso {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : cokernel biprod.inl ≅ Y

The cokernel of biprod.inl : X ⟶ X ⊞ Y is Y.

@[simp]

theorem CategoryTheory.Limits.cokernelBiprodInlIso_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : cokernelBiprodInlIso.hom = colimit.desc (parallelPair biprod.inl 0) (biprod.inlCokernelCofork X Y)

@[simp]

theorem CategoryTheory.Limits.cokernelBiprodInlIso_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : cokernelBiprodInlIso.inv = (biprod.isCokernelInlCokernelFork X Y).desc (colimit.cocone (parallelPair biprod.inl 0))

instance CategoryTheory.Limits.instHasCokernelInr {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : HasCokernel biprod.inr

noncomputable def CategoryTheory.Limits.cokernelBiprodInrIso {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : cokernel biprod.inr ≅ X

The cokernel of biprod.inr : Y ⟶ X ⊞ Y is X.

@[simp]

theorem CategoryTheory.Limits.cokernelBiprodInrIso_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : cokernelBiprodInrIso.hom = colimit.desc (parallelPair biprod.inr 0) (biprod.inrCokernelCofork X Y)

@[simp]

theorem CategoryTheory.Limits.cokernelBiprodInrIso_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] : cokernelBiprodInrIso.inv = (biprod.isCokernelInrCokernelFork X Y).desc (colimit.cocone (parallelPair biprod.inr 0))

noncomputable def CategoryTheory.Limits.isoBiprodZero {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero Y) : X ≅ X ⊞ Y

If Y is a zero object, X ≅ X ⊞ Y for any X.

@[simp]

theorem CategoryTheory.Limits.isoBiprodZero_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero Y) : (isoBiprodZero hY).hom = biprod.inl

@[simp]

theorem CategoryTheory.Limits.isoBiprodZero_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero Y) : (isoBiprodZero hY).inv = biprod.fst

noncomputable def CategoryTheory.Limits.isoZeroBiprod {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero X) : Y ≅ X ⊞ Y

If X is a zero object, Y ≅ X ⊞ Y for any Y.

@[simp]

theorem CategoryTheory.Limits.isoZeroBiprod_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero X) : (isoZeroBiprod hY).hom = biprod.inr

@[simp]

theorem CategoryTheory.Limits.isoZeroBiprod_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] {X Y : C} [HasBinaryBiproduct X Y] (hY : IsZero X) : (isoZeroBiprod hY).inv = biprod.snd

@[simp]

theorem CategoryTheory.Limits.biprod_isZero_iff {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] (A B : C) [HasBinaryBiproduct A B] : IsZero (A ⊞ B) ↔ IsZero A ∧ IsZero B

noncomputable def CategoryTheory.Limits.biprod.braiding {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : P ⊞ Q ≅ Q ⊞ P

The braiding isomorphism which swaps a binary biproduct.

@[simp]

theorem CategoryTheory.Limits.biprod.braiding_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : (braiding P Q).hom = lift snd fst

@[simp]

theorem CategoryTheory.Limits.biprod.braiding_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : (braiding P Q).inv = lift snd fst

noncomputable def CategoryTheory.Limits.biprod.braiding' {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : P ⊞ Q ≅ Q ⊞ P

An alternative formula for the braiding isomorphism which swaps a binary biproduct, using the fact that the biproduct is a coproduct.

@[simp]

theorem CategoryTheory.Limits.biprod.braiding'_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : (braiding' P Q).hom = desc inr inl

@[simp]

theorem CategoryTheory.Limits.biprod.braiding'_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : (braiding' P Q).inv = desc inr inl

theorem CategoryTheory.Limits.biprod.braiding'_eq_braiding {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {P Q : C} : braiding' P Q = braiding P Q

theorem CategoryTheory.Limits.biprod.braid_natural {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryStruct.comp (map f g) (braiding Y W).hom = CategoryStruct.comp (braiding X Z).hom (map g f)

The braiding isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.biprod.braid_natural_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⊞ Y ⟶ Z✝) : CategoryStruct.comp (map f g) (CategoryStruct.comp (braiding Y W).hom h) = CategoryStruct.comp (braiding X Z).hom (CategoryStruct.comp (map g f) h)

The braiding isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.biprod.braiding_map_braiding {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (braiding X W).hom (CategoryStruct.comp (map f g) (braiding Y Z).hom) = map g f

theorem CategoryTheory.Limits.biprod.braiding_map_braiding_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Z ⊞ Y ⟶ Z✝) : CategoryStruct.comp (braiding X W).hom (CategoryStruct.comp (map f g) (CategoryStruct.comp (braiding Y Z).hom h)) = CategoryStruct.comp (map g f) h

@[simp]

theorem CategoryTheory.Limits.biprod.symmetry' {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : CategoryStruct.comp (lift snd fst) (lift snd fst) = CategoryStruct.id (P ⊞ Q)

@[simp]

theorem CategoryTheory.Limits.biprod.symmetry'_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) {Z : C} (h : P ⊞ Q ⟶ Z) : CategoryStruct.comp (lift snd fst) (CategoryStruct.comp (lift snd fst) h) = h

theorem CategoryTheory.Limits.biprod.symmetry {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) : CategoryStruct.comp (braiding P Q).hom (braiding Q P).hom = CategoryStruct.id (P ⊞ Q)

The braiding isomorphism is symmetric.

theorem CategoryTheory.Limits.biprod.symmetry_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q : C) {Z : C} (h : P ⊞ Q ⟶ Z) : CategoryStruct.comp (braiding P Q).hom (CategoryStruct.comp (braiding Q P).hom h) = h

The braiding isomorphism is symmetric.

noncomputable def CategoryTheory.Limits.biprod.associator {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q R : C) : (P ⊞ Q) ⊞ R ≅ P ⊞ Q ⊞ R

The associator isomorphism which associates a binary biproduct.

@[simp]

theorem CategoryTheory.Limits.biprod.associator_hom {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q R : C) : (associator P Q R).hom = lift (CategoryStruct.comp fst fst) (lift (CategoryStruct.comp fst snd) snd)

@[simp]

theorem CategoryTheory.Limits.biprod.associator_inv {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] (P Q R : C) : (associator P Q R).inv = lift (lift fst (CategoryStruct.comp snd fst)) (CategoryStruct.comp snd snd)

theorem CategoryTheory.Limits.biprod.associator_natural {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) : CategoryStruct.comp (map (map f g) h) (associator X Y Z).hom = CategoryStruct.comp (associator U V W).hom (map f (map g h))

The associator isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.biprod.associator_natural_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) {Z✝ : C} (h✝ : X ⊞ Y ⊞ Z ⟶ Z✝) : CategoryStruct.comp (map (map f g) h) (CategoryStruct.comp (associator X Y Z).hom h✝) = CategoryStruct.comp (associator U V W).hom (CategoryStruct.comp (map f (map g h)) h✝)

The associator isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.biprod.associator_inv_natural {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) : CategoryStruct.comp (map f (map g h)) (associator X Y Z).inv = CategoryStruct.comp (associator U V W).inv (map (map f g) h)

The associator isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.biprod.associator_inv_natural_assoc {C : Type uC} [Category.{uC', uC} C] [HasZeroMorphisms C] [HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) {Z✝ : C} (h✝ : (X ⊞ Y) ⊞ Z ⟶ Z✝) : CategoryStruct.comp (map f (map g h)) (CategoryStruct.comp (associator X Y Z).inv h✝) = CategoryStruct.comp (associator U V W).inv (CategoryStruct.comp (map (map f g) h) h✝)

The associator isomorphism can be passed through a map by swapping the order.

def CategoryTheory.Indecomposable {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X : C) : Prop

An object is indecomposable if it cannot be written as the biproduct of two nonzero objects.

theorem CategoryTheory.isIso_left_of_isIso_biprod_map {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [IsIso (Limits.biprod.map f g)] : IsIso f

If

(f 0)
(0 g)

is invertible, then f is invertible.

theorem CategoryTheory.isIso_right_of_isIso_biprod_map {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [IsIso (Limits.biprod.map f g)] : IsIso g

If

(f 0)
(0 g)

is invertible, then g is invertible.