Limits involving zero objects

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

def CategoryTheory.Limits.binaryFanZeroLeft {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.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)

def CategoryTheory.Limits.binaryFanZeroLeftIsLimit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.HasBinaryProduct 0 X

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.zeroProdIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : (CategoryTheory.Limits.zeroProdIso X).hom = CategoryTheory.Limits.prod.snd

@[simp]

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

def CategoryTheory.Limits.binaryFanZeroRight {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.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

def CategoryTheory.Limits.binaryFanZeroRightIsLimit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.HasBinaryProduct X 0

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.prodZeroIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : (CategoryTheory.Limits.prodZeroIso X).hom = CategoryTheory.Limits.prod.fst

@[simp]

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

def CategoryTheory.Limits.binaryCofanZeroLeft {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.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)

def CategoryTheory.Limits.binaryCofanZeroLeftIsColimit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.HasBinaryCoproduct 0 X

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.zeroCoprodIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.zeroCoprodIso X).hom = CategoryTheory.CategoryStruct.id X

@[simp]

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

def CategoryTheory.Limits.binaryCofanZeroRight {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.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

def CategoryTheory.Limits.binaryCofanZeroRightIsColimit {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.HasBinaryCoproduct X 0

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.coprodZeroIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprodZeroIso X).hom = CategoryTheory.CategoryStruct.id X

@[simp]

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

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

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.pullbackZeroZeroIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackZeroZeroIso X Y).inv (CategoryTheory.Limits.pullback.fst 0 0) = CategoryTheory.Limits.prod.fst

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.pushoutZeroZeroIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.Limits.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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) (Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl 0 0) (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom = CategoryTheory.Limits.coprod.inl

@[simp]

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

@[simp]

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

@[simp]

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