Limits involving zero objects #

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

source

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

source

def CategoryTheory.Limits.binaryFanZeroLeftIsLimit {C : Type u_1} [Category.{u_2, 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) ⋯ ⋯ ⋯

source

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

HasBinaryProduct 0 X

source

def CategoryTheory.Limits.zeroProdIso {C : Type u_1} [Category.{u_2, 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 }

source

@[simp]

theorem CategoryTheory.Limits.zeroProdIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) :

(zeroProdIso X).hom = prod.snd

source

@[simp]

theorem CategoryTheory.Limits.zeroProdIso_inv_snd {C : Type u_1} [Category.{u_2, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) :

CategoryStruct.comp (zeroProdIso X).inv prod.snd = CategoryStruct.id X

source

def CategoryTheory.Limits.binaryFanZeroRight {C : Type u_1} [Category.{u_2, 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

source

def CategoryTheory.Limits.binaryFanZeroRightIsLimit {C : Type u_1} [Category.{u_2, 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) ⋯ ⋯ ⋯

source

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

HasBinaryProduct X 0

source

def CategoryTheory.Limits.prodZeroIso {C : Type u_1} [Category.{u_2, 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.

source

@[simp]

theorem CategoryTheory.Limits.prodZeroIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) :

(prodZeroIso X).hom = prod.fst

source

@[simp]

theorem CategoryTheory.Limits.prodZeroIso_iso_inv_snd {C : Type u_1} [Category.{u_2, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) :

CategoryStruct.comp (prodZeroIso X).inv prod.fst = CategoryStruct.id X

source

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

source

def CategoryTheory.Limits.binaryCofanZeroLeftIsColimit {C : Type u_1} [Category.{u_2, 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) ⋯ ⋯ ⋯

source

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

HasBinaryCoproduct 0 X

source

def CategoryTheory.Limits.zeroCoprodIso {C : Type u_1} [Category.{u_2, 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.

source

@[simp]

theorem CategoryTheory.Limits.inr_zeroCoprodIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) :

CategoryStruct.comp coprod.inr (zeroCoprodIso X).hom = CategoryStruct.id X

source

@[simp]

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

(zeroCoprodIso X).inv = coprod.inr

source

def CategoryTheory.Limits.binaryCofanZeroRight {C : Type u_1} [Category.{u_2, 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

source

def CategoryTheory.Limits.binaryCofanZeroRightIsColimit {C : Type u_1} [Category.{u_2, 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) ⋯ ⋯ ⋯

source

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

HasBinaryCoproduct X 0

source

def CategoryTheory.Limits.coprodZeroIso {C : Type u_1} [Category.{u_2, 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.

source

@[simp]

theorem CategoryTheory.Limits.inr_coprodZeroIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) :

CategoryStruct.comp coprod.inl (coprodZeroIso X).hom = CategoryStruct.id X

source

@[simp]

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

(coprodZeroIso X).inv = coprod.inl

source

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

HasPullback 0 0

source

def CategoryTheory.Limits.pullbackZeroZeroIso {C : Type u_1} [Category.{u_2, 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.

source

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst {C : Type u_1} [Category.{u_2, 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

source

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd {C : Type u_1} [Category.{u_2, 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

source

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst {C : Type u_1} [Category.{u_2, 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

source

@[simp]

theorem CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd {C : Type u_1} [Category.{u_2, 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

source

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

HasPushout 0 0

source

def CategoryTheory.Limits.pushoutZeroZeroIso {C : Type u_1} [Category.{u_2, 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.

source

@[simp]

theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom {C : Type u_1} [Category.{u_2, 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

source

@[simp]

theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom {C : Type u_1} [Category.{u_2, 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

source

@[simp]

theorem CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv {C : Type u_1} [Category.{u_2, 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

source

@[simp]

theorem CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv {C : Type u_1} [Category.{u_2, 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

Documentation

Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Limits involving zero objects #