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 leanprover-community/mathlib#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} (F : JC) :
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 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
theorem CategoryTheory.Limits.Bicone.ι_π {J : Type w} {C : Type uC} {F : JC} (self : ) (j : J) (j' : J) :
CategoryTheory.CategoryStruct.comp (self j) (self j') = if h : j = j' then 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.
@[simp]
theorem CategoryTheory.Limits.bicone_ι_π_self_assoc {J : Type w} {C : Type uC} {F : JC} (B : ) (j : J) {Z : C} (h : F j Z) :
@[simp]
theorem CategoryTheory.Limits.bicone_ι_π_self {J : Type w} {C : Type uC} {F : JC} (B : ) (j : J) :
@[simp]
theorem CategoryTheory.Limits.bicone_ι_π_ne_assoc {J : Type w} {C : Type uC} {F : JC} (B : ) {j : J} {j' : J} (h : j j') {Z : C} (h : F j' Z) :
@[simp]
theorem CategoryTheory.Limits.bicone_ι_π_ne {J : Type w} {C : Type uC} {F : JC} (B : ) {j : J} {j' : J} (h : j j') :
structure CategoryTheory.Limits.BiconeMorphism {J : Type w} {C : Type uC} {F : JC} (A : ) (B : ) :
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

Instances For
@[simp]
theorem CategoryTheory.Limits.BiconeMorphism. {J : Type w} {C : Type uC} {F : JC} {A : } {B : } (self : ) (j : J) :
CategoryTheory.CategoryStruct.comp self.hom (B j) = A j

The triangle consisting of the two natural transformations and hom commutes

@[simp]
theorem CategoryTheory.Limits.BiconeMorphism. {J : Type w} {C : Type uC} {F : JC} {A : } {B : } (self : ) (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} {F : JC} {A : } {B : } (self : ) (j : J) {Z : C} (h : B.pt Z) :
@[simp]
theorem CategoryTheory.Limits.BiconeMorphism.wπ_assoc {J : Type w} {C : Type uC} {F : JC} {A : } {B : } (self : ) (j : J) {Z : C} (h : F j Z) :
@[simp]
theorem CategoryTheory.Limits.Bicone.category_id_hom {J : Type w} {C : Type uC} {F : JC} (B : ) :
@[simp]
theorem CategoryTheory.Limits.Bicone.category_comp_hom {J : Type w} {C : Type uC} {F : JC} :
∀ {X Y Z : } (f : X Y) (g : Y Z), .hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
instance CategoryTheory.Limits.Bicone.category {J : Type w} {C : Type uC} {F : JC} :

The category of bicones on a given diagram.

Equations
• CategoryTheory.Limits.Bicone.category =
theorem CategoryTheory.Limits.BiconeMorphism.ext_iff {J : Type w} {C : Type uC} {F : JC} {c : } {c' : } {f : c c'} {g : c c'} :
f = g f.hom = g.hom
theorem CategoryTheory.Limits.BiconeMorphism.ext {J : Type w} {C : Type uC} {F : JC} {c : } {c' : } (f : c c') (g : c c') (w : f.hom = g.hom) :
f = g
@[simp]
theorem CategoryTheory.Limits.Bicones.ext_hom_hom {J : Type w} {C : Type uC} {F : JC} {c : } {c' : } (φ : c.pt c'.pt) (wι : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c j) φ.hom = c' j) _auto✝) (wπ : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c' j) = c j) _auto✝) :
.hom.hom = φ.hom
@[simp]
theorem CategoryTheory.Limits.Bicones.ext_inv_hom {J : Type w} {C : Type uC} {F : JC} {c : } {c' : } (φ : c.pt c'.pt) (wι : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c j) φ.hom = c' j) _auto✝) (wπ : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c' j) = c j) _auto✝) :
.inv.hom = φ.inv
def CategoryTheory.Limits.Bicones.ext {J : Type w} {C : Type uC} {F : JC} {c : } {c' : } (φ : c.pt c'.pt) (wι : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c j) φ.hom = c' j) _auto✝) (wπ : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c' j) = c j) _auto✝) :
c c'

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

