# Binary (co)products #

We define a category WalkingPair, which is the index category for a binary (co)product diagram. A convenience method pair X Y constructs the functor from the walking pair, hitting the given objects.

We define prod X Y and coprod X Y as limits and colimits of such functors.

Typeclasses HasBinaryProducts and HasBinaryCoproducts assert the existence of (co)limits shaped as walking pairs.

We include lemmas for simplifying equations involving projections and coprojections, and define braiding and associating isomorphisms, and the product comparison morphism.

## References #

The type of objects for the diagram indexing a binary (co)product.

Instances For
Equations
• = if h : x.toCtorIdx = y.toCtorIdx then else

The equivalence swapping left and right.

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

An equivalence from WalkingPair to Bool, sometimes useful when reindexing limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.pairFunction {C : Type u} (X : C) (Y : C) :

The function on the walking pair, sending the two points to X and Y.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.pairFunction_left {C : Type u} (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.Limits.pairFunction_right {C : Type u} (X : C) (Y : C) :
def CategoryTheory.Limits.pair {C : Type u} (X : C) (Y : C) :

The diagram on the walking pair, sending the two points to X and Y.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.pair_obj_left {C : Type u} (X : C) (Y : C) :
.obj = X
@[simp]
theorem CategoryTheory.Limits.pair_obj_right {C : Type u} (X : C) (Y : C) :
.obj = Y
def CategoryTheory.Limits.mapPair {C : Type u} (f : F.obj G.obj ) (g : F.obj G.obj ) :
F G

The natural transformation between two functors out of the walking pair, specified by its components.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.mapPair_left {C : Type u} (f : F.obj G.obj ) (g : F.obj G.obj ) :
.app = f
@[simp]
theorem CategoryTheory.Limits.mapPair_right {C : Type u} (f : F.obj G.obj ) (g : F.obj G.obj ) :
.app = g
@[simp]
theorem CategoryTheory.Limits.mapPairIso_inv_app {C : Type u} (f : F.obj G.obj ) (g : F.obj G.obj ) :
.inv.app X = .inv
@[simp]
theorem CategoryTheory.Limits.mapPairIso_hom_app {C : Type u} (f : F.obj G.obj ) (g : F.obj G.obj ) :
.hom.app X = .hom
def CategoryTheory.Limits.mapPairIso {C : Type u} (f : F.obj G.obj ) (g : F.obj G.obj ) :
F G

The natural isomorphism between two functors out of the walking pair, specified by its components.

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

Every functor out of the walking pair is naturally isomorphic (actually, equal) to a pair

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.pairComp {C : Type u} {D : Type u} (X : C) (Y : C) (F : ) :
.comp F CategoryTheory.Limits.pair (F.obj X) (F.obj Y)

The natural isomorphism between pair X Y ⋙ F and pair (F.obj X) (F.obj Y).

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.BinaryFan {C : Type u} (X : C) (Y : C) :
Type (max (max 0 u) v)

A binary fan is just a cone on a diagram indexing a product.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.BinaryFan.fst {C : Type u} {X : C} {Y : C} (s : ) :
.obj .obj

The first projection of a binary fan.

Equations
• s.fst = s.app
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.BinaryFan.snd {C : Type u} {X : C} {Y : C} (s : ) :
.obj .obj

The second projection of a binary fan.

Equations
• s.snd = s.app
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryFan.π_app_left {C : Type u} {X : C} {Y : C} (s : ) :
s.app = s.fst
@[simp]
theorem CategoryTheory.Limits.BinaryFan.π_app_right {C : Type u} {X : C} {Y : C} (s : ) :
s.app = s.snd
def CategoryTheory.Limits.BinaryFan.IsLimit.mk {C : Type u} {X : C} {Y : C} (s : ) (lift : {T : C} → (T X)(T Y)(T s.pt)) (hl₁ : ∀ {T : C} (f : T X) (g : T Y), CategoryTheory.CategoryStruct.comp (lift f g) s.fst = f) (hl₂ : ∀ {T : C} (f : T X) (g : T Y), CategoryTheory.CategoryStruct.comp (lift f g) s.snd = g) (uniq : ∀ {T : C} (f : T X) (g : T Y) (m : T s.pt), = f = gm = lift f g) :

A convenient way to show that a binary fan is a limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext {C : Type u} {W : C} {X : C} {Y : C} {s : } {f : W s.pt} {g : W s.pt} (h₁ : ) (h₂ : ) :
f = g
@[reducible, inline]
abbrev CategoryTheory.Limits.BinaryCofan {C : Type u} (X : C) (Y : C) :
Type (max (max 0 u) v)

A binary cofan is just a cocone on a diagram indexing a coproduct.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.BinaryCofan.inl {C : Type u} {X : C} {Y : C} (s : ) :
.obj .obj

The first inclusion of a binary cofan.

Equations
• s.inl = s.app
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.BinaryCofan.inr {C : Type u} {X : C} {Y : C} (s : ) :
.obj .obj

The second inclusion of a binary cofan.

Equations
• s.inr = s.app
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryCofan.ι_app_left {C : Type u} {X : C} {Y : C} (s : ) :
s.app = s.inl
@[simp]
theorem CategoryTheory.Limits.BinaryCofan.ι_app_right {C : Type u} {X : C} {Y : C} (s : ) :
s.app = s.inr
def CategoryTheory.Limits.BinaryCofan.IsColimit.mk {C : Type u} {X : C} {Y : C} (s : ) (desc : {T : C} → (X T)(Y T)(s.pt T)) (hd₁ : ∀ {T : C} (f : X T) (g : Y T), CategoryTheory.CategoryStruct.comp s.inl (desc f g) = f) (hd₂ : ∀ {T : C} (f : X T) (g : Y T), CategoryTheory.CategoryStruct.comp s.inr (desc f g) = g) (uniq : ∀ {T : C} (f : X T) (g : Y T) (m : s.pt T), = f = gm = desc f g) :

A convenient way to show that a binary cofan is a colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext {C : Type u} {W : C} {X : C} {Y : C} {s : } {f : s.pt W} {g : s.pt W} (h₁ : ) (h₂ : ) :
f = g
@[simp]
theorem CategoryTheory.Limits.BinaryFan.mk_pt {C : Type u} {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :
.pt = P
def CategoryTheory.Limits.BinaryFan.mk {C : Type u} {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :

A binary fan with vertex P consists of the two projections π₁ : P ⟶ X and π₂ : P ⟶ Y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryCofan.mk_pt {C : Type u} {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :
.pt = P
def CategoryTheory.Limits.BinaryCofan.mk {C : Type u} {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :

A binary cofan with vertex P consists of the two inclusions ι₁ : X ⟶ P and ι₂ : Y ⟶ P.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryFan.mk_fst {C : Type u} {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :
.fst = π₁
@[simp]
theorem CategoryTheory.Limits.BinaryFan.mk_snd {C : Type u} {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :
.snd = π₂
@[simp]
theorem CategoryTheory.Limits.BinaryCofan.mk_inl {C : Type u} {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :
.inl = ι₁
@[simp]
theorem CategoryTheory.Limits.BinaryCofan.mk_inr {C : Type u} {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :
.inr = ι₂
def CategoryTheory.Limits.isoBinaryFanMk {C : Type u} {X : C} {Y : C} (c : ) :

Every BinaryFan is isomorphic to an application of BinaryFan.mk.

Equations
Instances For

Every BinaryFan is isomorphic to an application of BinaryFan.mk.

Equations
Instances For
def CategoryTheory.Limits.BinaryFan.isLimitMk {C : Type u} {X : C} {Y : C} {W : C} {fst : W X} {snd : W Y} (lift : (s : ) → s.pt W) (fac_left : ∀ (s : ), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : ), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : ) (m : s.pt W), = s.fst = s.sndm = lift s) :

This is a more convenient formulation to show that a BinaryFan constructed using BinaryFan.mk is a limit cone.

Equations
Instances For
def CategoryTheory.Limits.BinaryCofan.isColimitMk {C : Type u} {X : C} {Y : C} {W : C} {inl : X W} {inr : Y W} (desc : (s : ) → W s.pt) (fac_left : ∀ (s : ), CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : ), CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : ) (m : W s.pt), = s.inl = s.inrm = desc s) :

This is a more convenient formulation to show that a BinaryCofan constructed using BinaryCofan.mk is a colimit cocone.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe {C : Type u} {W : C} {X : C} {Y : C} {s : } (f : W X) (g : W Y) :
= h.lift
def CategoryTheory.Limits.BinaryFan.IsLimit.lift' {C : Type u} {W : C} {X : C} {Y : C} {s : } (f : W X) (g : W Y) :
{ l : W s.pt // = f = g }

If s is a limit binary fan over X and Y, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ s.pt satisfying l ≫ s.fst = f and l ≫ s.snd = g.

Equations
• = h.lift ,
Instances For
@[simp]
theorem CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe {C : Type u} {W : C} {X : C} {Y : C} {s : } (f : X W) (g : Y W) :
= h.desc
def CategoryTheory.Limits.BinaryCofan.IsColimit.desc' {C : Type u} {W : C} {X : C} {Y : C} {s : } (f : X W) (g : Y W) :
{ l : s.pt W // = f = g }

If s is a colimit binary cofan over X and Y,, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : s.pt ⟶ W satisfying s.inl ≫ l = f and s.inr ≫ l = g.

Equations
• = h.desc ,
Instances For
def CategoryTheory.Limits.BinaryFan.isLimitFlip {C : Type u} {X : C} {Y : C} {c : } (hc : ) :

Binary products are symmetric.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst {C : Type u} {X : C} {Y : C} (c : ) :
theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd {C : Type u} {X : C} {Y : C} (c : ) :
noncomputable def CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso {C : Type u} {X : C} {Y : C} {X' : C} (c : ) (f : X X') :

If X' ≅ X, then X × Y also is the product of X' and Y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.BinaryFan.isLimitCompRightIso {C : Type u} {X : C} {Y : C} {Y' : C} (c : ) (f : Y Y') :

If Y' ≅ Y, then X x Y also is the product of X and Y'.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.BinaryCofan.isColimitFlip {C : Type u} {X : C} {Y : C} {c : } (hc : ) :

Binary coproducts are symmetric.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso {C : Type u} {X : C} {Y : C} {X' : C} (c : ) (f : X' X) :

If X' ≅ X, then X ⨿ Y also is the coproduct of X' and Y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.BinaryCofan.isColimitCompRightIso {C : Type u} {X : C} {Y : C} {Y' : C} (c : ) (f : Y' Y) :

If Y' ≅ Y, then X ⨿ Y also is the coproduct of X and Y'.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.HasBinaryProduct {C : Type u} (X : C) (Y : C) :

An abbreviation for HasLimit (pair X Y).

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.HasBinaryCoproduct {C : Type u} (X : C) (Y : C) :

An abbreviation for HasColimit (pair X Y).

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.prod {C : Type u} (X : C) (Y : C) :
C

If we have a product of X and Y, we can access it using prod X Y or X ⨯ Y.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.coprod {C : Type u} (X : C) (Y : C) :
C

If we have a coproduct of X and Y, we can access it using coprod X Y or X ⨿ Y.

Equations
Instances For

Notation for the product

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

Notation for the coproduct

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.prod.fst {C : Type u} {X : C} {Y : C} :
X Y X

The projection map to the first component of the product.

Equations
• CategoryTheory.Limits.prod.fst =
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.prod.snd {C : Type u} {X : C} {Y : C} :
X Y Y

The projection map to the second component of the product.

Equations
• CategoryTheory.Limits.prod.snd =
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.coprod.inl {C : Type u} {X : C} {Y : C} :
X X ⨿ Y

The inclusion map from the first component of the coproduct.

Equations
• CategoryTheory.Limits.coprod.inl =
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.coprod.inr {C : Type u} {X : C} {Y : C} :
Y X ⨿ Y

The inclusion map from the second component of the coproduct.

Equations
• CategoryTheory.Limits.coprod.inr =
Instances For
def CategoryTheory.Limits.prodIsProd {C : Type u} (X : C) (Y : C) :
CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)

The binary fan constructed from the projection maps is a limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.coprodIsCoprod {C : Type u} (X : C) (Y : C) :
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)

The binary cofan constructed from the coprojection maps is a colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.prod.hom_ext_iff {C : Type u} {W : C} {X : C} {Y : C} {f : W X Y} {g : W X Y} :
f = g CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd
theorem CategoryTheory.Limits.prod.hom_ext {C : Type u} {W : C} {X : C} {Y : C} {f : W X Y} {g : W X Y} (h₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst) (h₂ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd) :
f = g
theorem CategoryTheory.Limits.coprod.hom_ext_iff {C : Type u} {W : C} {X : C} {Y : C} {f : X ⨿ Y W} {g : X ⨿ Y W} :
f = g CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g
theorem CategoryTheory.Limits.coprod.hom_ext {C : Type u} {W : C} {X : C} {Y : C} {f : X ⨿ Y W} {g : X ⨿ Y W} (h₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g) (h₂ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g) :
f = g
@[reducible, inline]
abbrev CategoryTheory.Limits.prod.lift {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :
W X Y

If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism prod.lift f g : W ⟶ X ⨯ Y.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.diag {C : Type u} (X : C) :
X X X

diagonal arrow of the binary product in the category fam I

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.coprod.desc {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) :
X ⨿ Y W

If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism coprod.desc f g : X ⨿ Y ⟶ W.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.codiag {C : Type u} (X : C) :
X ⨿ X X

codiagonal arrow of the binary coproduct

Equations
Instances For
theorem CategoryTheory.Limits.prod.lift_fst_assoc {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) {Z : C} (h : X Z) :
theorem CategoryTheory.Limits.prod.lift_fst {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst = f
theorem CategoryTheory.Limits.prod.lift_snd_assoc {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.Limits.prod.lift_snd {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd = g
theorem CategoryTheory.Limits.coprod.inl_desc_assoc {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) {Z : C} (h : W Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl =
theorem CategoryTheory.Limits.coprod.inl_desc {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl = f
theorem CategoryTheory.Limits.coprod.inr_desc_assoc {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) {Z : C} (h : W Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr =
theorem CategoryTheory.Limits.coprod.inr_desc {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr = g
instance CategoryTheory.Limits.prod.mono_lift_of_mono_left {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :
Equations
• =
instance CategoryTheory.Limits.prod.mono_lift_of_mono_right {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :
Equations
• =
instance CategoryTheory.Limits.coprod.epi_desc_of_epi_left {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) :
Equations
• =
instance CategoryTheory.Limits.coprod.epi_desc_of_epi_right {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) :
Equations
• =
def CategoryTheory.Limits.prod.lift' {C : Type u} {W : C} {X : C} {Y : C} (f : W X) (g : W Y) :
{ l : W X Y // CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.fst = f CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.snd = g }

If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ X ⨯ Y satisfying l ≫ Prod.fst = f and l ≫ Prod.snd = g.

Equations
Instances For
def CategoryTheory.Limits.coprod.desc' {C : Type u} {W : C} {X : C} {Y : C} (f : X W) (g : Y W) :
{ l : X ⨿ Y W // CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl l = f CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr l = g }

If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : X ⨿ Y ⟶ W satisfying coprod.inl ≫ l = f and coprod.inr ≫ l = g.

Equations
Instances For
def CategoryTheory.Limits.prod.map {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
W X Y Z

If the products W ⨯ X and Y ⨯ Z exist, then every pair of morphisms f : W ⟶ Y and g : X ⟶ Z induces a morphism prod.map f g : W ⨯ X ⟶ Y ⨯ Z.

Equations
Instances For
def CategoryTheory.Limits.coprod.map {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
W ⨿ X Y ⨿ Z

If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of morphisms f : W ⟶ Y and g : W ⟶ Z induces a morphism coprod.map f g : W ⨿ X ⟶ Y ⨿ Z.

Equations
Instances For
theorem CategoryTheory.Limits.prod.comp_lift_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} (f : V W) (g : W X) (h : W Y) {Z : C} (h : X Y Z) :
@[simp]
theorem CategoryTheory.Limits.prod.comp_lift {C : Type u} {V : C} {W : C} {X : C} {Y : C} (f : V W) (g : W X) (h : W Y) :
theorem CategoryTheory.Limits.prod.comp_diag {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.prod.map_fst_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z✝) {Z : C} (h : Y Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst
@[simp]
theorem CategoryTheory.Limits.prod.map_fst {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f
@[simp]
theorem CategoryTheory.Limits.prod.map_snd_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z✝) {Z : C} (h : Z✝ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
@[simp]
theorem CategoryTheory.Limits.prod.map_snd {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g
@[simp]
theorem CategoryTheory.Limits.prod.map_id_id {C : Type u} {X : C} {Y : C} :
@[simp]
theorem CategoryTheory.Limits.prod.lift_fst_snd {C : Type u} {X : C} {Y : C} :
CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd =
@[simp]
theorem CategoryTheory.Limits.prod.lift_map_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : V X) (h : W Y) (k : X Z✝) {Z : C} (h : Y Z✝ Z) :
@[simp]
theorem CategoryTheory.Limits.prod.lift_map {C : Type u} {V : C} {W : C} {X : C} {Y : C} {Z : C} (f : V W) (g : V X) (h : W Y) (k : X Z) :
@[simp]
theorem CategoryTheory.Limits.prod.lift_fst_comp_snd_comp {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (g : W X) (g' : Y Z) :
CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g') =
@[simp]
theorem CategoryTheory.Limits.prod.map_map_assoc {C : Type u} {A₁ : C} {A₂ : C} {A₃ : C} {B₁ : C} {B₂ : C} {B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) {Z : C} (h : A₃ B₃ Z) :
@[simp]
theorem CategoryTheory.Limits.prod.map_map {C : Type u} {A₁ : C} {A₂ : C} {A₃ : C} {B₁ : C} {B₂ : C} {B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) :
theorem CategoryTheory.Limits.prod.map_swap_assoc {C : Type u} {A : C} {B : C} {X : C} {Y : C} (f : A B) (g : X Y) {Z : C} (h : Y B Z) :
theorem CategoryTheory.Limits.prod.map_swap {C : Type u} {A : C} {B : C} {X : C} {Y : C} (f : A B) (g : X Y) :
theorem CategoryTheory.Limits.prod.map_comp_id_assoc {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z✝) {Z : C} (h : Z✝ W Z) :
theorem CategoryTheory.Limits.prod.map_comp_id {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.Limits.prod.map_id_comp_assoc {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z✝) {Z : C} (h : W Z✝ Z) :
theorem CategoryTheory.Limits.prod.map_id_comp {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.Limits.prod.mapIso_hom {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem CategoryTheory.Limits.prod.mapIso_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
def CategoryTheory.Limits.prod.mapIso {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
W X Y Z

If the products W ⨯ X and Y ⨯ Z exist, then every pair of isomorphisms f : W ≅ Y and g : X ≅ Z induces an isomorphism prod.mapIso f g : W ⨯ X ≅ Y ⨯ Z.

Equations
Instances For
instance CategoryTheory.Limits.isIso_prod {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
Equations
• =
instance CategoryTheory.Limits.prod.map_mono {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
Equations
• =
theorem CategoryTheory.Limits.prod.diag_map_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Y Z) :
theorem CategoryTheory.Limits.prod.diag_map {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.prod.diag_map_fst_snd {C : Type u} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryProduct (X Y) (X Y)] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X Y)) (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) =
theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp_assoc {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (g : X Y) (g' : X' Y') {Z : C} (h : Y Y' Z) :
theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (g : X Y) (g' : X' Y') :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.coprod.desc_comp {C : Type u} {V : C} {W : C} {X : C} {Y : C} (f : V W) (g : X V) (h : Y V) :
theorem CategoryTheory.Limits.coprod.desc_comp_assoc {C : Type u} {V : C} {W : C} {X : C} {Y : C} (f : V W) (g : X V) (h : Y V) {Z : C} (l : W Z) :
theorem CategoryTheory.Limits.coprod.diag_comp {C : Type u} {X : C} {Y : C} (f : X Y) :
@[simp]
theorem CategoryTheory.Limits.coprod.inl_map_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z✝) {Z : C} (h : Y ⨿ Z✝ Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h)
@[simp]
theorem CategoryTheory.Limits.coprod.inl_map {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl = CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl
@[simp]
theorem CategoryTheory.Limits.coprod.inr_map_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z✝) {Z : C} (h : Y ⨿ Z✝ Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h)
@[simp]
theorem CategoryTheory.Limits.coprod.inr_map {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr
@[simp]
theorem CategoryTheory.Limits.coprod.map_id_id {C : Type u} {X : C} {Y : C} :
@[simp]
theorem CategoryTheory.Limits.coprod.desc_inl_inr {C : Type u} {X : C} {Y : C} :
CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr =
theorem CategoryTheory.Limits.coprod.map_desc_assoc {C : Type u} {S : C} {T : C} {U : C} {V : C} {W : C} (f : U S) (g : W S) (h : T U) (k : V W) {Z : C} (h : S Z) :
@[simp]
theorem CategoryTheory.Limits.coprod.map_desc {C : Type u} {S : C} {T : C} {U : C} {V : C} {W : C} (f : U S) (g : W S) (h : T U) (k : V W) :
@[simp]
theorem CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (g : W X) (g' : Y Z) :
CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.coprod.inr) =
@[simp]
theorem CategoryTheory.Limits.coprod.map_map_assoc {C : Type u} {A₁ : C} {A₂ : C} {A₃ : C} {B₁ : C} {B₂ : C} {B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) {Z : C} (h : A₃ ⨿ B₃ Z) :
@[simp]
theorem CategoryTheory.Limits.coprod.map_map {C : Type u} {A₁ : C} {A₂ : C} {A₃ : C} {B₁ : C} {B₂ : C} {B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) :
theorem CategoryTheory.Limits.coprod.map_swap_assoc {C : Type u} {A : C} {B : C} {X : C} {Y : C} (f : A B) (g : X Y) {Z : C} (h : Y ⨿ B Z) :
theorem CategoryTheory.Limits.coprod.map_swap {C : Type u} {A : C} {B : C} {X : C} {Y : C} (f : A B) (g : X Y) :
theorem CategoryTheory.Limits.coprod.map_comp_id_assoc {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z✝) {Z : C} (h : Z✝ ⨿ W Z) :
theorem CategoryTheory.Limits.coprod.map_comp_id {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z) :
theorem CategoryTheory.Limits.coprod.map_id_comp_assoc {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z✝) {Z : C} (h : W ⨿ Z✝ Z) :
theorem CategoryTheory.Limits.coprod.map_id_comp {C : Type u} {X : C} {Y : C} {Z : C} {W : C} (f : X Y) (g : Y Z) :
@[simp]
theorem CategoryTheory.Limits.coprod.mapIso_hom {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem CategoryTheory.Limits.coprod.mapIso_inv {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
def CategoryTheory.Limits.coprod.mapIso {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
W ⨿ X Y ⨿ Z

If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of isomorphisms f : W ≅ Y and g : W ≅ Z induces an isomorphism coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z.

Equations
Instances For
instance CategoryTheory.Limits.isIso_coprod {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
Equations
• =
instance CategoryTheory.Limits.coprod.map_epi {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} (f : W Y) (g : X Z) :
Equations
• =
theorem CategoryTheory.Limits.coprod.map_codiag_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.Limits.coprod.map_codiag {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag_assoc {C : Type u} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] {Z : C} (h : X ⨿ Y Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr) = h
theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag_assoc {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (g : X Y) (g' : X' Y') {Z : C} (h : Y ⨿ Y' Z) :
theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (g : X Y) (g' : X' Y') :
@[reducible, inline]

HasBinaryProducts represents a choice of product for every pair of objects.

Equations
Instances For
@[reducible, inline]

HasBinaryCoproducts represents a choice of coproduct for every pair of objects.

Equations
Instances For

If C has all limits of diagrams pair X Y, then it has all binary products

If C has all colimits of diagrams pair X Y, then it has all binary coproducts

@[simp]
theorem CategoryTheory.Limits.prod.braiding_inv {C : Type u} (P : C) (Q : C) :
.inv = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
@[simp]
theorem CategoryTheory.Limits.prod.braiding_hom {C : Type u} (P : C) (Q : C) :
.hom = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
def CategoryTheory.Limits.prod.braiding {C : Type u} (P : C) (Q : C) :
P Q Q P

The braiding isomorphism which swaps a binary product.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.braid_natural_assoc {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : Z✝ W) {Z : C} (h : W Y Z) :
theorem CategoryTheory.Limits.braid_natural {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : Z W) :

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

theorem CategoryTheory.Limits.prod.symmetry'_assoc {C : Type u} (P : C) (Q : C) {Z : C} (h : P Q Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) h) = h
theorem CategoryTheory.Limits.prod.symmetry' {C : Type u} (P : C) (Q : C) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) =
theorem CategoryTheory.Limits.prod.symmetry_assoc {C : Type u} (P : C) (Q : C) {Z : C} (h : P Q Z) :
theorem CategoryTheory.Limits.prod.symmetry {C : Type u} (P : C) (Q : C) :

The braiding isomorphism is symmetric.

@[simp]
theorem CategoryTheory.Limits.prod.associator_hom {C : Type u} (P : C) (Q : C) (R : C) :
.hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
@[simp]
theorem CategoryTheory.Limits.prod.associator_inv {C : Type u} (P : C) (Q : C) (R : C) :
.inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
def CategoryTheory.Limits.prod.associator {C : Type u} (P : C) (Q : C) (R : C) :
(P Q) R P Q R

The associator isomorphism for binary products.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.prod.associator_naturality_assoc {C : Type u} {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) {Z : C} (h : Y₁ Y₂ Y₃ Z) :
theorem CategoryTheory.Limits.prod.associator_naturality {C : Type u} {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
=
@[simp]
@[simp]
theorem CategoryTheory.Limits.prod.leftUnitor_hom {C : Type u} (P : C) :
= CategoryTheory.Limits.prod.snd

The left unitor isomorphism for binary products with the terminal object.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.prod.rightUnitor_hom {C : Type u} (P : C) :
= CategoryTheory.Limits.prod.fst
@[simp]

The right unitor isomorphism for binary products with the terminal object.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : (⊤_ C) Y Z) :
theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality_assoc {C : Type u} {X : C} {Y : C} (f : X Y) {Z : C} (h : Y ⊤_ C Z) :
theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Limits.prod.triangle {C : Type u} (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.Limits.coprod.braiding_inv {C : Type u} (P : C) (Q : C) :
.inv = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
@[simp]
theorem CategoryTheory.Limits.coprod.braiding_hom {C : Type u} (P : C) (Q : C) :
.hom = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
def CategoryTheory.Limits.coprod.braiding {C : Type u} (P : C) (Q : C) :
P ⨿ Q Q ⨿ P

The braiding isomorphism which swaps a binary coproduct.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.coprod.symmetry'_assoc {C : Type u} (P : C) (Q : C) {Z : C} (h : P ⨿ Q Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) h) = h
theorem CategoryTheory.Limits.coprod.symmetry' {C : Type u} (P : C) (Q : C) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) =
theorem CategoryTheory.Limits.coprod.symmetry {C : Type u} (P : C) (Q : C) :

The braiding isomorphism is symmetric.

@[simp]
theorem CategoryTheory.Limits.coprod.associator_hom {C : Type u} (P : C) (Q : C) (R : C) :
.hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
@[simp]
theorem CategoryTheory.Limits.coprod.associator_inv {C : Type u} (P : C) (Q : C) (R : C) :
.inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)
def CategoryTheory.Limits.coprod.associator {C : Type u} (P : C) (Q : C) (R : C) :
(P ⨿ Q) ⨿ R P ⨿ Q ⨿ R

The associator isomorphism for binary coproducts.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.coprod.associator_naturality {C : Type u} {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
=
@[simp]
theorem CategoryTheory.Limits.coprod.leftUnitor_inv {C : Type u} (P : C) :
= CategoryTheory.Limits.coprod.inr
@[simp]

The left unitor isomorphism for binary coproducts with the initial object.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem CategoryTheory.Limits.coprod.rightUnitor_inv {C : Type u} (P : C) :
= CategoryTheory.Limits.coprod.inl

The right unitor isomorphism for binary coproducts with the initial object.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.prod.functor_map_app {C : Type u} :
∀ {X Y : C} (f : X Y) (T : C), (CategoryTheory.Limits.prod.functor.map f).app T =
@[simp]
theorem CategoryTheory.Limits.prod.functor_obj_obj {C : Type u} (X : C) (Y : C) :
(CategoryTheory.Limits.prod.functor.obj X).obj Y = (X Y)
@[simp]
theorem CategoryTheory.Limits.prod.functor_obj_map {C : Type u} (X : C) {Y : C} {Z : C} (g : Y Z) :
(CategoryTheory.Limits.prod.functor.obj X).map g =

The binary product functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.prod.functorLeftComp {C : Type u} (X : C) (Y : C) :
CategoryTheory.Limits.prod.functor.obj (X Y) (CategoryTheory.Limits.prod.functor.obj Y).comp (CategoryTheory.Limits.prod.functor.obj X)

The product functor can be decomposed.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coprod.functor_obj_obj {C : Type u} (X : C) (Y : C) :
(CategoryTheory.Limits.coprod.functor.obj X).obj Y = (X ⨿ Y)
@[simp]
theorem CategoryTheory.Limits.coprod.functor_map_app {C : Type u} :
∀ {X Y : C} (f : X Y) (T : C), (CategoryTheory.Limits.coprod.functor.map f).app T =
@[simp]
theorem CategoryTheory.Limits.coprod.functor_obj_map {C : Type u} (X : C) {Y : C} {Z : C} (g : Y Z) :
(CategoryTheory.Limits.coprod.functor.obj X).map g =

The binary coproduct functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.coprod.functorLeftComp {C : Type u} (X : C) (Y : C) :
CategoryTheory.Limits.coprod.functor.obj (X ⨿ Y) (CategoryTheory.Limits.coprod.functor.obj Y).comp (CategoryTheory.Limits.coprod.functor.obj X)

The coproduct functor can be decomposed.

Equations
Instances For
def CategoryTheory.Limits.prodComparison {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] :
F.obj (A B) F.obj A F.obj B

The product comparison morphism.

In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary products.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.prodComparison_fst_assoc {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h
@[simp]
theorem CategoryTheory.Limits.prodComparison_fst {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst = F.map CategoryTheory.Limits.prod.fst
@[simp]
theorem CategoryTheory.Limits.prodComparison_snd_assoc {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj B Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.snd) h
@[simp]
theorem CategoryTheory.Limits.prodComparison_snd {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd = F.map CategoryTheory.Limits.prod.snd
theorem CategoryTheory.Limits.prodComparison_natural_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A A') (g : B B') {Z : D} (h : F.obj A' F.obj B' Z) :
theorem CategoryTheory.Limits.prodComparison_natural {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A A') (g : B B') :

Naturality of the prodComparison morphism in both arguments.

@[simp]
theorem CategoryTheory.Limits.prodComparisonNatTrans_app {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) :
def CategoryTheory.Limits.prodComparisonNatTrans {C : Type u} {D : Type u₂} [] (F : ) (A : C) :
(CategoryTheory.Limits.prod.functor.obj A).comp F F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))

The product comparison morphism from F(A ⨯ -) to FA ⨯ F-, whose components are given by prodComparison.

Equations
• = { app := fun (B : C) => , naturality := }
Instances For
theorem CategoryTheory.Limits.inv_prodComparison_map_fst_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
theorem CategoryTheory.Limits.inv_prodComparison_map_fst {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst
theorem CategoryTheory.Limits.inv_prodComparison_map_snd_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj B Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.snd) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
theorem CategoryTheory.Limits.inv_prodComparison_map_snd {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.snd) = CategoryTheory.Limits.prod.snd
theorem CategoryTheory.Limits.prodComparison_inv_natural_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A A') (g : B B') {Z : D} (h : F.obj (A' B') Z) :
theorem CategoryTheory.Limits.prodComparison_inv_natural {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A A') (g : B B') :

If the product comparison morphism is an iso, its inverse is natural.

@[simp]
theorem CategoryTheory.Limits.prodComparisonNatIso_hom {C : Type u} {D : Type u₂} [] (F : ) (A : C) [∀ (B : C), ] :
@[simp]
theorem CategoryTheory.Limits.prodComparisonNatIso_inv {C : Type u} {D : Type u₂} [] (F : ) (A : C) [∀ (B : C), ] :
= (CategoryTheory.asIso { app := fun (B : C) => , naturality := }).inv
def CategoryTheory.Limits.prodComparisonNatIso {C : Type u} {D : Type u₂} [] (F : ) (A : C) [∀ (B : C), ] :
(CategoryTheory.Limits.prod.functor.obj A).comp F F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))

The natural isomorphism F(A ⨯ -) ≅ FA ⨯ F-, provided each prodComparison F A B is an isomorphism (as B changes).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.prodComparison_comp {C : Type u} {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))] [CategoryTheory.Limits.HasBinaryProduct ((F.comp G).obj A) ((F.comp G).obj B)] :
def CategoryTheory.Limits.coprodComparison {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] :
F.obj A ⨿ F.obj B F.obj (A ⨿ B)

The coproduct comparison morphism.

In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary coproducts.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.coprodComparison_inl_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) h
@[simp]
theorem CategoryTheory.Limits.coprodComparison_inl {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl = F.map CategoryTheory.Limits.coprod.inl
@[simp]
theorem CategoryTheory.Limits.coprodComparison_inr_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) h
@[simp]
theorem CategoryTheory.Limits.coprodComparison_inr {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr = F.map CategoryTheory.Limits.coprod.inr
theorem CategoryTheory.Limits.coprodComparison_natural_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A A') (g : B B') {Z : D} (h : F.obj (A' ⨿ B') Z) :
theorem CategoryTheory.Limits.coprodComparison_natural {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A A') (g : B B') :

Naturality of the coprod_comparison morphism in both arguments.

@[simp]
theorem CategoryTheory.Limits.coprodComparisonNatTrans_app {C : Type u} {D : Type u₂} [] (F : ) (A : C) (B : C) :
def CategoryTheory.Limits.coprodComparisonNatTrans {C : Type u} {D : Type u₂} [] (F : ) (A : C) :
F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) (CategoryTheory.Limits.coprod.functor.obj A).comp F

The coproduct comparison morphism from FA ⨿ F- to F(A ⨿ -), whose components are given by coprodComparison.

Equations
• = { app := fun (B : C) => , naturality := }
Instances For
theorem CategoryTheory.Limits.map_inl_inv_coprodComparison_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A ⨿ F.obj B Z) :
CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
theorem CategoryTheory.Limits.map_inl_inv_coprodComparison {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) = CategoryTheory.Limits.coprod.inl
theorem CategoryTheory.Limits.map_inr_inv_coprodComparison_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A ⨿ F.obj B Z) :
CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
theorem CategoryTheory.Limits.map_inr_inv_coprodComparison {C : Type u} {D : Type u₂} [] (F : ) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] :
CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) = CategoryTheory.Limits.coprod.inr
theorem CategoryTheory.Limits.coprodComparison_inv_natural_assoc {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A A') (g : B B') {Z : D} (h : F.obj A' ⨿ F.obj B' Z) :
=
theorem CategoryTheory.Limits.coprodComparison_inv_natural {C : Type u} {D : Type u₂} [] (F : ) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A A') (g : B B') :

If the coproduct comparison morphism is an iso, its inverse is natural.

@[simp]
theorem CategoryTheory.Limits.coprodComparisonNatIso_hom {C : Type u} {D : Type u₂} [] (F : ) [