Biproducts and binary biproducts

We introduce the notion of (finite) biproducts and 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.

For biproducts indexed by a Fintype J, a bicone again consists of a cone point X and morphisms π j : X ⟶ F j and ι j : F j ⟶ X for each j, such that ι j ≫ π j' is the identity when j = j' and zero otherwise.

Notation

As ⊕ is already taken for the sum of types, we introduce the notation X ⊞ Y for a binary biproduct. We introduce ⨁ f for the indexed biproduct.

Implementation notes

Prior to https://github.com/leanprover-community/mathlib3/pull/14046, HasFiniteBiproducts required a DecidableEq instance on the indexing type. As this had no pay-off (everything about limits is non-constructive in mathlib), and occasional cost (constructing decidability instances appropriate for constructions involving the indexing type), we made everything classical.

structure CategoryTheory.Limits.Bicone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) : Type (max (max uC uC') w)

A c : Bicone F is:

• an object c.pt and
• morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
• such that ι j ≫ π j' is the identity when j = j' and zero otherwise.

• pt : C

  A c : Bicone F is:

  • an object c.pt and
  • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
  • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
• π : (j : J) → self.pt ⟶ F j

  A c : Bicone F is:

  • an object c.pt and
  • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
  • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
• ι : (j : J) → F j ⟶ self.pt

  A c : Bicone F is:

  • an object c.pt and
  • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
  • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
• ι_π : ∀ (j j' : J), CategoryTheory.CategoryStruct.comp (self.ι j) (self.π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0

  A c : Bicone F is:

  • an object c.pt and
  • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
  • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.

Instances For

• CategoryTheory.Limits.Bicone.category

@[simp]

theorem CategoryTheory.Limits.bicone_ι_π_self {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j) = CategoryTheory.CategoryStruct.id (F j)

@[simp]

theorem CategoryTheory.Limits.bicone_ι_π_self_assoc {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) {Z : C} (h : F j ⟶ Z) : CategoryTheory.CategoryStruct.comp (B.ι j) (CategoryTheory.CategoryStruct.comp (B.π j) h) = h

@[simp]

theorem CategoryTheory.Limits.bicone_ι_π_ne {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) {j j' : J} (h : j ≠ j') : CategoryTheory.CategoryStruct.comp (B.ι j) (B.π j') = 0

@[simp]

theorem CategoryTheory.Limits.bicone_ι_π_ne_assoc {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) {j j' : J} (h : j ≠ j') {Z : C} (h✝ : F j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (B.ι j) (CategoryTheory.CategoryStruct.comp (B.π j') h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

structure CategoryTheory.Limits.BiconeMorphism {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (A B : CategoryTheory.Limits.Bicone F) : Type uC'

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

• hom : A.pt ⟶ B.pt

  A morphism between the two vertex objects of the bicones

• wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp self.hom (B.π j) = A.π j

  The triangle consisting of the two natural transformations and hom commutes

• wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) self.hom = B.ι j

  The triangle consisting of the two natural transformations and hom commutes

@[simp]

theorem CategoryTheory.Limits.BiconeMorphism.wι_assoc {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) {Z : C} (h : B.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.ι j) (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (B.ι j) h

@[simp]

theorem CategoryTheory.Limits.BiconeMorphism.wπ_assoc {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {A B : CategoryTheory.Limits.Bicone F} (self : CategoryTheory.Limits.BiconeMorphism A B) (j : J) {Z : C} (h : F j ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (B.π j) h) = CategoryTheory.CategoryStruct.comp (A.π j) h

instance CategoryTheory.Limits.Bicone.category {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Category.{uC', max (max uC uC') w} (CategoryTheory.Limits.Bicone F)

The category of bicones on a given diagram.

Equations

• CategoryTheory.Limits.Bicone.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.Bicone.category_comp_hom {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {X✝ Y✝ Z✝ : CategoryTheory.Limits.Bicone F} (f : X✝ ⟶ Y✝) (g : Y✝ ⟶ Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[simp]

theorem CategoryTheory.Limits.Bicone.category_id_hom {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt

theorem CategoryTheory.Limits.BiconeMorphism.ext {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

def CategoryTheory.Limits.Bicones.ext {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (φ : c.pt ≅ c'.pt) (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j := by aesop_cat) (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j := by aesop_cat) : c ≅ c'

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

Equations

• CategoryTheory.Limits.Bicones.ext φ wι wπ = { hom := { hom := φ.hom, wπ := ⋯, wι := ⋯ }, inv := { hom := φ.inv, wπ := ⋯, wι := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Bicones.ext_hom_hom {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (φ : c.pt ≅ c'.pt) (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j := by aesop_cat) (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j := by aesop_cat) : (CategoryTheory.Limits.Bicones.ext φ wι wπ).hom.hom = φ.hom

@[simp]

theorem CategoryTheory.Limits.Bicones.ext_inv_hom {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F} (φ : c.pt ≅ c'.pt) (wι : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j := by aesop_cat) (wπ : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j := by aesop_cat) : (CategoryTheory.Limits.Bicones.ext φ wι wπ).inv.hom = φ.inv

def CategoryTheory.Limits.Bicones.functoriality {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Bicone (G.obj ∘ F))

A functor G : C ⥤ D sends bicones over F to bicones over G.obj ∘ F functorially.

Equations

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

Instances For

• CategoryTheory.Limits.Bicones.functoriality_faithful
• CategoryTheory.Limits.Bicones.functoriality_full

@[simp]

theorem CategoryTheory.Limits.Bicones.functoriality_obj_pt {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) : ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).pt = G.obj A.pt

@[simp]

theorem CategoryTheory.Limits.Bicones.functoriality_map_hom {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X✝ Y✝ : CategoryTheory.Limits.Bicone F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.Bicones.functoriality F G).map f).hom = G.map f.hom

@[simp]

theorem CategoryTheory.Limits.Bicones.functoriality_obj_ι {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) (j : J) : ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).ι j = G.map (A.ι j)

@[simp]

theorem CategoryTheory.Limits.Bicones.functoriality_obj_π {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : J → C) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] (A : CategoryTheory.Limits.Bicone F) (j : J) : ((CategoryTheory.Limits.Bicones.functoriality F G).obj A).π j = G.map (A.π j)

instance CategoryTheory.Limits.Bicones.functoriality_full {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] {F : J → C} (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [G.Full] [G.Faithful] : (CategoryTheory.Limits.Bicones.functoriality F G).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.Bicones.functoriality_faithful {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] {F : J → C} (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] [G.Faithful] : (CategoryTheory.Limits.Bicones.functoriality F G).Faithful

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.Bicone.toConeFunctor {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F))

Extract the cone from a bicone.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.Bicone.toCone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor F)

A shorthand for toConeFunctor.obj

Equations

• B.toCone = CategoryTheory.Limits.Bicone.toConeFunctor.obj B

@[simp]

theorem CategoryTheory.Limits.Bicone.toCone_pt {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : B.toCone.pt = B.pt

@[simp]

theorem CategoryTheory.Limits.Bicone.toCone_π_app {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCone.π.app j = B.π j.as

theorem CategoryTheory.Limits.Bicone.toCone_π_app_mk {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : B.toCone.π.app { as := j } = B.π j

@[simp]

theorem CategoryTheory.Limits.Bicone.toCone_proj {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.Limits.Fan.proj B.toCone j = B.π j

def CategoryTheory.Limits.Bicone.toCoconeFunctor {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} : CategoryTheory.Functor (CategoryTheory.Limits.Bicone F) (CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F))

Extract the cocone from a bicone.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.Bicone.toCocone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor F)

A shorthand for toCoconeFunctor.obj

Equations

• B.toCocone = CategoryTheory.Limits.Bicone.toCoconeFunctor.obj B

@[simp]

theorem CategoryTheory.Limits.Bicone.toCocone_pt {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : B.toCocone.pt = B.pt

@[simp]

theorem CategoryTheory.Limits.Bicone.toCocone_ι_app {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : CategoryTheory.Discrete J) : B.toCocone.ι.app j = B.ι j.as

@[simp]

theorem CategoryTheory.Limits.Bicone.toCocone_inj {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : CategoryTheory.Limits.Cofan.inj B.toCocone j = B.ι j

theorem CategoryTheory.Limits.Bicone.toCocone_ι_app_mk {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J) : B.toCocone.ι.app { as := j } = B.ι j

def CategoryTheory.Limits.Bicone.ofLimitCone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) : CategoryTheory.Limits.Bicone f

We can turn any limit cone over a discrete collection of objects into a bicone.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Bicone.ofLimitCone_pt {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).pt = t.pt

@[simp]

theorem CategoryTheory.Limits.Bicone.ofLimitCone_π {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).π j = t.π.app { as := j }

@[simp]

theorem CategoryTheory.Limits.Bicone.ofLimitCone_ι {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsLimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofLimitCone ht).ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun (j' : J) => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)

theorem CategoryTheory.Limits.Bicone.ι_of_isLimit {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsLimit t.toCone) (j : J) : t.ι j = ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun (j' : J) => if h : j = j' then CategoryTheory.eqToHom ⋯ else 0)

def CategoryTheory.Limits.Bicone.ofColimitCocone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) : CategoryTheory.Limits.Bicone f

We can turn any colimit cocone over a discrete collection of objects into a bicone.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Bicone.ofColimitCocone_ι {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).ι j = t.ι.app { as := j }

@[simp]

theorem CategoryTheory.Limits.Bicone.ofColimitCocone_π {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) (j : J) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun (j' : J) => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)

@[simp]

theorem CategoryTheory.Limits.Bicone.ofColimitCocone_pt {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Cocone (CategoryTheory.Discrete.functor f)} (ht : CategoryTheory.Limits.IsColimit t) : (CategoryTheory.Limits.Bicone.ofColimitCocone ht).pt = t.pt

theorem CategoryTheory.Limits.Bicone.π_of_isColimit {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f} (ht : CategoryTheory.Limits.IsColimit t.toCocone) (j : J) : t.π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun (j' : J) => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)

structure CategoryTheory.Limits.Bicone.IsBilimit {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) : Type (max (max uC uC') w)

Structure witnessing that a bicone is both a limit cone and a colimit cocone.

• isLimit : CategoryTheory.Limits.IsLimit B.toCone

  Structure witnessing that a bicone is both a limit cone and a colimit cocone.

• isColimit : CategoryTheory.Limits.IsColimit B.toCocone

  Structure witnessing that a bicone is both a limit cone and a colimit cocone.

Instances For

• CategoryTheory.Limits.Bicone.subsingleton_isBilimit

theorem CategoryTheory.Limits.Bicone.IsBilimit.ext {J : Type w} {C : Type uC} {inst✝ : CategoryTheory.Category.{uC', uC} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F} {x y : B.IsBilimit} (isLimit : x.isLimit = y.isLimit) (isColimit : x.isColimit = y.isColimit) : x = y

instance CategoryTheory.Limits.Bicone.subsingleton_isBilimit {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {c : CategoryTheory.Limits.Bicone f} : Subsingleton c.IsBilimit

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.Bicone.whisker {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : CategoryTheory.Limits.Bicone (f ∘ ⇑g)

Whisker a bicone with an equivalence between the indexing types.

Equations

• c.whisker g = { pt := c.pt, π := fun (k : K) => c.π (g k), ι := fun (k : K) => c.ι (g k), ι_π := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Bicone.whisker_ι {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) (k : K) : (c.whisker g).ι k = c.ι (g k)

@[simp]

theorem CategoryTheory.Limits.Bicone.whisker_π {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) (k : K) : (c.whisker g).π k = c.π (g k)

@[simp]

theorem CategoryTheory.Limits.Bicone.whisker_pt {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).pt = c.pt

def CategoryTheory.Limits.Bicone.whiskerToCone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).toCone ≅ (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Discrete.functorComp f ⇑g).inv).obj (CategoryTheory.Limits.Cone.whisker (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCone)

Taking the cone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cone and postcomposing with a suitable isomorphism.

Equations

• c.whiskerToCone g = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (c.whisker g).toCone.pt) ⋯

def CategoryTheory.Limits.Bicone.whiskerToCocone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).toCocone ≅ (CategoryTheory.Limits.Cocones.precompose (CategoryTheory.Discrete.functorComp f ⇑g).hom).obj (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g)) c.toCocone)

Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cocone and precomposing with a suitable isomorphism.

Equations

• c.whiskerToCocone g = CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl (c.whisker g).toCocone.pt) ⋯

def CategoryTheory.Limits.Bicone.whiskerIsBilimitIff {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} {f : J → C} (c : CategoryTheory.Limits.Bicone f) (g : K ≃ J) : (c.whisker g).IsBilimit ≃ c.IsBilimit

Whiskering a bicone with an equivalence between types preserves being a bilimit bicone.

Equations

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

structure CategoryTheory.Limits.LimitBicone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) : Type (max (max uC uC') w)

A bicone over F : J → C, which is both a limit cone and a colimit cocone.

• bicone : CategoryTheory.Limits.Bicone F

  A bicone over F : J → C, which is both a limit cone and a colimit cocone.

• isBilimit : self.bicone.IsBilimit

  A bicone over F : J → C, which is both a limit cone and a colimit cocone.

class CategoryTheory.Limits.HasBiproduct {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) : Prop

HasBiproduct F expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram F.

• mk' :: (
• exists_biproduct : Nonempty (CategoryTheory.Limits.LimitBicone F)

  HasBiproduct F expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram F.

• )

Instances

• CategoryTheory.Limits.hasBiproduct_unique
• CategoryTheory.Limits.instHasBiproductSigmaFstSndOfBiproduct

theorem CategoryTheory.Limits.HasBiproduct.mk {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (d : CategoryTheory.Limits.LimitBicone F) : CategoryTheory.Limits.HasBiproduct F

def CategoryTheory.Limits.getBiproductData {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.LimitBicone F

Use the axiom of choice to extract explicit BiproductData F from HasBiproduct F.

Equations

• CategoryTheory.Limits.getBiproductData F = Classical.choice ⋯

def CategoryTheory.Limits.biproduct.bicone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.Bicone F

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

Equations

• CategoryTheory.Limits.biproduct.bicone F = (CategoryTheory.Limits.getBiproductData F).bicone

def CategoryTheory.Limits.biproduct.isBilimit {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : (CategoryTheory.Limits.biproduct.bicone F).IsBilimit

biproduct.bicone F is a bilimit bicone.

Equations

• CategoryTheory.Limits.biproduct.isBilimit F = (CategoryTheory.Limits.getBiproductData F).isBilimit

def CategoryTheory.Limits.biproduct.isLimit {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.biproduct.bicone F).toCone

biproduct.bicone F is a limit cone.

Equations

• CategoryTheory.Limits.biproduct.isLimit F = (CategoryTheory.Limits.getBiproductData F).isBilimit.isLimit

def CategoryTheory.Limits.biproduct.isColimit {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.biproduct.bicone F).toCocone

biproduct.bicone F is a colimit cocone.

Equations

• CategoryTheory.Limits.biproduct.isColimit F = (CategoryTheory.Limits.getBiproductData F).isBilimit.isColimit

@[instance 100]

instance CategoryTheory.Limits.hasProduct_of_hasBiproduct {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.HasProduct F

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.hasCoproduct_of_hasBiproduct {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [CategoryTheory.Limits.HasBiproduct F] : CategoryTheory.Limits.HasCoproduct F

Equations

• ⋯ = ⋯

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

C has biproducts of shape J if we have a limit and a colimit, with the same cone points, of every function F : J → C.

• has_biproduct : ∀ (F : J → C), CategoryTheory.Limits.HasBiproduct F

Instances

• CategoryTheory.Limits.hasBiproductsOfShape_finite

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

HasFiniteBiproducts C represents a choice of biproduct for every family of objects in C indexed by a finite type.

• out : ∀ (n : ℕ), CategoryTheory.Limits.HasBiproductsOfShape (Fin n) C

  HasFiniteBiproducts C represents a choice of biproduct for every family of objects in C indexed by a finite type.

theorem CategoryTheory.Limits.hasBiproductsOfShape_of_equiv {J : Type w} (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type w'} [CategoryTheory.Limits.HasBiproductsOfShape K C] (e : J ≃ K) : CategoryTheory.Limits.HasBiproductsOfShape J C

@[instance 100]

instance CategoryTheory.Limits.hasBiproductsOfShape_finite {J : Type w} (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [Finite J] : CategoryTheory.Limits.HasBiproductsOfShape J C

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteBiproducts (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasFiniteProducts C

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasFiniteCoproducts C

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.hasProductsOfShape_of_hasBiproductsOfShape {J : Type w} (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] : CategoryTheory.Limits.HasProductsOfShape J C

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.hasCoproductsOfShape_of_hasBiproductsOfShape {J : Type w} (C : Type uC) [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] : CategoryTheory.Limits.HasCoproductsOfShape J C

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.biproductIso {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : J → C) [CategoryTheory.Limits.HasBiproduct F] : ∏ᶜ F ≅ ∐ F

The isomorphism between the specified limit and the specified colimit for a functor with a bilimit.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.biproduct {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] : C

biproduct f computes the biproduct of a family of elements f. (It is defined as an abbreviation for limit (Discrete.functor f), so for most facts about biproduct f, you will just use general facts about limits and colimits.)

Equations

• (⨁ f) = (CategoryTheory.Limits.biproduct.bicone f).pt

def CategoryTheory.Limits.«term⨁_» : Lean.ParserDescr

biproduct f computes the biproduct of a family of elements f. (It is defined as an abbreviation for limit (Discrete.functor f), so for most facts about biproduct f, you will just use general facts about limits and colimits.)

Equations

• CategoryTheory.Limits.«term⨁_» = Lean.ParserDescr.node `CategoryTheory.Limits.«term⨁_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨁ ") (Lean.ParserDescr.cat `term 20))

@[reducible, inline]

abbrev CategoryTheory.Limits.biproduct.π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (b : J) : ⨁ f ⟶ f b

The projection onto a summand of a biproduct.

Equations

• CategoryTheory.Limits.biproduct.π f b = (CategoryTheory.Limits.biproduct.bicone f).π b

Instances For

• CategoryTheory.Limits.biproduct.π_epi
• CategoryTheory.Limits.instHasKernelπ

@[simp]

theorem CategoryTheory.Limits.biproduct.bicone_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (b : J) : (CategoryTheory.Limits.biproduct.bicone f).π b = CategoryTheory.Limits.biproduct.π f b

@[reducible, inline]

abbrev CategoryTheory.Limits.biproduct.ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (b : J) : f b ⟶ ⨁ f

The inclusion into a summand of a biproduct.

Equations

• CategoryTheory.Limits.biproduct.ι f b = (CategoryTheory.Limits.biproduct.bicone f).ι b

Instances For

• CategoryTheory.Limits.biproduct.ι_mono
• CategoryTheory.Limits.instHasCokernelι

@[simp]

theorem CategoryTheory.Limits.biproduct.bicone_ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (b : J) : (CategoryTheory.Limits.biproduct.bicone f).ι b = CategoryTheory.Limits.biproduct.ι f b

theorem CategoryTheory.Limits.biproduct.ι_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (j j' : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.π f j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0

Note that as this lemma has an if in the statement, we include a DecidableEq argument. This means you may not be able to simp using this lemma unless you open scoped Classical.

theorem CategoryTheory.Limits.biproduct.ι_π_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [DecidableEq J] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (j j' : J) {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h) = CategoryTheory.CategoryStruct.comp (if h : j = j' then CategoryTheory.eqToHom ⋯ else 0) h

theorem CategoryTheory.Limits.biproduct.ι_π_self {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.π f j) = CategoryTheory.CategoryStruct.id (f j)

theorem CategoryTheory.Limits.biproduct.ι_π_self_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (j : J) {Z : C} (h : f j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) h) = h

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_π_ne {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (h : j ≠ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.π f j') = 0

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_π_ne_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (h : j ≠ j') {Z : C} (h✝ : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem CategoryTheory.Limits.biproduct.eqToHom_comp_ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.biproduct.ι f j') = CategoryTheory.Limits.biproduct.ι f j

@[simp]

theorem CategoryTheory.Limits.biproduct.eqToHom_comp_ι_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') {Z : C} (h : ⨁ f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) h

@[simp]

theorem CategoryTheory.Limits.biproduct.π_comp_eqToHom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.Limits.biproduct.π f j'

@[simp]

theorem CategoryTheory.Limits.biproduct.π_comp_eqToHom_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h

@[reducible, inline]

abbrev CategoryTheory.Limits.biproduct.lift {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {P : C} (p : (b : J) → P ⟶ f b) : P ⟶ ⨁ f

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

Equations

• CategoryTheory.Limits.biproduct.lift p = (CategoryTheory.Limits.biproduct.isLimit f).lift (CategoryTheory.Limits.Fan.mk P p)

@[reducible, inline]

abbrev CategoryTheory.Limits.biproduct.desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {P : C} (p : (b : J) → f b ⟶ P) : ⨁ f ⟶ P

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

Equations

• CategoryTheory.Limits.biproduct.desc p = (CategoryTheory.Limits.biproduct.isColimit f).desc (CategoryTheory.Limits.Cofan.mk P p)

@[simp]

theorem CategoryTheory.Limits.biproduct.lift_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {P : C} (p : (b : J) → P ⟶ f b) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift p) (CategoryTheory.Limits.biproduct.π f j) = p j

@[simp]

theorem CategoryTheory.Limits.biproduct.lift_π_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {P : C} (p : (b : J) → P ⟶ f b) (j : J) {Z : C} (h : f j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) h) = CategoryTheory.CategoryStruct.comp (p j) h

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {P : C} (p : (b : J) → f b ⟶ P) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.desc p) = p j

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_desc_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {P : C} (p : (b : J) → f b ⟶ P) (j : J) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc p) h) = CategoryTheory.CategoryStruct.comp (p j) h

@[reducible, inline]

abbrev CategoryTheory.Limits.biproduct.map {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ⟶ g b) : ⨁ f ⟶ ⨁ g

Given a collection of maps between corresponding summands of a pair of biproducts indexed by the same type, we obtain a map between the biproducts.

Equations

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

Instances For

• CategoryTheory.Limits.biproduct.map_epi
• CategoryTheory.Limits.biproduct.map_mono

@[reducible, inline]

abbrev CategoryTheory.Limits.biproduct.map' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ⟶ g b) : ⨁ f ⟶ ⨁ g

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

Equations

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

theorem CategoryTheory.Limits.biproduct.hom_ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {Z : C} (g h : Z ⟶ ⨁ f) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.π f j) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.biproduct.π f j)) : g = h

theorem CategoryTheory.Limits.biproduct.hom_ext' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] {Z : C} (g h : ⨁ f ⟶ Z) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) h) : g = h

def CategoryTheory.Limits.biproduct.isoProduct {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] : ⨁ f ≅ ∏ᶜ f

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

Equations

• CategoryTheory.Limits.biproduct.isoProduct f = (CategoryTheory.Limits.biproduct.isLimit f).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor f))

@[simp]

theorem CategoryTheory.Limits.biproduct.isoProduct_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] : (CategoryTheory.Limits.biproduct.isoProduct f).hom = CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π f)

@[simp]

theorem CategoryTheory.Limits.biproduct.isoProduct_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] : (CategoryTheory.Limits.biproduct.isoProduct f).inv = CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π f)

def CategoryTheory.Limits.biproduct.isoCoproduct {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] : ⨁ f ≅ ∐ f

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.biproduct.isoCoproduct_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] : (CategoryTheory.Limits.biproduct.isoCoproduct f).inv = CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι f)

@[simp]

theorem CategoryTheory.Limits.biproduct.isoCoproduct_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [CategoryTheory.Limits.HasBiproduct f] : (CategoryTheory.Limits.biproduct.isoCoproduct f).hom = CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι f)

def CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] : CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.lim

If a category has biproducts of a shape J, its colim and lim functor on diagrams over J are isomorphic.

Equations

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

@[simp]

theorem CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_inv_app {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.inv.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.Pi.π fun (j : J) => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.Sigma.ι fun (j : J) => X.obj { as := j })) (CategoryTheory.Limits.Sigma.isoColimit X).hom))

@[simp]

theorem CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim_hom_app {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBiproductsOfShape J C] (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C) : CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.hom.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι fun (j : J) => X.obj { as := j })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π fun (j : J) => X.obj { as := j })) (CategoryTheory.Limits.Pi.isoLimit X).hom))

theorem CategoryTheory.Limits.biproduct.map_eq_map' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ⟶ g b) : CategoryTheory.Limits.biproduct.map p = CategoryTheory.Limits.biproduct.map' p

@[simp]

theorem CategoryTheory.Limits.biproduct.map_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) (CategoryTheory.Limits.biproduct.π g j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (p j)

@[simp]

theorem CategoryTheory.Limits.biproduct.map_π_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J) {Z : C} (h : g j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) (CategoryTheory.CategoryStruct.comp (p j) h)

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_map {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.map p) = CategoryTheory.CategoryStruct.comp (p j) (CategoryTheory.Limits.biproduct.ι g j)

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_map_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J) {Z : C} (h : ⨁ g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) h) = CategoryTheory.CategoryStruct.comp (p j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι g j) h)

