Limits involving zero objects

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

noncomputable def CategoryTheory.Limits.binaryFanZeroLeft {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : BinaryFan 0 X

The limit cone for the product with a zero object.

Equations

• CategoryTheory.Limits.binaryFanZeroLeft X = CategoryTheory.Limits.BinaryFan.mk 0 (CategoryTheory.CategoryStruct.id X)

noncomputable def CategoryTheory.Limits.binaryFanZeroLeftIsLimit {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : IsLimit (binaryFanZeroLeft X)

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

Equations

• CategoryTheory.Limits.binaryFanZeroLeftIsLimit X = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (s : CategoryTheory.Limits.BinaryFan 0 X) => s.snd) ⋯ ⋯ ⋯

instance CategoryTheory.Limits.hasBinaryProduct_zero_left {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : HasBinaryProduct 0 X

noncomputable def CategoryTheory.Limits.zeroProdIso {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : 0 ⨯ X ≅ X

A zero object is a left unit for categorical product.

Equations

• CategoryTheory.Limits.zeroProdIso X = CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.binaryFanZeroLeft X, isLimit := CategoryTheory.Limits.binaryFanZeroLeftIsLimit X }

@[simp]

theorem CategoryTheory.Limits.zeroProdIso_hom {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : (zeroProdIso X).hom = prod.snd

@[simp]

theorem CategoryTheory.Limits.zeroProdIso_inv_snd {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : CategoryStruct.comp (zeroProdIso X).inv prod.snd = CategoryStruct.id X

noncomputable def CategoryTheory.Limits.binaryFanZeroRight {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : BinaryFan X 0

The limit cone for the product with a zero object.

Equations

• CategoryTheory.Limits.binaryFanZeroRight X = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X) 0

noncomputable def CategoryTheory.Limits.binaryFanZeroRightIsLimit {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : IsLimit (binaryFanZeroRight X)

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

Equations

• CategoryTheory.Limits.binaryFanZeroRightIsLimit X = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (s : CategoryTheory.Limits.BinaryFan X 0) => s.fst) ⋯ ⋯ ⋯

instance CategoryTheory.Limits.hasBinaryProduct_zero_right {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : HasBinaryProduct X 0

noncomputable def CategoryTheory.Limits.prodZeroIso {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (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.

@[simp]

theorem CategoryTheory.Limits.prodZeroIso_hom {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : (prodZeroIso X).hom = prod.fst

@[simp]

theorem CategoryTheory.Limits.prodZeroIso_iso_inv_snd {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : CategoryStruct.comp (prodZeroIso X).inv prod.fst = CategoryStruct.id X

noncomputable def CategoryTheory.Limits.binaryCofanZeroLeft {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : BinaryCofan 0 X

The colimit cocone for the coproduct with a zero object.

Equations

• CategoryTheory.Limits.binaryCofanZeroLeft X = CategoryTheory.Limits.BinaryCofan.mk 0 (CategoryTheory.CategoryStruct.id X)

noncomputable def CategoryTheory.Limits.binaryCofanZeroLeftIsColimit {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : IsColimit (binaryCofanZeroLeft X)

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

Equations

• CategoryTheory.Limits.binaryCofanZeroLeftIsColimit X = CategoryTheory.Limits.BinaryCofan.isColimitMk (fun (s : CategoryTheory.Limits.BinaryCofan 0 X) => s.inr) ⋯ ⋯ ⋯

instance CategoryTheory.Limits.hasBinaryCoproduct_zero_left {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : HasBinaryCoproduct 0 X

noncomputable def CategoryTheory.Limits.zeroCoprodIso {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (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.

@[simp]

theorem CategoryTheory.Limits.inr_zeroCoprodIso_hom {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : CategoryStruct.comp coprod.inr (zeroCoprodIso X).hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.zeroCoprodIso_inv {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : (zeroCoprodIso X).inv = coprod.inr

noncomputable def CategoryTheory.Limits.binaryCofanZeroRight {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : BinaryCofan X 0

The colimit cocone for the coproduct with a zero object.

Equations

• CategoryTheory.Limits.binaryCofanZeroRight X = CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.id X) 0

noncomputable def CategoryTheory.Limits.binaryCofanZeroRightIsColimit {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : IsColimit (binaryCofanZeroRight X)

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

Equations

• CategoryTheory.Limits.binaryCofanZeroRightIsColimit X = CategoryTheory.Limits.BinaryCofan.isColimitMk (fun (s : CategoryTheory.Limits.BinaryCofan X 0) => s.inl) ⋯ ⋯ ⋯

instance CategoryTheory.Limits.hasBinaryCoproduct_zero_right {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : HasBinaryCoproduct X 0

noncomputable def CategoryTheory.Limits.coprodZeroIso {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (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.

@[simp]

theorem CategoryTheory.Limits.inr_coprodZeroIso_hom {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : CategoryStruct.comp coprod.inl (coprodZeroIso X).hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.coprodZeroIso_inv {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : (coprodZeroIso X).inv = coprod.inl

instance CategoryTheory.Limits.hasPullback_over_zero {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : HasPullback 0 0

noncomputable def CategoryTheory.Limits.pullbackZeroZeroIso {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : pullback 0 0 ≅ X ⨯ Y

The pullback over the zero object is the product.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (pullbackZeroZeroIso X Y).inv (pullback.fst 0 0) = prod.fst

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (pullbackZeroZeroIso X Y).inv (pullback.snd 0 0) = prod.snd

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (pullbackZeroZeroIso X Y).hom prod.fst = pullback.fst 0 0

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (pullbackZeroZeroIso X Y).hom prod.snd = pullback.snd 0 0

instance CategoryTheory.Limits.hasPushout_over_zero {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : HasPushout 0 0

noncomputable def CategoryTheory.Limits.pushoutZeroZeroIso {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : pushout 0 0 ≅ X ⨿ Y

The pushout over the zero object is the coproduct.

Equations

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

@[simp]

theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp (pushout.inl 0 0) (pushoutZeroZeroIso X Y).hom = coprod.inl

@[simp]

theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp (pushout.inr 0 0) (pushoutZeroZeroIso X Y).hom = coprod.inr

@[simp]

theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp coprod.inl (pushoutZeroZeroIso X Y).inv = pushout.inl 0 0

@[simp]

theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp coprod.inr (pushoutZeroZeroIso X Y).inv = pushout.inr 0 0