# Limits involving zero objects #

Binary products and coproducts with a zero object always exist, and pullbacks/pushouts over a zero object are products/coproducts.

The limit cone for the product with a zero object.

Equations
Instances For

The limit cone for the product with a zero object is limiting.

Equations
Instances For
Equations
• =
def CategoryTheory.Limits.zeroProdIso {C : Type u_1} [] (X : C) :
0 X X

A zero object is a left unit for categorical product.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.zeroProdIso_hom {C : Type u_1} [] (X : C) :
= CategoryTheory.Limits.prod.snd
@[simp]
theorem CategoryTheory.Limits.zeroProdIso_inv_snd {C : Type u_1} [] (X : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd =

The limit cone for the product with a zero object.

Equations
Instances For

The limit cone for the product with a zero object is limiting.

Equations
Instances For
Equations
• =
def CategoryTheory.Limits.prodZeroIso {C : Type u_1} [] (X : C) :
X 0 X

A zero object is a right unit for categorical product.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.prodZeroIso_hom {C : Type u_1} [] (X : C) :
= CategoryTheory.Limits.prod.fst
@[simp]
theorem CategoryTheory.Limits.prodZeroIso_iso_inv_snd {C : Type u_1} [] (X : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst =

The colimit cocone for the coproduct with a zero object.

Equations
Instances For

The colimit cocone for the coproduct with a zero object is colimiting.

Equations
Instances For
Equations
• =
def CategoryTheory.Limits.zeroCoprodIso {C : Type u_1} [] (X : C) :
0 ⨿ X X

A zero object is a left unit for categorical coproduct.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.inr_zeroCoprodIso_hom {C : Type u_1} [] (X : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr =
@[simp]
theorem CategoryTheory.Limits.zeroCoprodIso_inv {C : Type u_1} [] (X : C) :
= CategoryTheory.Limits.coprod.inr

The colimit cocone for the coproduct with a zero object.

Equations
Instances For

The colimit cocone for the coproduct with a zero object is colimiting.

Equations
Instances For
Equations
• =
def CategoryTheory.Limits.coprodZeroIso {C : Type u_1} [] (X : C) :
X ⨿ 0 X

A zero object is a right unit for categorical coproduct.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.inr_coprodZeroIso_hom {C : Type u_1} [] (X : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl =
@[simp]
theorem CategoryTheory.Limits.coprodZeroIso_inv {C : Type u_1} [] (X : C) :
= CategoryTheory.Limits.coprod.inl
instance CategoryTheory.Limits.hasPullback_over_zero {C : Type u_1} [] (X : C) (Y : C) :
Equations
• =
def CategoryTheory.Limits.pullbackZeroZeroIso {C : Type u_1} [] (X : C) (Y : C) :
X Y

The pullback over the zero object is the product.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst {C : Type u_1} [] (X : C) (Y : C) :
= CategoryTheory.Limits.prod.fst
@[simp]
theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd {C : Type u_1} [] (X : C) (Y : C) :
= CategoryTheory.Limits.prod.snd
@[simp]
theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst {C : Type u_1} [] (X : C) (Y : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst =
@[simp]
theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd {C : Type u_1} [] (X : C) (Y : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd =
instance CategoryTheory.Limits.hasPushout_over_zero {C : Type u_1} [] (X : C) (Y : C) :
Equations
• =
def CategoryTheory.Limits.pushoutZeroZeroIso {C : Type u_1} [] (X : C) (Y : C) :
X ⨿ Y

The pushout over the zero object is the coproduct.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom {C : Type u_1} [] (X : C) (Y : C) :
= CategoryTheory.Limits.coprod.inl
@[simp]
theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom {C : Type u_1} [] (X : C) (Y : C) :
= CategoryTheory.Limits.coprod.inr
@[simp]
theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv {C : Type u_1} [] (X : C) (Y : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl .inv =
@[simp]
theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv {C : Type u_1} [] (X : C) (Y : C) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr .inv =