@[simp]

theorem CategoryTheory.Limits.biproduct.map_desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) {P : C} (k : (j : J) → g j ⟶ P) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) (CategoryTheory.Limits.biproduct.desc k) = CategoryTheory.Limits.biproduct.desc fun (j : J) => CategoryTheory.CategoryStruct.comp (p j) (k j)

@[simp]

theorem CategoryTheory.Limits.biproduct.map_desc_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) {P : C} (k : (j : J) → g j ⟶ P) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc fun (j : J) => CategoryTheory.CategoryStruct.comp (p j) (k j)) h

@[simp]

theorem CategoryTheory.Limits.biproduct.lift_map {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] {P : C} (k : (j : J) → P ⟶ f j) (p : (j : J) → f j ⟶ g j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift k) (CategoryTheory.Limits.biproduct.map p) = CategoryTheory.Limits.biproduct.lift fun (j : J) => CategoryTheory.CategoryStruct.comp (k j) (p j)

@[simp]

theorem CategoryTheory.Limits.biproduct.lift_map_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] {P : C} (k : (j : J) → P ⟶ f j) (p : (j : J) → f j ⟶ g j) {Z : C} (h : ⨁ g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.lift fun (j : J) => CategoryTheory.CategoryStruct.comp (k j) (p j)) h

