mathlib3 documentation

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.

source
noncomputable def category_theory.limits.binary_fan_zero_left {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.binary_fan 0 X

The limit cone for the product with a zero object.

Equations
source
noncomputable def category_theory.limits.binary_fan_zero_left_is_limit {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.is_limit (category_theory.limits.binary_fan_zero_left X)

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

Equations
source
@[protected, instance]
def category_theory.limits.has_binary_product_zero_left {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.has_binary_product 0 X
source
noncomputable def category_theory.limits.zero_prod_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
0 ⨯ X ≅ X

A zero object is a left unit for categorical product.

Equations
source
@[simp]
theorem category_theory.limits.zero_prod_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.limits.zero_prod_iso X).hom = category_theory.limits.prod.snd
source
@[simp]
theorem category_theory.limits.zero_prod_iso_inv_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.limits.zero_prod_iso X).inv ≫ category_theory.limits.prod.snd = 𝟙 X
source
noncomputable def category_theory.limits.binary_fan_zero_right {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.binary_fan X 0

The limit cone for the product with a zero object.

Equations
source
noncomputable def category_theory.limits.binary_fan_zero_right_is_limit {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.is_limit (category_theory.limits.binary_fan_zero_right X)

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

Equations
source
@[protected, instance]
def category_theory.limits.has_binary_product_zero_right {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.has_binary_product X 0
source
noncomputable def category_theory.limits.prod_zero_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
X ⨯ 0 ≅ X

A zero object is a right unit for categorical product.

Equations
source
@[simp]
theorem category_theory.limits.prod_zero_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.limits.prod_zero_iso X).hom = category_theory.limits.prod.fst
source
@[simp]
theorem category_theory.limits.prod_zero_iso_iso_inv_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.limits.prod_zero_iso X).inv ≫ category_theory.limits.prod.fst = 𝟙 X
source
noncomputable def category_theory.limits.binary_cofan_zero_left {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.binary_cofan 0 X

The colimit cocone for the coproduct with a zero object.

Equations
source
noncomputable def category_theory.limits.binary_cofan_zero_left_is_colimit {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan_zero_left X)

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

Equations
source
@[protected, instance]
def category_theory.limits.has_binary_coproduct_zero_left {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.has_binary_coproduct 0 X
source
noncomputable def category_theory.limits.zero_coprod_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
0 ⨿ X ≅ X

A zero object is a left unit for categorical coproduct.

Equations
source
@[simp]
theorem category_theory.limits.inr_zero_coprod_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.coprod.inr ≫ (category_theory.limits.zero_coprod_iso X).hom = 𝟙 X
source
@[simp]
theorem category_theory.limits.zero_coprod_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.limits.zero_coprod_iso X).inv = category_theory.limits.coprod.inr
source
noncomputable def category_theory.limits.binary_cofan_zero_right {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.binary_cofan X 0

The colimit cocone for the coproduct with a zero object.

Equations
source
noncomputable def category_theory.limits.binary_cofan_zero_right_is_colimit {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan_zero_right X)

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

Equations
source
@[protected, instance]
def category_theory.limits.has_binary_coproduct_zero_right {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.has_binary_coproduct X 0
source
noncomputable def category_theory.limits.coprod_zero_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
X ⨿ 0 ≅ X

A zero object is a right unit for categorical coproduct.

Equations
source
@[simp]
theorem category_theory.limits.inr_coprod_zeroiso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
category_theory.limits.coprod.inl ≫ (category_theory.limits.coprod_zero_iso X).hom = 𝟙 X
source
@[simp]
theorem category_theory.limits.coprod_zero_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X : C) :
(category_theory.limits.coprod_zero_iso X).inv = category_theory.limits.coprod.inl
source
@[protected, instance]
def category_theory.limits.has_pullback_over_zero {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
category_theory.limits.has_pullback 0 0
source
noncomputable def category_theory.limits.pullback_zero_zero_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
category_theory.limits.pullback 0 0 ≅ X ⨯ Y

The pullback over the zeron object is the product.

Equations
source
@[simp]
theorem category_theory.limits.pullback_zero_zero_iso_inv_fst {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
(category_theory.limits.pullback_zero_zero_iso X Y).inv ≫ category_theory.limits.pullback.fst = category_theory.limits.prod.fst
source
@[simp]
theorem category_theory.limits.pullback_zero_zero_iso_inv_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
(category_theory.limits.pullback_zero_zero_iso X Y).inv ≫ category_theory.limits.pullback.snd = category_theory.limits.prod.snd
source
@[simp]
theorem category_theory.limits.pullback_zero_zero_iso_hom_fst {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
(category_theory.limits.pullback_zero_zero_iso X Y).hom ≫ category_theory.limits.prod.fst = category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.pullback_zero_zero_iso_hom_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
(category_theory.limits.pullback_zero_zero_iso X Y).hom ≫ category_theory.limits.prod.snd = category_theory.limits.pullback.snd
source
@[protected, instance]
def category_theory.limits.has_pushout_over_zero {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.has_pushout 0 0
source
noncomputable def category_theory.limits.pushout_zero_zero_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.pushout 0 0 ≅ X ⨿ Y

The pushout over the zero object is the coproduct.

Equations
source
@[simp]
theorem category_theory.limits.inl_pushout_zero_zero_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.pushout.inl ≫ (category_theory.limits.pushout_zero_zero_iso X Y).hom = category_theory.limits.coprod.inl
source
@[simp]
theorem category_theory.limits.inr_pushout_zero_zero_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.pushout.inr ≫ (category_theory.limits.pushout_zero_zero_iso X Y).hom = category_theory.limits.coprod.inr
source
@[simp]
theorem category_theory.limits.inl_pushout_zero_zero_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.coprod.inl ≫ (category_theory.limits.pushout_zero_zero_iso X Y).inv = category_theory.limits.pushout.inl
source
@[simp]
theorem category_theory.limits.inr_pushout_zero_zero_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.coprod.inr ≫ (category_theory.limits.pushout_zero_zero_iso X Y).inv = category_theory.limits.pushout.inr