mathlib3documentation

category_theory.limits.constructions.zero_objects

Limits involving zero objects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

noncomputable def category_theory.limits.binary_fan_zero_left {C : Type u_1} (X : C) :

The limit cone for the product with a zero object.

Equations

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

Equations
@[protected, instance]
noncomputable def category_theory.limits.zero_prod_iso {C : Type u_1} (X : C) :
0 X X

A zero object is a left unit for categorical product.

Equations
@[simp]
@[simp]
noncomputable def category_theory.limits.binary_fan_zero_right {C : Type u_1} (X : C) :

The limit cone for the product with a zero object.

Equations

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

Equations
@[protected, instance]
noncomputable def category_theory.limits.prod_zero_iso {C : Type u_1} (X : C) :
X 0 X

A zero object is a right unit for categorical product.

Equations
@[simp]
@[simp]
noncomputable def category_theory.limits.binary_cofan_zero_left {C : Type u_1} (X : C) :

The colimit cocone for the coproduct with a zero object.

Equations

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

Equations
@[protected, instance]
noncomputable def category_theory.limits.zero_coprod_iso {C : Type u_1} (X : C) :
0 ⨿ X X

A zero object is a left unit for categorical coproduct.

Equations
@[simp]
@[simp]
noncomputable def category_theory.limits.binary_cofan_zero_right {C : Type u_1} (X : C) :

The colimit cocone for the coproduct with a zero object.

Equations

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

Equations
@[protected, instance]
noncomputable def category_theory.limits.coprod_zero_iso {C : Type u_1} (X : C) :
X ⨿ 0 X

A zero object is a right unit for categorical coproduct.

Equations
@[simp]
@[simp]
@[protected, instance]
noncomputable def category_theory.limits.pullback_zero_zero_iso {C : Type u_1} (X Y : C)  :

The pullback over the zeron object is the product.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
noncomputable def category_theory.limits.pushout_zero_zero_iso {C : Type u_1} (X Y : C)  :
X ⨿ Y

The pushout over the zero object is the coproduct.

Equations
@[simp]
@[simp]
@[simp]
@[simp]