def CategoryTheory.Limits.biproduct.mapIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ≅ g b) : ⨁ f ≅ ⨁ g

Given a collection of isomorphisms between corresponding summands of a pair of biproducts indexed by the same type, we obtain an isomorphism between the biproducts.

Equations

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

@[simp]

theorem CategoryTheory.Limits.biproduct.mapIso_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ≅ g b) : (CategoryTheory.Limits.biproduct.mapIso p).hom = CategoryTheory.Limits.biproduct.map fun (b : J) => (p b).hom

@[simp]

theorem CategoryTheory.Limits.biproduct.mapIso_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (b : J) → f b ≅ g b) : (CategoryTheory.Limits.biproduct.mapIso p).inv = CategoryTheory.Limits.biproduct.map fun (b : J) => (p b).inv

instance CategoryTheory.Limits.biproduct.map_epi {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Epi (p j)] : CategoryTheory.Epi (CategoryTheory.Limits.biproduct.map p)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.Pi.map_epi {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Epi (p j)] : CategoryTheory.Epi (CategoryTheory.Limits.Pi.map p)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.biproduct.map_mono {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Mono (p j)] : CategoryTheory.Mono (CategoryTheory.Limits.biproduct.map p)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.Sigma.map_mono {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Mono (p j)] : CategoryTheory.Mono (CategoryTheory.Limits.Sigma.map p)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.biproduct.whiskerEquiv {J : Type w} {K : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] : ⨁ f ≅ ⨁ g

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

