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} [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.

Instances For

source

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.

Instances For

source

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

source

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.

Instances For

source

@[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

source

@[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

source

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.

Instances For

source

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.

Instances For

source

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

source

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.

Instances For

source

@[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

source

@[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

source

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.

Instances For

source

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.

Instances For

source

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

source

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.

Instances For

source

@[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

source

@[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

source

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.

Instances For

source

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.

Instances For

source

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

source

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.

Instances For

source

@[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

source

@[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

source

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

source

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.

Instances For

source

@[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 = CategoryTheory.Limits.prod.fst

source

@[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 = CategoryTheory.Limits.prod.snd

source

@[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

source

@[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

source

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

source

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.

Instances For

source

@[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 (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom = CategoryTheory.Limits.coprod.inl

source

@[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 (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom = CategoryTheory.Limits.coprod.inr

source

@[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

source

@[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