ZeroObjects

📁 Source: Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean

Statistics

Metric	Count
Definitions `binaryCofanZeroLeft`, `binaryCofanZeroLeftIsColimit`, `binaryCofanZeroRight`, `binaryCofanZeroRightIsColimit`, `binaryFanZeroLeft`, `binaryFanZeroLeftIsLimit`, `binaryFanZeroRight`, `binaryFanZeroRightIsLimit`, `coprodZeroIso`, `prodZeroIso`, `pullbackZeroZeroIso`, `pushoutZeroZeroIso`, `zeroCoprodIso`, `zeroProdIso`	14
Theorems `coprodZeroIso_inv`, `hasBinaryCoproduct_zero_left`, `hasBinaryCoproduct_zero_right`, `hasBinaryProduct_zero_left`, `hasBinaryProduct_zero_right`, `hasPullback_over_zero`, `hasPushout_over_zero`, `inl_pushoutZeroZeroIso_hom`, `inl_pushoutZeroZeroIso_inv`, `inr_coprodZeroIso_hom`, `inr_pushoutZeroZeroIso_hom`, `inr_pushoutZeroZeroIso_inv`, `inr_zeroCoprodIso_hom`, `prodZeroIso_hom`, `prodZeroIso_iso_inv_snd`, `pullbackZeroZeroIso_hom_fst`, `pullbackZeroZeroIso_hom_snd`, `pullbackZeroZeroIso_inv_fst`, `pullbackZeroZeroIso_inv_snd`, `zeroCoprodIso_inv`, `zeroProdIso_hom`, `zeroProdIso_inv_snd`	22
Total	36

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`binaryCofanZeroLeft` 📖	CompOp	—
`binaryCofanZeroLeftIsColimit` 📖	CompOp	—
`binaryCofanZeroRight` 📖	CompOp	—
`binaryCofanZeroRightIsColimit` 📖	CompOp	—
`binaryFanZeroLeft` 📖	CompOp	—
`binaryFanZeroLeftIsLimit` 📖	CompOp	—
`binaryFanZeroRight` 📖	CompOp	—
`binaryFanZeroRightIsLimit` 📖	CompOp	—
`coprodZeroIso` 📖	CompOp	2 math math: `coprodZeroIso_inv`, `inr_coprodZeroIso_hom`
`prodZeroIso` 📖	CompOp	2 math math: `prodZeroIso_hom`, `prodZeroIso_iso_inv_snd`
`pullbackZeroZeroIso` 📖	CompOp	4 math math: `pullbackZeroZeroIso_inv_fst`, `pullbackZeroZeroIso_hom_snd`, `pullbackZeroZeroIso_hom_fst`, `pullbackZeroZeroIso_inv_snd`
`pushoutZeroZeroIso` 📖	CompOp	4 math math: `inr_pushoutZeroZeroIso_hom`, `inr_pushoutZeroZeroIso_inv`, `inl_pushoutZeroZeroIso_inv`, `inl_pushoutZeroZeroIso_hom`
`zeroCoprodIso` 📖	CompOp	2 math math: `inr_zeroCoprodIso_hom`, `zeroCoprodIso_inv`
`zeroProdIso` 📖	CompOp	2 math math: `zeroProdIso_hom`, `zeroProdIso_inv_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprodZeroIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `coprod` `HasZeroObject.zero'` `hasBinaryCoproduct_zero_right` `coprodZeroIso` `coprod.inl`	—	`hasBinaryCoproduct_zero_right`
`hasBinaryCoproduct_zero_left` 📖	mathematical	—	`HasBinaryCoproduct` `HasZeroObject.zero'`	—	—
`hasBinaryCoproduct_zero_right` 📖	mathematical	—	`HasBinaryCoproduct` `HasZeroObject.zero'`	—	—
`hasBinaryProduct_zero_left` 📖	mathematical	—	`HasBinaryProduct` `HasZeroObject.zero'`	—	—
`hasBinaryProduct_zero_right` 📖	mathematical	—	`HasBinaryProduct` `HasZeroObject.zero'`	—	—
`hasPullback_over_zero` 📖	mathematical	—	`HasPullback` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HasZeroMorphisms.zero`	—	`IsTerminal.hom_ext`
`hasPushout_over_zero` 📖	mathematical	—	`HasPushout` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HasZeroMorphisms.zero`	—	`IsInitial.hom_ext`
`inl_pushoutZeroZeroIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPushout_over_zero` `coprod` `pushout.inl` `CategoryTheory.Iso.hom` `pushoutZeroZeroIso` `coprod.inl`	—	`hasPushout_over_zero` `colimit.isoColimitCocone_ι_hom`
`inl_pushoutZeroZeroIso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `coprod` `pushout` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPushout_over_zero` `coprod.inl` `CategoryTheory.Iso.inv` `pushoutZeroZeroIso` `pushout.inl`	—	`hasPushout_over_zero` `inl_pushoutZeroZeroIso_hom`
`inr_coprodZeroIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `coprod` `HasZeroObject.zero'` `hasBinaryCoproduct_zero_right` `coprod.inl` `CategoryTheory.Iso.hom` `coprodZeroIso` `CategoryTheory.CategoryStruct.id`	—	`hasBinaryCoproduct_zero_right` `colimit.isoColimitCocone_ι_hom`
`inr_pushoutZeroZeroIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPushout_over_zero` `coprod` `pushout.inr` `CategoryTheory.Iso.hom` `pushoutZeroZeroIso` `coprod.inr`	—	`hasPushout_over_zero` `colimit.isoColimitCocone_ι_hom`
`inr_pushoutZeroZeroIso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `coprod` `pushout` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPushout_over_zero` `coprod.inr` `CategoryTheory.Iso.inv` `pushoutZeroZeroIso` `pushout.inr`	—	`hasPushout_over_zero` `inr_pushoutZeroZeroIso_hom`
`inr_zeroCoprodIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `coprod` `HasZeroObject.zero'` `hasBinaryCoproduct_zero_left` `coprod.inr` `CategoryTheory.Iso.hom` `zeroCoprodIso` `CategoryTheory.CategoryStruct.id`	—	`hasBinaryCoproduct_zero_left` `colimit.isoColimitCocone_ι_hom`
`prodZeroIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `prod` `HasZeroObject.zero'` `hasBinaryProduct_zero_right` `prodZeroIso` `prod.fst`	—	`hasBinaryProduct_zero_right`
`prodZeroIso_iso_inv_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `prod` `HasZeroObject.zero'` `hasBinaryProduct_zero_right` `CategoryTheory.Iso.inv` `prodZeroIso` `prod.fst` `CategoryTheory.CategoryStruct.id`	—	`hasBinaryProduct_zero_right` `limit.isoLimitCone_inv_π`
`pullbackZeroZeroIso_hom_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPullback_over_zero` `prod` `CategoryTheory.Iso.hom` `pullbackZeroZeroIso` `prod.fst` `pullback.fst`	—	`hasPullback_over_zero` `pullbackZeroZeroIso_inv_fst`
`pullbackZeroZeroIso_hom_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPullback_over_zero` `prod` `CategoryTheory.Iso.hom` `pullbackZeroZeroIso` `prod.snd` `pullback.snd`	—	`hasPullback_over_zero` `pullbackZeroZeroIso_inv_snd`
`pullbackZeroZeroIso_inv_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `prod` `pullback` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPullback_over_zero` `CategoryTheory.Iso.inv` `pullbackZeroZeroIso` `pullback.fst` `prod.fst`	—	`hasPullback_over_zero` `limit.isoLimitCone_inv_π`
`pullbackZeroZeroIso_inv_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `prod` `pullback` `HasZeroObject.zero'` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HasZeroMorphisms.zero` `hasPullback_over_zero` `CategoryTheory.Iso.inv` `pullbackZeroZeroIso` `pullback.snd` `prod.snd`	—	`hasPullback_over_zero` `limit.isoLimitCone_inv_π`
`zeroCoprodIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `coprod` `HasZeroObject.zero'` `hasBinaryCoproduct_zero_left` `zeroCoprodIso` `coprod.inr`	—	`hasBinaryCoproduct_zero_left`
`zeroProdIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `prod` `HasZeroObject.zero'` `hasBinaryProduct_zero_left` `zeroProdIso` `prod.snd`	—	`hasBinaryProduct_zero_left`
`zeroProdIso_inv_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `prod` `HasZeroObject.zero'` `hasBinaryProduct_zero_left` `CategoryTheory.Iso.inv` `zeroProdIso` `prod.snd` `CategoryTheory.CategoryStruct.id`	—	`hasBinaryProduct_zero_left` `limit.isoLimitCone_inv_π`

---

← Back to Index