Unfortunately there are two natural ways to define each direction of this isomorphism (because it is true for both products and coproducts separately). We give the alternative definitions as lemmas below.

Equations

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

@[simp]

theorem CategoryTheory.Limits.biproduct.whiskerEquiv_inv {J : Type w} {K : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] : (CategoryTheory.Limits.biproduct.whiskerEquiv e w).inv = CategoryTheory.Limits.biproduct.desc fun (k : K) => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (w (e.symm k)).hom (CategoryTheory.Limits.biproduct.ι f (e.symm k)))

@[simp]

theorem CategoryTheory.Limits.biproduct.whiskerEquiv_hom {J : Type w} {K : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] : (CategoryTheory.Limits.biproduct.whiskerEquiv e w).hom = CategoryTheory.Limits.biproduct.desc fun (j : J) => CategoryTheory.CategoryStruct.comp (w j).inv (CategoryTheory.Limits.biproduct.ι g (e j))

theorem CategoryTheory.Limits.biproduct.whiskerEquiv_hom_eq_lift {J : Type w} {K : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] : (CategoryTheory.Limits.biproduct.whiskerEquiv e w).hom = CategoryTheory.Limits.biproduct.lift fun (k : K) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f (e.symm k)) (CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom ⋯))

theorem CategoryTheory.Limits.biproduct.whiskerEquiv_inv_eq_lift {J : Type w} {K : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] : (CategoryTheory.Limits.biproduct.whiskerEquiv e w).inv = CategoryTheory.Limits.biproduct.lift fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g (e j)) (w j).hom