Equations
• = { hom := { hom := φ.hom, := , := }, inv := { hom := φ.inv, := , := }, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Limits.Bicones.functoriality_obj_pt {J : Type w} {C : Type uC} {D : Type uD} (F : JC) (G : ) [G.PreservesZeroMorphisms] (A : ) :
( A).pt = G.obj A.pt
@[simp]
theorem CategoryTheory.Limits.Bicones.functoriality_map_hom {J : Type w} {C : Type uC} {D : Type uD} (F : JC) (G : ) [G.PreservesZeroMorphisms] :
∀ {X Y : } (f : X Y), ( f).hom = G.map f.hom
@[simp]
theorem CategoryTheory.Limits.Bicones.functoriality_obj_π {J : Type w} {C : Type uC} {D : Type uD} (F : JC) (G : ) [G.PreservesZeroMorphisms] (A : ) (j : J) :
( A) j = G.map (A j)
@[simp]
theorem CategoryTheory.Limits.Bicones.functoriality_obj_ι {J : Type w} {C : Type uC} {D : Type uD} (F : JC) (G : ) [G.PreservesZeroMorphisms] (A : ) (j : J) :
( A) j = G.map (A j)
def CategoryTheory.Limits.Bicones.functoriality {J : Type w} {C : Type uC} {D : Type uD} (F : JC) (G : ) [G.PreservesZeroMorphisms] :

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
instance CategoryTheory.Limits.Bicones.functoriality_full {J : Type w} {C : Type uC} {D : Type uD} {F : JC} (G : ) [G.PreservesZeroMorphisms] [G.Full] [G.Faithful] :
.Full
Equations
• =
instance CategoryTheory.Limits.Bicones.functoriality_faithful {J : Type w} {C : Type uC} {D : Type uD} {F : JC} (G : ) [G.PreservesZeroMorphisms] [G.Faithful] :
.Faithful
Equations
• =
def CategoryTheory.Limits.Bicone.toConeFunctor {J : Type w} {C : Type uC} {F : JC} :

Extract the cone from a bicone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.Bicone.toCone {J : Type w} {C : Type uC} {F : JC} (B : ) :

A shorthand for toConeFunctor.obj

Equations
• B.toCone = CategoryTheory.Limits.Bicone.toConeFunctor.obj B
Instances For
@[simp]
theorem CategoryTheory.Limits.Bicone.toCone_pt {J : Type w} {C : Type uC} {F : JC} (B : ) :
B.toCone.pt = B.pt
@[simp]
theorem CategoryTheory.Limits.Bicone.toCone_π_app {J : Type w} {C : Type uC} {F : JC} (B : ) (j : ) :
B.toCone.app j = B j.as
theorem CategoryTheory.Limits.Bicone.toCone_π_app_mk {J : Type w} {C : Type uC} {F : JC} (B : ) (j : J) :
B.toCone.app { as := j } = B j
@[simp]
theorem CategoryTheory.Limits.Bicone.toCone_proj {J : Type w} {C : Type uC} {F : JC} (B : ) (j : J) :
def CategoryTheory.Limits.Bicone.toCoconeFunctor {J : Type w} {C : Type uC} {F : JC} :

Extract the cocone from a bicone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.Bicone.toCocone {J : Type w} {C : Type uC} {F : JC} (B : ) :

A shorthand for toCoconeFunctor.obj

Equations
• B.toCocone = CategoryTheory.Limits.Bicone.toCoconeFunctor.obj B
Instances For
@[simp]
theorem CategoryTheory.Limits.Bicone.toCocone_pt {J : Type w} {C : Type uC} {F : JC} (B : ) :
B.toCocone.pt = B.pt
@[simp]
theorem CategoryTheory.Limits.Bicone.toCocone_ι_app {J : Type w} {C : Type uC} {F : JC} (B : ) (j : ) :
B.toCocone.app j = B j.as
@[simp]
theorem CategoryTheory.Limits.Bicone.toCocone_inj {J : Type w} {C : Type uC} {F : JC} (B : ) (j : J) :
theorem CategoryTheory.Limits.Bicone.toCocone_ι_app_mk {J : Type w} {C : Type uC} {F : JC} (B : ) (j : J) :
B.toCocone.app { as := j } = B j
@[simp]
theorem CategoryTheory.Limits.Bicone.ofLimitCone_ι {J : Type w} {C : Type uC} {f : JC} (ht : ) (j : J) :
= ht.lift (CategoryTheory.Limits.Fan.mk (f j) fun (j' : J) => if h : j = j' then else 0)
@[simp]
theorem CategoryTheory.Limits.Bicone.ofLimitCone_π {J : Type w} {C : Type uC} {f : JC} (ht : ) (j : J) :
= t.app { as := j }
@[simp]
theorem CategoryTheory.Limits.Bicone.ofLimitCone_pt {J : Type w} {C : Type uC} {f : JC} (ht : ) :
= t.pt
def CategoryTheory.Limits.Bicone.ofLimitCone {J : Type w} {C : Type uC} {f : JC} (ht : ) :

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.
Instances For
theorem CategoryTheory.Limits.Bicone.ι_of_isLimit {J : Type w} {C : Type uC} {f : JC} {t : } (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 else 0)
@[simp]
theorem CategoryTheory.Limits.Bicone.ofColimitCocone_ι {J : Type w} {C : Type uC} {f : JC} (ht : ) (j : J) :
= t.app { as := j }
@[simp]
theorem CategoryTheory.Limits.Bicone.ofColimitCocone_pt {J : Type w} {C : Type uC} {f : JC} (ht : ) :
= t.pt
@[simp]
theorem CategoryTheory.Limits.Bicone.ofColimitCocone_π {J : Type w} {C : Type uC} {f : JC} (ht : ) (j : J) :
= ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun (j' : J) => if h : j' = j then else 0)
def CategoryTheory.Limits.Bicone.ofColimitCocone {J : Type w} {C : Type uC} {f : JC} (ht : ) :

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.
Instances For
theorem CategoryTheory.Limits.Bicone.π_of_isColimit {J : Type w} {C : Type uC} {f : JC} {t : } (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 else 0)
structure CategoryTheory.Limits.Bicone.IsBilimit {J : Type w} {C : Type uC} {F : JC} (B : ) :
Type (max (max uC uC') w)

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

Instances For
theorem CategoryTheory.Limits.Bicone.IsBilimit.ext_iff {J : Type w} {C : Type uC} :
∀ {inst : } {inst_1 : } {F : JC} {B : } {x y : B.IsBilimit}, x = y x.isLimit = y.isLimit x.isColimit = y.isColimit
theorem CategoryTheory.Limits.Bicone.IsBilimit.ext {J : Type w} {C : Type uC} :
∀ {inst : } {inst_1 : } {F : JC} {B : } {x y : B.IsBilimit}, x.isLimit = y.isLimitx.isColimit = y.isColimitx = y
instance CategoryTheory.Limits.Bicone.subsingleton_isBilimit {J : Type w} {C : Type uC} {f : JC} {c : } :
Subsingleton c.IsBilimit
Equations
• =
@[simp]
theorem CategoryTheory.Limits.Bicone.whisker_pt {J : Type w} {C : Type uC} {K : Type w'} {f : JC} (c : ) (g : K J) :
(c.whisker g).pt = c.pt
@[simp]
theorem CategoryTheory.Limits.Bicone.whisker_π {J : Type w} {C : Type uC} {K : Type w'} {f : JC} (c : ) (g : K J) (k : K) :
(c.whisker g) k = c (g k)
@[simp]
theorem CategoryTheory.Limits.Bicone.whisker_ι {J : Type w} {C : Type uC} {K : Type w'} {f : JC} (c : ) (g : K J) (k : K) :
(c.whisker g) k = c (g k)
def CategoryTheory.Limits.Bicone.whisker {J : Type w} {C : Type uC} {K : Type w'} {f : JC} (c : ) (g : K J) :

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), ι_π := }
Instances For
def CategoryTheory.Limits.Bicone.whiskerToCone {J : Type w} {C : Type uC} {K : Type w'} {f : JC} (c : ) (g : K J) :
(c.whisker g).toCone (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
Instances For
def CategoryTheory.Limits.Bicone.whiskerToCocone {J : Type w} {C : Type uC} {K : Type w'} {f : JC} (c : ) (g : K J) :
(c.whisker g).toCocone (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
Instances For
def CategoryTheory.Limits.Bicone.whiskerIsBilimitIff {J : Type w} {C : Type uC} {K : Type w'} {f : JC} (c : ) (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.
Instances For
structure CategoryTheory.Limits.LimitBicone {J : Type w} {C : Type uC} (F : JC) :
Type (max (max uC uC') w)

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

• bicone :

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.

Instances For
class CategoryTheory.Limits.HasBiproduct {J : Type w} {C : Type uC} (F : JC) :

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

• mk' :: (
• exists_biproduct :

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

• )
Instances
theorem CategoryTheory.Limits.HasBiproduct.exists_biproduct {J : Type w} {C : Type uC} {F : JC} [self : ] :

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

theorem CategoryTheory.Limits.HasBiproduct.mk {J : Type w} {C : Type uC} {F : JC} :
def CategoryTheory.Limits.getBiproductData {J : Type w} {C : Type uC} (F : JC) :

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

Equations
Instances For
def CategoryTheory.Limits.biproduct.bicone {J : Type w} {C : Type uC} (F : JC) :

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

Equations
Instances For
def CategoryTheory.Limits.biproduct.isBilimit {J : Type w} {C : Type uC} (F : JC) :
.IsBilimit

biproduct.bicone F is a bilimit bicone.

Equations
Instances For
def CategoryTheory.Limits.biproduct.isLimit {J : Type w} {C : Type uC} (F : JC) :

biproduct.bicone F is a limit cone.

Equations
• = .isBilimit.isLimit
Instances For
def CategoryTheory.Limits.biproduct.isColimit {J : Type w} {C : Type uC} (F : JC) :

biproduct.bicone F is a colimit cocone.

Equations
• = .isBilimit.isColimit
Instances For
@[instance 100]
instance CategoryTheory.Limits.hasProduct_of_hasBiproduct {J : Type w} {C : Type uC} {F : JC} :
Equations
• =
@[instance 100]
instance CategoryTheory.Limits.hasCoproduct_of_hasBiproduct {J : Type w} {C : Type uC} {F : JC} :
Equations
• =

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 : JC),
Instances
theorem CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct {J : Type w} {C : Type uC} [self : ] (F : JC) :

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

• out : ∀ (n : ),

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

Instances

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) {K : Type w'} (e : J K) :
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
def CategoryTheory.Limits.biproductIso {J : Type w} {C : Type uC} (F : JC) :

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.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.biproduct {J : Type w} {C : Type u} (f : JC) :
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
Instances For

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
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.biproduct.π {J : Type w} {C : Type u} (f : JC) (b : J) :
f f b

The projection onto a summand of a biproduct.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.bicone_π {J : Type w} {C : Type u} (f : JC) (b : J) :
@[reducible, inline]
abbrev CategoryTheory.Limits.biproduct.ι {J : Type w} {C : Type u} (f : JC) (b : J) :
f b f

The inclusion into a summand of a biproduct.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.bicone_ι {J : Type w} {C : Type u} (f : JC) (b : J) :
theorem CategoryTheory.Limits.biproduct.ι_π_assoc {J : Type w} {C : Type u} [] (f : JC) (j : J) (j' : J) {Z : C} (h : f j' Z) :
= CategoryTheory.CategoryStruct.comp (if h : j = j' then else 0) h
theorem CategoryTheory.Limits.biproduct.ι_π {J : Type w} {C : Type u} [] (f : JC) (j : J) (j' : J) :
= if h : j = j' then 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.ι_π_self_assoc {J : Type w} {C : Type u} (f : JC) (j : J) {Z : C} (h : f j Z) :
theorem CategoryTheory.Limits.biproduct.ι_π_self {J : Type w} {C : Type u} (f : JC) (j : J) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_π_ne_assoc {J : Type w} {C : Type u} (f : JC) {j : J} {j' : J} (h : j j') {Z : C} (h : f j' Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_π_ne {J : Type w} {C : Type u} (f : JC) {j : J} {j' : J} (h : j j') :
@[simp]
theorem CategoryTheory.Limits.biproduct.eqToHom_comp_ι_assoc {J : Type w} {C : Type u} (f : JC) {j : J} {j' : J} (w : j = j') {Z : C} (h : f Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.eqToHom_comp_ι {J : Type w} {C : Type u} (f : JC) {j : J} {j' : J} (w : j = j') :
@[simp]
theorem CategoryTheory.Limits.biproduct.π_comp_eqToHom_assoc {J : Type w} {C : Type u} (f : JC) {j : J} {j' : J} (w : j = j') {Z : C} (h : f j' Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.π_comp_eqToHom {J : Type w} {C : Type u} (f : JC) {j : J} {j' : J} (w : j = j') :
@[reducible, inline]
abbrev CategoryTheory.Limits.biproduct.lift {J : Type w} {C : Type u} {f : JC} {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
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.biproduct.desc {J : Type w} {C : Type u} {f : JC} {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
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.lift_π_assoc {J : Type w} {C : Type u} {f : JC} {P : C} (p : (b : J) → P f b) (j : J) {Z : C} (h : f j Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.lift_π {J : Type w} {C : Type u} {f : JC} {P : C} (p : (b : J) → P f b) (j : J) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_desc_assoc {J : Type w} {C : Type u} {f : JC} {P : C} (p : (b : J) → f b P) (j : J) {Z : C} (h : P Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_desc {J : Type w} {C : Type u} {f : JC} {P : C} (p : (b : J) → f b P) (j : J) :
@[reducible, inline]
abbrev CategoryTheory.Limits.biproduct.map {J : Type w} {C : Type u} {f : JC} {g : JC} (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
@[reducible, inline]
abbrev CategoryTheory.Limits.biproduct.map' {J : Type w} {C : Type u} {f : JC} {g : JC} (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.
Instances For
theorem CategoryTheory.Limits.biproduct.hom_ext_iff {J : Type w} {C : Type u} {f : JC} {Z : C} {g : Z f} {h : Z f} :
g = h ∀ (j : J),
theorem CategoryTheory.Limits.biproduct.hom_ext {J : Type w} {C : Type u} {f : JC} {Z : C} (g : Z f) (h : Z f) (w : ) :
g = h
theorem CategoryTheory.Limits.biproduct.hom_ext'_iff {J : Type w} {C : Type u} {f : JC} {Z : C} {g : f Z} {h : f Z} :
g = h ∀ (j : J),
theorem CategoryTheory.Limits.biproduct.hom_ext' {J : Type w} {C : Type u} {f : JC} {Z : C} (g : f Z) (h : f Z) (w : ) :
g = h
def CategoryTheory.Limits.biproduct.isoProduct {J : Type w} {C : Type u} (f : JC) :

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

Equations
• = .conePointUniqueUpToIso
Instances For
@[simp]
@[simp]
def CategoryTheory.Limits.biproduct.isoCoproduct {J : Type w} {C : Type u} (f : JC) :
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.
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.isoCoproduct_inv {J : Type w} {C : Type u} {f : JC} :
@[simp]
theorem CategoryTheory.Limits.biproduct.isoCoproduct_hom {J : Type w} {C : Type u} {f : JC} :
theorem CategoryTheory.Limits.biproduct.map_eq_map' {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (b : J) → f b g b) :
@[simp]
theorem CategoryTheory.Limits.biproduct.map_π_assoc {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (j : J) → f j g j) (j : J) {Z : C} (h : g j Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.map_π {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (j : J) → f j g j) (j : J) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_map_assoc {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (j : J) → f j g j) (j : J) {Z : C} (h : g Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_map {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (j : J) → f j g j) (j : J) :
@[simp]
theorem CategoryTheory.Limits.biproduct.map_desc_assoc {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (j : J) → f j g j) {P : C} (k : (j : J) → g j P) {Z : C} (h : P Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.map_desc {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (j : J) → f j g j) {P : C} (k : (j : J) → g j P) :
@[simp]
theorem CategoryTheory.Limits.biproduct.lift_map_assoc {J : Type w} {C : Type u} {f : JC} {g : JC} {P : C} (k : (j : J) → P f j) (p : (j : J) → f j g j) {Z : C} (h : g Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.lift_map {J : Type w} {C : Type u} {f : JC} {g : JC} {P : C} (k : (j : J) → P f j) (p : (j : J) → f j g j) :
@[simp]
theorem CategoryTheory.Limits.biproduct.mapIso_hom {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (b : J) → f b g b) :
= CategoryTheory.Limits.biproduct.map fun (b : J) => (p b).hom
@[simp]
theorem CategoryTheory.Limits.biproduct.mapIso_inv {J : Type w} {C : Type u} {f : JC} {g : JC} (p : (b : J) → f b g b) :
= CategoryTheory.Limits.biproduct.map fun (b : J) => (p b).inv
def CategoryTheory.Limits.biproduct.mapIso {J : Type w} {C : Type u} {f : JC} {g : JC} (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.
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.whiskerEquiv_inv {J : Type w} {K : Type u_1} {C : Type u} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) :
@[simp]
theorem CategoryTheory.Limits.biproduct.whiskerEquiv_hom {J : Type w} {K : Type u_1} {C : Type u} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) :
def CategoryTheory.Limits.biproduct.whiskerEquiv {J : Type w} {K : Type u_1} {C : Type u} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) :
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.
Instances For
theorem CategoryTheory.Limits.biproduct.whiskerEquiv_hom_eq_lift {J : Type w} {K : Type u_1} {C : Type u} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) :
theorem CategoryTheory.Limits.biproduct.whiskerEquiv_inv_eq_lift {J : Type w} {K : Type u_1} {C : Type u} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) :
instance CategoryTheory.Limits.instHasBiproductSigmaFstSndOfBiproduct {C : Type u} {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), ] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => g i] :
CategoryTheory.Limits.HasBiproduct fun (p : (i : ι) × f i) => g p.fst p.snd
Equations
• =
@[simp]
theorem CategoryTheory.Limits.biproductBiproductIso_inv {C : Type u} {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), ] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => g i] :
= 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} {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), ] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => g i] :
= 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)
def CategoryTheory.Limits.biproductBiproductIso {C : Type u} {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (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.
Instances For
def CategoryTheory.Limits.biproduct.fromSubtype {J : Type w} {C : Type u} (f : JC) (p : JProp) :
f

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

Equations
Instances For
def CategoryTheory.Limits.biproduct.toSubtype {J : Type w} {C : Type u} (f : JC) (p : JProp) :
f

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.fromSubtype_π_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) [] (j : J) {Z : C} (h : f j Z) :
= CategoryTheory.CategoryStruct.comp (if h : p j then else 0) h
@[simp]
theorem CategoryTheory.Limits.biproduct.fromSubtype_π {J : Type w} {C : Type u} (f : JC) (p : JProp) [] (j : J) :
= if h : p j then else 0
theorem CategoryTheory.Limits.biproduct.fromSubtype_eq_lift {J : Type w} {C : Type u} (f : JC) (p : JProp) [] :
= CategoryTheory.Limits.biproduct.lift fun (j : J) => if h : p j then else 0
theorem CategoryTheory.Limits.biproduct.fromSubtype_π_subtype_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) {Z : C} (h : f j Z) :
theorem CategoryTheory.Limits.biproduct.fromSubtype_π_subtype {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) :
@[simp]
theorem CategoryTheory.Limits.biproduct.toSubtype_π_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) {Z : C} (h : Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.toSubtype_π {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_toSubtype_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) [] (j : J) {Z : C} (h : Z) :
= CategoryTheory.CategoryStruct.comp (if h : p j then else 0) h
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_toSubtype {J : Type w} {C : Type u} (f : JC) (p : JProp) [] (j : J) :
= if h : p j then else 0
theorem CategoryTheory.Limits.biproduct.toSubtype_eq_desc {J : Type w} {C : Type u} (f : JC) (p : JProp) [] :
= CategoryTheory.Limits.biproduct.desc fun (j : J) => if h : p j then else 0
theorem CategoryTheory.Limits.biproduct.ι_toSubtype_subtype_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) {Z : C} (h : Z) :
theorem CategoryTheory.Limits.biproduct.ι_toSubtype_subtype {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_fromSubtype_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) {Z : C} (h : f Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_fromSubtype {J : Type w} {C : Type u} (f : JC) (p : JProp) (j : ) :
@[simp]
theorem CategoryTheory.Limits.biproduct.fromSubtype_toSubtype_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) {Z : C} (h : Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.fromSubtype_toSubtype {J : Type w} {C : Type u} (f : JC) (p : JProp) :
@[simp]
theorem CategoryTheory.Limits.biproduct.toSubtype_fromSubtype_assoc {J : Type w} {C : Type u} (f : JC) (p : JProp) [] {Z : C} (h : f Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.toSubtype_fromSubtype {J : Type w} {C : Type u} (f : JC) (p : JProp) [] :
= CategoryTheory.Limits.biproduct.map fun (j : J) => if p j then else 0

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.
Instances For
instance CategoryTheory.Limits.instHasKernelπ {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.kernelBiproductπIso_hom {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
@[simp]
theorem CategoryTheory.Limits.kernelBiproductπIso_inv {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
=
def CategoryTheory.Limits.kernelBiproductπIso {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
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.
Instances For

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.
Instances For
instance CategoryTheory.Limits.instHasCokernelι {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.cokernelBiproductιIso_inv {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
@[simp]
theorem CategoryTheory.Limits.cokernelBiproductιIso_hom {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
def CategoryTheory.Limits.cokernelBiproductιIso {J : Type w} {C : Type u} (f : JC) (i : J) [CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun (j : J) => j i) f)] :
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.
Instances For
@[simp]
theorem CategoryTheory.Limits.kernelForkBiproductToSubtype_cone {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
@[simp]
theorem CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
.isLimit = CategoryTheory.Limits.KernelFork.IsLimit.ofι (fun {W : C} (g : W f) (x : ) => )

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.
Instances For
instance CategoryTheory.Limits.instHasKernelToSubtype {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
= (CategoryTheory.Limits.KernelFork.IsLimit.ofι (fun {W : C} (g : W f) (x : ) => ) ).lift
@[simp]
theorem CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
def CategoryTheory.Limits.kernelBiproductToSubtypeIso {C : Type u} {K : Type} [] (f : KC) (p : Set K) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
@[simp]
theorem CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
.isColimit = CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (fun {W : C} (g : f W) (x : ) => )

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.
Instances For
instance CategoryTheory.Limits.instHasCokernelFromSubtype {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
Equations
• =
@[simp]
@[simp]
theorem CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv {C : Type u} {K : Type} [] (f : KC) (p : Set K) :
= (CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ (fun {W : C} (g : f W) (x : ) => ) ).desc
def CategoryTheory.Limits.cokernelBiproductFromSubtypeIso {C : Type u} {K : Type} [] (f : KC) (p : Set K) :

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

Equations
Instances For
def CategoryTheory.Limits.biproduct.matrix {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) :
f g

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.matrix_π_assoc {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) (k : K) {Z : C} (h : g k Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.matrix_π {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) (k : K) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_matrix_assoc {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) (j : J) {Z : C} (h : g Z) :
@[simp]
theorem CategoryTheory.Limits.biproduct.ι_matrix {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) (j : J) :
def CategoryTheory.Limits.biproduct.components {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (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.
Instances For
@[simp]
theorem CategoryTheory.Limits.biproduct.matrix_components {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) (j : J) (k : K) :
@[simp]
theorem CategoryTheory.Limits.biproduct.components_matrix {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : f g) :
(CategoryTheory.Limits.biproduct.matrix fun (j : J) (k : K) => ) = m
@[simp]
theorem CategoryTheory.Limits.biproduct.matrixEquiv_symm_apply {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) :
CategoryTheory.Limits.biproduct.matrixEquiv.symm m =
@[simp]
theorem CategoryTheory.Limits.biproduct.matrixEquiv_apply {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} (m : f g) (j : J) (k : K) :
CategoryTheory.Limits.biproduct.matrixEquiv m j k =
def CategoryTheory.Limits.biproduct.matrixEquiv {J : Type} [] {K : Type} [] {C : Type u} {f : JC} {g : KC} :
( 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 := }
Instances For
instance CategoryTheory.Limits.biproduct.ι_mono {J : Type w} {C : Type u} (f : JC) (b : J) :
Equations
• =
instance CategoryTheory.Limits.biproduct.π_epi {J : Type w} {C : Type u} (f : JC) (b : J) :
Equations
• =
theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_hom {J : Type w} {C : Type u} (f : JC) {b : } (hb : b.IsBilimit) :
(hb.isLimit.conePointUniqueUpToIso ).hom =

Auxiliary lemma for biproduct.uniqueUpToIso.

theorem CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv {J : Type w} {C : Type u} (f : JC) {b : } (hb : b.IsBilimit) :
(hb.isLimit.conePointUniqueUpToIso ).inv =

Auxiliary lemma for biproduct.uniqueUpToIso.

@[simp]
theorem CategoryTheory.Limits.biproduct.uniqueUpToIso_inv {J : Type w} {C : Type u} (f : JC) {b : } (hb : b.IsBilimit) :
@[simp]
theorem CategoryTheory.Limits.biproduct.uniqueUpToIso_hom {J : Type w} {C : Type u} (f : JC) {b : } (hb : b.IsBilimit) :
def CategoryTheory.Limits.biproduct.uniqueUpToIso {J : Type w} {C : Type u} (f : JC) {b : } (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
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
@[instance 100]

A category with finite biproducts has a zero object.

Equations
• =
@[simp]
theorem CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isColimit {J : Type w} {C : Type u} [] (f : JC) :
.isBilimit.isColimit = .isColimit
@[simp]
theorem CategoryTheory.Limits.limitBiconeOfUnique_bicone_π {J : Type w} {C : Type u} [] (f : JC) (j : J) :
.bicone j =
@[simp]
theorem CategoryTheory.Limits.limitBiconeOfUnique_bicone_ι {J : Type w} {C : Type u} [] (f : JC) (j : J) :
.bicone j =
@[simp]
theorem CategoryTheory.Limits.limitBiconeOfUnique_isBilimit_isLimit {J : Type w} {C : Type u} [] (f : JC) :
.isBilimit.isLimit = .isLimit
@[simp]
theorem CategoryTheory.Limits.limitBiconeOfUnique_bicone_pt {J : Type w} {C : Type u} [] (f : JC) :
.bicone.pt = f default
def CategoryTheory.Limits.limitBiconeOfUnique {J : Type w} {C : Type u} [] (f : JC) :

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.
Instances For
@[instance 100]
instance CategoryTheory.Limits.hasBiproduct_unique {J : Type w} {C : Type u} [] (f : JC) :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.biproductUniqueIso_hom {J : Type w} {C : Type u} [] (f : JC) :
@[simp]
theorem CategoryTheory.Limits.biproductUniqueIso_inv {J : Type w} {C : Type u} [] (f : JC) :
def CategoryTheory.Limits.biproductUniqueIso {J : Type w} {C : Type u} [] (f : JC) :
f f default

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

Equations
Instances For
structure CategoryTheory.Limits.BinaryBicone {C : Type u} (P : C) (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 =

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 =

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
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inl_fst {C : Type u} {P : C} {Q : C} (self : ) :

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

@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inl_snd {C : Type u} {P : C} {Q : C} (self : ) :

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

@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inr_fst {C : Type u} {P : C} {Q : C} (self : ) :

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

@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inr_snd {C : Type u} {P : C} {Q : C} (self : ) :

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

@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inl_snd_assoc {C : Type u} {P : C} {Q : C} (self : ) {Z : C} (h : Q Z) :
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inr_fst_assoc {C : Type u} {P : C} {Q : C} (self : ) {Z : C} (h : P Z) :
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inr_snd_assoc {C : Type u} {P : C} {Q : C} (self : ) {Z : C} (h : Q Z) :
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.inl_fst_assoc {C : Type u} {P : C} {Q : C} (self : ) {Z : C} (h : P Z) :
structure CategoryTheory.Limits.BinaryBiconeMorphism {C : Type u} {P : C} {Q : C} (A : ) (B : ) :

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.

Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.wfst {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) :

The triangle consisting of the two natural transformations and hom commutes

@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.wsnd {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) :

The triangle consisting of the two natural transformations and hom commutes

@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.winl {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) :

The triangle consisting of the two natural transformations and hom commutes

@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.winr {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) :

The triangle consisting of the two natural transformations and hom commutes

@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.wsnd_assoc {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) {Z : C} (h : Q Z) :
@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.wfst_assoc {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) {Z : C} (h : P Z) :
@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.winl_assoc {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) {Z : C} (h : B.pt Z) :
@[simp]
theorem CategoryTheory.Limits.BinaryBiconeMorphism.winr_assoc {C : Type u} {P : C} {Q : C} {A : } {B : } (self : ) {Z : C} (h : B.pt Z) :
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.category_id_hom {C : Type u} {P : C} {Q : C} (B : ) :
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.category_comp_hom {C : Type u} {P : C} {Q : C} :
∀ {X Y Z : } (f : X Y) (g : Y Z), .hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
instance CategoryTheory.Limits.BinaryBicone.category {C : Type u} {P : C} {Q : C} :

The category of binary bicones on a given diagram.

Equations
• CategoryTheory.Limits.BinaryBicone.category =
theorem CategoryTheory.Limits.BinaryBiconeMorphism.ext_iff {C : Type u} {P : C} {Q : C} {c : } {c' : } {f : c c'} {g : c c'} :
f = g f.hom = g.hom
theorem CategoryTheory.Limits.BinaryBiconeMorphism.ext {C : Type u} {P : C} {Q : C} {c : } {c' : } (f : c c') (g : c c') (w : f.hom = g.hom) :
f = g
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.ext_hom_hom {C : Type u} {P : C} {Q : C} {c : } {c' : } (φ : c.pt c'.pt) (winl : autoParam (CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl) _auto✝) (winr : autoParam (CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr) _auto✝) (wfst : autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst) _auto✝) (wsnd : autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd) _auto✝) :
(CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).hom.hom = φ.hom
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.ext_inv_hom {C : Type u} {P : C} {Q : C} {c : } {c' : } (φ : c.pt c'.pt) (winl : autoParam (CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl) _auto✝) (winr : autoParam (CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr) _auto✝) (wfst : autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst) _auto✝) (wsnd : autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd) _auto✝) :
(CategoryTheory.Limits.BinaryBicones.ext φ winl winr wfst wsnd).inv.hom = φ.inv
def CategoryTheory.Limits.BinaryBicones.ext {C : Type u} {P : C} {Q : C} {c : } {c' : } (φ : c.pt c'.pt) (winl : autoParam (CategoryTheory.CategoryStruct.comp c.inl φ.hom = c'.inl) _auto✝) (winr : autoParam (CategoryTheory.CategoryStruct.comp c.inr φ.hom = c'.inr) _auto✝) (wfst : autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.fst = c.fst) _auto✝) (wsnd : autoParam (CategoryTheory.CategoryStruct.comp φ.hom c'.snd = c.snd) _auto✝) :
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.
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_inr {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] (A : ) :
( A).inr = F.map A.inr
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_fst {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] (A : ) :
( A).fst = F.map A.fst
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_snd {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] (A : ) :
( A).snd = F.map A.snd
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_inl {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] (A : ) :
( A).inl = F.map A.inl
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.functoriality_map_hom {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] :
∀ {X Y : } (f : X Y), ( f).hom = F.map f.hom
@[simp]
theorem CategoryTheory.Limits.BinaryBicones.functoriality_obj_pt {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] (A : ) :
( A).pt = F.obj A.pt
def CategoryTheory.Limits.BinaryBicones.functoriality {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] :

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
instance CategoryTheory.Limits.BinaryBicones.functoriality_full {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] [F.Full] [F.Faithful] :
.Full
Equations
• =
instance CategoryTheory.Limits.BinaryBicones.functoriality_faithful {C : Type u} {D : Type uD} (P : C) (Q : C) (F : ) [F.PreservesZeroMorphisms] [F.Faithful] :
.Faithful
Equations
• =
def CategoryTheory.Limits.BinaryBicone.toCone {C : Type u} {P : C} {Q : C} (c : ) :

Extract the cone from a binary bicone.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.toCone_pt {C : Type u} {P : C} {Q : C} (c : ) :
c.toCone.pt = c.pt
@[simp]
theorem CategoryTheory.Limits.BinaryBicone.toCone_π_app_left {C : Type u} {P : C} {Q : C} (c : ) :
c.toCone.app = c.fst