instance CategoryTheory.Limits.instHasBiproductSigmaFstSndOfBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => ⨁ g i] : CategoryTheory.Limits.HasBiproduct fun (p : (i : ι) × f i) => g p.fst p.snd

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.biproductBiproductIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => ⨁ g i] : (⨁ fun (i : ι) => ⨁ g i) ≅ ⨁ fun (p : (i : ι) × f i) => g p.fst p.snd

An iterated biproduct is a biproduct over a sigma type.

Equations

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

@[simp]

theorem CategoryTheory.Limits.biproductBiproductIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => ⨁ g i] : (CategoryTheory.Limits.biproductBiproductIso f g).inv = CategoryTheory.Limits.biproduct.lift fun (i : ι) => CategoryTheory.Limits.biproduct.lift fun (x : f i) => CategoryTheory.Limits.biproduct.π (fun (p : (i : ι) × f i) => g p.fst p.snd) ⟨i, x⟩

@[simp]

theorem CategoryTheory.Limits.biproductBiproductIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => ⨁ g i] : (CategoryTheory.Limits.biproductBiproductIso f g).hom = CategoryTheory.Limits.biproduct.lift fun (x : (i : ι) × f i) => match x with | ⟨i, x⟩ => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (i : ι) => ⨁ g i) i) (CategoryTheory.Limits.biproduct.π (g i) x)

def CategoryTheory.Limits.biproduct.fromSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] : ⨁ Subtype.restrict p f ⟶ ⨁ f

The canonical morphism from the biproduct over a restricted index type to the biproduct of the full index type.

Equations

• CategoryTheory.Limits.biproduct.fromSubtype f p = CategoryTheory.Limits.biproduct.desc fun (j : Subtype p) => CategoryTheory.Limits.biproduct.ι f ↑j

Instances For

• CategoryTheory.Limits.instHasCokernelFromSubtype

def CategoryTheory.Limits.biproduct.toSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] : ⨁ f ⟶ ⨁ Subtype.restrict p f

The canonical morphism from a biproduct to the biproduct over a restriction of its index type.

Equations

• CategoryTheory.Limits.biproduct.toSubtype f p = CategoryTheory.Limits.biproduct.lift fun (x : Subtype p) => CategoryTheory.Limits.biproduct.π f ↑x

Instances For

• CategoryTheory.Limits.instHasKernelToSubtype

@[simp]

theorem CategoryTheory.Limits.biproduct.fromSubtype_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) (CategoryTheory.Limits.biproduct.π f j) = if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0

@[simp]

theorem CategoryTheory.Limits.biproduct.fromSubtype_π_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] (j : J) {Z : C} (h : f j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j) h) = CategoryTheory.CategoryStruct.comp (if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0) h

theorem CategoryTheory.Limits.biproduct.fromSubtype_eq_lift {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] : CategoryTheory.Limits.biproduct.fromSubtype f p = CategoryTheory.Limits.biproduct.lift fun (j : J) => if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0

theorem CategoryTheory.Limits.biproduct.fromSubtype_π_subtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) (CategoryTheory.Limits.biproduct.π f ↑j) = CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j

theorem CategoryTheory.Limits.biproduct.fromSubtype_π_subtype_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C} (h : f ↑j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f ↑j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j) h

@[simp]

theorem CategoryTheory.Limits.biproduct.toSubtype_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) (CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j) = CategoryTheory.Limits.biproduct.π f ↑j

@[simp]

theorem CategoryTheory.Limits.biproduct.toSubtype_π_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C} (h : Subtype.restrict p f j ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f ↑j) h

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_toSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.Limits.biproduct.toSubtype f p) = if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_toSubtype_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] (j : J) {Z : C} (h : ⨁ Subtype.restrict p f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) h) = CategoryTheory.CategoryStruct.comp (if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0) h

theorem CategoryTheory.Limits.biproduct.toSubtype_eq_desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] : CategoryTheory.Limits.biproduct.toSubtype f p = CategoryTheory.Limits.biproduct.desc fun (j : J) => if h : p j then CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0

theorem CategoryTheory.Limits.biproduct.ι_toSubtype_subtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f ↑j) (CategoryTheory.Limits.biproduct.toSubtype f p) = CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j

theorem CategoryTheory.Limits.biproduct.ι_toSubtype_subtype_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C} (h : ⨁ Subtype.restrict p f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f ↑j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j) h

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_fromSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j) (CategoryTheory.Limits.biproduct.fromSubtype f p) = CategoryTheory.Limits.biproduct.ι f ↑j

@[simp]

theorem CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] (j : Subtype p) {Z : C} (h : ⨁ f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (Subtype.restrict p f) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f ↑j) h

@[simp]

theorem CategoryTheory.Limits.biproduct.fromSubtype_toSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) (CategoryTheory.Limits.biproduct.toSubtype f p) = CategoryTheory.CategoryStruct.id (⨁ Subtype.restrict p f)

@[simp]

theorem CategoryTheory.Limits.biproduct.fromSubtype_toSubtype_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] {Z : C} (h : ⨁ Subtype.restrict p f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) h) = h

@[simp]

theorem CategoryTheory.Limits.biproduct.toSubtype_fromSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) (CategoryTheory.Limits.biproduct.fromSubtype f p) = CategoryTheory.Limits.biproduct.map fun (j : J) => if p j then CategoryTheory.CategoryStruct.id (f j) else 0

@[simp]

theorem CategoryTheory.Limits.biproduct.toSubtype_fromSubtype_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (p : J → Prop) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [DecidablePred p] {Z : C} (h : ⨁ f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map fun (j : J) => if p j then CategoryTheory.CategoryStruct.id (f j) else 0) h

def CategoryTheory.Limits.biproduct.isLimitFromSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f fun (j : J) => j ≠ i) ⋯)

The kernel of biproduct.π f i is the inclusion from the biproduct which omits i from the index set J into the biproduct over J.

Equations

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

instance CategoryTheory.Limits.instHasKernelπ {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.biproduct.π f i)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.kernelBiproductπIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : CategoryTheory.Limits.kernel (CategoryTheory.Limits.biproduct.π f i) ≅ ⨁ Subtype.restrict (fun (j : J) => j ≠ i) f

The kernel of biproduct.π f i is ⨁ Subtype.restrict {i}ᶜ f.

Equations

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

@[simp]

theorem CategoryTheory.Limits.kernelBiproductπIso_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : (CategoryTheory.Limits.kernelBiproductπIso f i).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0) (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f fun (j : J) => ¬j = i) ⋯)

@[simp]

theorem CategoryTheory.Limits.kernelBiproductπIso_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : (CategoryTheory.Limits.kernelBiproductπIso f i).hom = (CategoryTheory.Limits.biproduct.isLimitFromSubtype f i).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0))

def CategoryTheory.Limits.biproduct.isColimitToSubtype {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f fun (j : J) => j ≠ i) ⋯)

The cokernel of biproduct.ι f i is the projection from the biproduct over the index set J onto the biproduct omitting i.

Equations

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

instance CategoryTheory.Limits.instHasCokernelι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.biproduct.ι f i)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.cokernelBiproductιIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : CategoryTheory.Limits.cokernel (CategoryTheory.Limits.biproduct.ι f i) ≅ ⨁ Subtype.restrict (fun (j : J) => j ≠ i) f

The cokernel of biproduct.ι f i is ⨁ Subtype.restrict {i}ᶜ f.

Equations

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

@[simp]

theorem CategoryTheory.Limits.cokernelBiproductιIso_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : (CategoryTheory.Limits.cokernelBiproductιIso f i).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f fun (j : J) => ¬j = i) ⋯)

@[simp]

theorem CategoryTheory.Limits.cokernelBiproductιIso_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J) [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j ≠ i) f)] : (CategoryTheory.Limits.cokernelBiproductιIso f i).inv = (CategoryTheory.Limits.biproduct.isColimitToSubtype f i).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.ι f i) 0))

def CategoryTheory.Limits.kernelForkBiproductToSubtype {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0)

The limit cone exhibiting ⨁ Subtype.restrict pᶜ f as the kernel of biproduct.toSubtype f p

Equations

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

@[simp]

theorem CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.kernelForkBiproductToSubtype f p).isLimit = CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {x : C} (g : x ⟶ ⨁ f) (x_1 : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f p) = 0) => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.kernelForkBiproductToSubtype_cone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.kernelForkBiproductToSubtype f p).cone = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯

instance CategoryTheory.Limits.instHasKernelToSubtype {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.biproduct.toSubtype f p)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.kernelBiproductToSubtypeIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : CategoryTheory.Limits.kernel (CategoryTheory.Limits.biproduct.toSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f

The kernel of biproduct.toSubtype f p is ⨁ Subtype.restrict pᶜ f.

Equations

• CategoryTheory.Limits.kernelBiproductToSubtypeIso f p = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.kernelForkBiproductToSubtype f p)

@[simp]

theorem CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).hom = (CategoryTheory.Limits.KernelFork.IsLimit.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯ (fun {x : C} (g : x ⟶ ⨁ f) (x_1 : CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f p) = 0) => CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.biproduct.toSubtype f pᶜ)) ⋯ ⋯).lift (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0))

@[simp]

theorem CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.kernelBiproductToSubtypeIso f p).inv = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0) (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) ⋯)

def CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0)

The colimit cocone exhibiting ⨁ Subtype.restrict pᶜ f as the cokernel of biproduct.fromSubtype f p

Equations

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

@[simp]

theorem CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).cocone = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p).isColimit = CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ (fun {x : C} (g : ⨁ f ⟶ x) (x_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) g = 0) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) g) ⋯ ⋯

instance CategoryTheory.Limits.instHasCokernelFromSubtype {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.biproduct.fromSubtype f p)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.cokernelBiproductFromSubtypeIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : CategoryTheory.Limits.cokernel (CategoryTheory.Limits.biproduct.fromSubtype f p) ≅ ⨁ Subtype.restrict pᶜ f

The cokernel of biproduct.fromSubtype f p is ⨁ Subtype.restrict pᶜ f.

Equations

• CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype f p)

@[simp]

theorem CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0) (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯)

@[simp]

theorem CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Type} [Finite K] [CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : Set K) : (CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).inv = (CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯ (fun {x : C} (g : ⨁ f ⟶ x) (x_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) g = 0) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f pᶜ) g) ⋯ ⋯).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0))

def CategoryTheory.Limits.biproduct.matrix {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) : ⨁ f ⟶ ⨁ g

Convert a (dependently typed) matrix to a morphism of biproducts.

Equations

• CategoryTheory.Limits.biproduct.matrix m = CategoryTheory.Limits.biproduct.desc fun (j : J) => CategoryTheory.Limits.biproduct.lift fun (k : K) => m j k

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.biproduct.matrix_π_assoc {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (k : K) {Z : C} (h : g k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.desc fun (j : J) => m j k) h

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.biproduct.components {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : ⨁ f ⟶ ⨁ g) (j : J) (k : K) : f j ⟶ g k

Extract the matrix components from a morphism of biproducts.

Equations

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

@[simp]

theorem CategoryTheory.Limits.biproduct.matrix_components {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) (j : J) (k : K) : CategoryTheory.Limits.biproduct.components (CategoryTheory.Limits.biproduct.matrix m) j k = m j k

@[simp]

theorem CategoryTheory.Limits.biproduct.components_matrix {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : ⨁ f ⟶ ⨁ g) : (CategoryTheory.Limits.biproduct.matrix fun (j : J) (k : K) => CategoryTheory.Limits.biproduct.components m j k) = m

def CategoryTheory.Limits.biproduct.matrixEquiv {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} : (⨁ f ⟶ ⨁ g) ≃ ((j : J) → (k : K) → f j ⟶ g k)

Morphisms between direct sums are matrices.

Equations

• CategoryTheory.Limits.biproduct.matrixEquiv = { toFun := CategoryTheory.Limits.biproduct.components, invFun := CategoryTheory.Limits.biproduct.matrix, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.Limits.biproduct.matrixEquiv_symm_apply {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : (j : J) → (k : K) → f j ⟶ g k) : CategoryTheory.Limits.biproduct.matrixEquiv.symm m = CategoryTheory.Limits.biproduct.matrix m

@[simp]

theorem CategoryTheory.Limits.biproduct.matrixEquiv_apply {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : J → C} {g : K → C} (m : ⨁ f ⟶ ⨁ g) (j : J) (k : K) : CategoryTheory.Limits.biproduct.matrixEquiv m j k = CategoryTheory.Limits.biproduct.components m j k

instance CategoryTheory.Limits.biproduct.ι_mono {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (b : J) : CategoryTheory.IsSplitMono (CategoryTheory.Limits.biproduct.ι f b)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.biproduct.π_epi {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] (b : J) : CategoryTheory.IsSplitEpi (CategoryTheory.Limits.biproduct.π f b)

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).hom = CategoryTheory.Limits.biproduct.lift b.π

Auxiliary lemma for biproduct.uniqueUpToIso.

theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).inv = CategoryTheory.Limits.biproduct.desc b.ι

Auxiliary lemma for biproduct.uniqueUpToIso.

def CategoryTheory.Limits.biproduct.uniqueUpToIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : b.pt ≅ ⨁ f

Biproducts are unique up to isomorphism. This already follows because bilimits are limits, but in the case of biproducts we can give an isomorphism with particularly nice definitional properties, namely that biproduct.lift b.π and biproduct.desc b.ι are inverses of each other.

Equations

• CategoryTheory.Limits.biproduct.uniqueUpToIso f hb = { hom := CategoryTheory.Limits.biproduct.lift b.π, inv := CategoryTheory.Limits.biproduct.desc b.ι, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.biproduct.uniqueUpToIso_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).hom = CategoryTheory.Limits.biproduct.lift b.π

@[simp]

theorem CategoryTheory.Limits.biproduct.uniqueUpToIso_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [CategoryTheory.Limits.HasBiproduct f] {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit) : (CategoryTheory.Limits.biproduct.uniqueUpToIso f hb).inv = CategoryTheory.Limits.biproduct.desc b.ι

@[instance 100]

instance CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.HasZeroObject C

A category with finite biproducts has a zero object.

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.limitBiconeOfUnique {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : CategoryTheory.Limits.LimitBicone f

The limit bicone for the biproduct over an index type with exactly one term.

Equations

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

@[simp]

theorem CategoryTheory.Limits.limitBiconeOfUnique_bicone_pt {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.pt = f default

@[simp]

theorem CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isColimit {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isColimit = (CategoryTheory.Limits.colimitCoconeOfUnique f).isColimit

@[simp]

theorem CategoryTheory.Limits.limitBiconeOfUnique_bicone_ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) (j : J) : (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.ι j = CategoryTheory.eqToHom ⋯

@[simp]

theorem CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isLimit {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit.isLimit = (CategoryTheory.Limits.limitConeOfUnique f).isLimit

@[simp]

theorem CategoryTheory.Limits.limitBiconeOfUnique_bicone_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) (j : J) : (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.π j = CategoryTheory.eqToHom ⋯

@[instance 100]

instance CategoryTheory.Limits.hasBiproduct_unique {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Subsingleton J] [Nonempty J] (f : J → C) : CategoryTheory.Limits.HasBiproduct f

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.biproductUniqueIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : ⨁ f ≅ f default

A biproduct over an index type with exactly one term is just the object over that term.

Equations

• CategoryTheory.Limits.biproductUniqueIso f = (CategoryTheory.Limits.biproduct.uniqueUpToIso f (CategoryTheory.Limits.limitBiconeOfUnique f).isBilimit).symm

@[simp]

theorem CategoryTheory.Limits.biproductUniqueIso_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.biproductUniqueIso f).hom = CategoryTheory.Limits.biproduct.desc (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.ι

@[simp]

theorem CategoryTheory.Limits.biproductUniqueIso_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [Unique J] (f : J → C) : (CategoryTheory.Limits.biproductUniqueIso f).inv = CategoryTheory.Limits.biproduct.lift (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.π

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

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 : CategoryTheory.CategoryStruct.comp self.inl self.fst = CategoryTheory.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 : CategoryTheory.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 : CategoryTheory.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 : CategoryTheory.CategoryStruct.comp self.inr self.snd = CategoryTheory.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

Instances For

• CategoryTheory.Limits.BinaryBicone.category

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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 : CategoryTheory.CategoryStruct.comp self.hom B.fst = A.fst

  The triangle consisting of the two natural transformations and hom commutes

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

  The triangle consisting of the two natural transformations and hom commutes

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

  The triangle consisting of the two natural transformations and hom commutes

• winr : CategoryTheory.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 u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B) {Z : C} (h : Q ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp B.snd h) = CategoryTheory.CategoryStruct.comp A.snd h

@[simp]

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

@[simp]

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

@[simp]

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

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

The category of binary bicones on a given diagram.

Equations

• CategoryTheory.Limits.BinaryBicone.category = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.BinaryBicones.functoriality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [CategoryTheory.Category.{uD', uD} D] [CategoryTheory.Limits.HasZeroMorphisms D] (P Q : C) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] : CategoryTheory.Functor (CategoryTheory.Limits.BinaryBicone P Q) (CategoryTheory.Limits.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.

Equations

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

Instances For

• CategoryTheory.Limits.BinaryBicones.functoriality_faithful
• CategoryTheory.Limits.BinaryBicones.functoriality_full

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Extract the cone from a binary bicone.

Equations

• c.toCone = CategoryTheory.Limits.BinaryFan.mk c.fst c.snd

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Extract the cocone from a binary bicone.

Equations

• c.toCocone = CategoryTheory.Limits.BinaryCofan.mk c.inl c.inr

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Convert a BinaryBicone into a Bicone over a pair.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

A shorthand for toBiconeFunctor.obj

Equations

• b.toBicone = CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b

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

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

Equations

• b.toBiconeIsLimit = CategoryTheory.Limits.IsLimit.equivIsoLimit (CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl b.toBicone.toCone.pt) ⋯)

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

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

Equations

• b.toBiconeIsColimit = CategoryTheory.Limits.IsColimit.equivIsoColimit (CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl b.toBicone.toCocone.pt) ⋯)

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

A shorthand for toBinaryBiconeFunctor.obj

Equations

• b.toBinaryBicone = CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b

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

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

Equations

• b.toBinaryBiconeIsLimit = CategoryTheory.Limits.IsLimit.equivIsoLimit (CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl b.toBinaryBicone.toCone.pt) ⋯)

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

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

Equations

• b.toBinaryBiconeIsColimit = CategoryTheory.Limits.IsColimit.equivIsoColimit (CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl b.toBinaryBicone.toCocone.pt) ⋯)

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

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

• isLimit : CategoryTheory.Limits.IsLimit b.toCone

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

• isColimit : CategoryTheory.Limits.IsColimit b.toCocone

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

def CategoryTheory.Limits.BinaryBicone.toBiconeIsBilimit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.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.

Equations

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

def CategoryTheory.Limits.Bicone.toBinaryBiconeIsBilimit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.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.

Equations

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

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

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

• bicone : CategoryTheory.Limits.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 u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.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 (CategoryTheory.Limits.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 u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} (d : CategoryTheory.Limits.BinaryBiproductData P Q) : CategoryTheory.Limits.HasBinaryBiproduct P Q

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

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

Equations

• CategoryTheory.Limits.getBinaryBiproductData P Q = Classical.choice ⋯

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

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

Equations

• CategoryTheory.Limits.BinaryBiproduct.bicone P Q = (CategoryTheory.Limits.getBinaryBiproductData P Q).bicone

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

BinaryBiproduct.bicone P Q is a limit bicone.

Equations

• CategoryTheory.Limits.BinaryBiproduct.isBilimit P Q = (CategoryTheory.Limits.getBinaryBiproductData P Q).isBilimit

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

BinaryBiproduct.bicone P Q is a limit cone.

Equations

• CategoryTheory.Limits.BinaryBiproduct.isLimit P Q = (CategoryTheory.Limits.getBinaryBiproductData P Q).isBilimit.isLimit

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

BinaryBiproduct.bicone P Q is a colimit cocone.

Equations

• CategoryTheory.Limits.BinaryBiproduct.isColimit P Q = (CategoryTheory.Limits.getBinaryBiproductData P Q).isBilimit.isColimit

class CategoryTheory.Limits.HasBinaryBiproducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.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), CategoryTheory.Limits.HasBinaryBiproduct P Q

theorem CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Limits.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 u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C} [CategoryTheory.Limits.HasBinaryBiproduct P Q] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair P Q)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.biprodIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.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.

Equations

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

@[reducible, inline]

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

An arbitrary choice of biproduct of a pair of objects.

Equations

• (X ⊞ Y) = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).pt

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

An arbitrary choice of biproduct of a pair of objects.

Equations

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

@[reducible, inline]

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

The projection onto the first summand of a binary biproduct.

Equations

• CategoryTheory.Limits.biprod.fst = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).fst

Instances For

• CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd
• CategoryTheory.Limits.biprod.fst_epi
• CategoryTheory.Limits.instHasKernelFst

@[reducible, inline]

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

The projection onto the second summand of a binary biproduct.

Equations

• CategoryTheory.Limits.biprod.snd = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).snd

Instances For

• CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd
• CategoryTheory.Limits.biprod.snd_epi
• CategoryTheory.Limits.instHasKernelSnd

@[reducible, inline]

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

The inclusion into the first summand of a binary biproduct.

Equations

• CategoryTheory.Limits.biprod.inl = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inl

Instances For

• CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd
• CategoryTheory.Limits.biprod.inl_mono
• CategoryTheory.Limits.instHasCokernelInl

@[reducible, inline]

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

The inclusion into the second summand of a binary biproduct.

Equations

• CategoryTheory.Limits.biprod.inr = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inr

Instances For

• CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd
• CategoryTheory.Limits.biprod.inr_mono
• CategoryTheory.Limits.instHasCokernelInr

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[reducible, inline]

abbrev CategoryTheory.Limits.biprod.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y : C} [CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.biprod.lift f g = (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y).lift (CategoryTheory.Limits.BinaryFan.mk f g)

Instances For

• CategoryTheory.Limits.biprod.mono_lift_of_mono_left
• CategoryTheory.Limits.biprod.mono_lift_of_mono_right

@[reducible, inline]

abbrev CategoryTheory.Limits.biprod.desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y : C} [CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.biprod.desc f g = (CategoryTheory.Limits.BinaryBiproduct.isColimit X Y).desc (CategoryTheory.Limits.BinaryCofan.mk f g)

Instances For

• CategoryTheory.Limits.biprod.epi_desc_of_epi_left
• CategoryTheory.Limits.biprod.epi_desc_of_epi_right

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Limits.biprod.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.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.

Equations

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

Instances For

• CategoryTheory.Limits.biprod.map_epi
• CategoryTheory.Limits.biprod.map_mono

@[reducible, inline]

abbrev CategoryTheory.Limits.biprod.map' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.biprod.map' f g = (CategoryTheory.Limits.BinaryBiproduct.isColimit W X).map (CategoryTheory.Limits.BinaryBiproduct.bicone Y Z).toCocone (CategoryTheory.Limits.mapPair f g)

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

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

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

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

Equations

• CategoryTheory.Limits.biprod.isoProd X Y = (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.pair X Y))

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.biprod.mapIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {W X Y Z : C} [CategoryTheory.Limits.HasBinaryBiproduct W X] [CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.biprod.mapIso f g = { hom := CategoryTheory.Limits.biprod.map f.hom g.hom, inv := CategoryTheory.Limits.biprod.map f.inv g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

Auxiliary lemma for biprod.uniqueUpToIso.

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

Auxiliary lemma for biprod.uniqueUpToIso.

def CategoryTheory.Limits.biprod.uniqueUpToIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.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.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• c.fstKernelFork = CategoryTheory.Limits.KernelFork.ofι c.inr ⋯

@[simp]

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

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

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

Equations

• c.sndKernelFork = CategoryTheory.Limits.KernelFork.ofι c.inl ⋯

@[simp]

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

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

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

Equations

• c.inlCokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ c.snd ⋯

@[simp]

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

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

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

Equations

• c.inrCokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ c.fst ⋯

@[simp]

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• CategoryTheory.Limits.biprod.fstKernelFork X Y = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).fstKernelFork

@[simp]

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

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

The fork biprod.fstKernelFork is indeed a limit.

Equations

• CategoryTheory.Limits.biprod.isKernelFstKernelFork X Y = CategoryTheory.Limits.BinaryBicone.isLimitFstKernelFork (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)

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

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

Equations

• CategoryTheory.Limits.biprod.sndKernelFork X Y = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).sndKernelFork

@[simp]

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

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

The fork biprod.sndKernelFork is indeed a limit.

Equations

• CategoryTheory.Limits.biprod.isKernelSndKernelFork X Y = CategoryTheory.Limits.BinaryBicone.isLimitSndKernelFork (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)

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

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

Equations

• CategoryTheory.Limits.biprod.inlCokernelCofork X Y = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inlCokernelCofork

@[simp]

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

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

The cofork biprod.inlCokernelFork is indeed a colimit.

Equations

• CategoryTheory.Limits.biprod.isCokernelInlCokernelFork X Y = CategoryTheory.Limits.BinaryBicone.isColimitInlCokernelCofork (CategoryTheory.Limits.BinaryBiproduct.isColimit X Y)

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

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

Equations

• CategoryTheory.Limits.biprod.inrCokernelCofork X Y = (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inrCokernelCofork

@[simp]

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

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

The cofork biprod.inrCokernelFork is indeed a colimit.

Equations

• CategoryTheory.Limits.biprod.isCokernelInrCokernelFork X Y = CategoryTheory.Limits.BinaryBicone.isColimitInrCokernelCofork (CategoryTheory.Limits.BinaryBiproduct.isColimit X Y)

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

Equations

• ⋯ = ⋯

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.isoBiprodZero hY = { hom := CategoryTheory.Limits.biprod.inl, inv := CategoryTheory.Limits.biprod.fst, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.isoZeroBiprod hY = { hom := CategoryTheory.Limits.biprod.inr, inv := CategoryTheory.Limits.biprod.snd, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

The braiding isomorphism which swaps a binary biproduct.

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.biprod.braiding' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.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.

Equations

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

@[simp]

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

@[simp]

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

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

theorem CategoryTheory.Limits.biprod.braid_natural {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.Limits.biprod.braiding Y W).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X Z).hom (CategoryTheory.Limits.biprod.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 u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⊞ Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding Y W).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map g f) h)

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

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

@[simp]

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

@[simp]

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

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

The braiding isomorphism is symmetric.

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

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

The associator isomorphism which associates a binary biproduct.

Equations

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Limits.biprod.associator_natural {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h) (CategoryTheory.Limits.biprod.associator X Y Z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).hom (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.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 u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.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✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator X Y Z).hom h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h)) h✝)

theorem CategoryTheory.Limits.biprod.associator_inv_natural {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h)) (CategoryTheory.Limits.biprod.associator X Y Z).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).inv (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.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 u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.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✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator X Y Z).inv h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h) h✝)

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

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

Equations

• CategoryTheory.Indecomposable X = (¬CategoryTheory.Limits.IsZero X ∧ ∀ (Y Z : C), (X ≅ Y ⊞ Z) → CategoryTheory.Limits.IsZero Y ∨ CategoryTheory.Limits.IsZero Z)

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

If

(f 0)
(0 g)

is invertible, then f is invertible.

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

If

(f 0)
(0 g)

is invertible, then g is invertible.