Documentation Verification Report

ContainsZero

📁 Source: Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean

Statistics

Metric	Count
Definitions `kernel`, `ContainsZero`	2
Theorems `exists_zero`, `exists_prop_of_containsZero`, `instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject`, `instContainsZeroIsZeroOfHasZeroObject`, `instContainsZeroIsoClosure`, `instContainsZeroMapOfPreservesZeroMorphisms`, `instContainsZeroMinOfIsClosedUnderIsomorphisms`, `instContainsZeroOppositeOp`, `instContainsZeroTopOfHasZeroObject`, `instContainsZeroUnopOfOpposite`, `instHasZeroObjectFullSubcategoryOfContainsZero`, `prop_of_isZero`, `prop_zero`	13
Total	15

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`kernel` 📖	CompOp	6 math math: `CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff`, `CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint`, `CategoryTheory.Abelian.isoModSerre_kernel_eq_leftBousfield_W_of_rightAdjoint`, `CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint`, `CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy`, `CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms`

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`ContainsZero` 📖	CompData	14 math math: `instContainsZeroRightOrthogonalOfHasZeroObject`, `IsTriangulated.toContainsZero`, `instContainsZeroOppositeOp`, `IsSerreClass.toContainsZero`, `CategoryTheory.instContainsZeroIsArtinianObjectOfHasZeroObject`, `instContainsZeroTopOfHasZeroObject`, `instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject`, `CategoryTheory.instContainsZeroIsNoetherianObjectOfHasZeroObject`, `instContainsZeroIsoClosure`, `instContainsZeroMinOfIsClosedUnderIsomorphisms`, `instContainsZeroMapOfPreservesZeroMorphisms`, `instContainsZeroLeftOrthogonalOfHasZeroObject`, `instContainsZeroIsZeroOfHasZeroObject`, `instContainsZeroUnopOfOpposite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_prop_of_containsZero` 📖	mathematical	—	`CategoryTheory.Limits.IsZero`	—	`ContainsZero.exists_zero`
`instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject` 📖	mathematical	—	`ContainsZero` `inverseImage`	—	`CategoryTheory.Limits.isZero_zero` `prop_of_isZero` `CategoryTheory.Functor.map_isZero`
`instContainsZeroIsZeroOfHasZeroObject` 📖	mathematical	—	`ContainsZero` `CategoryTheory.Limits.IsZero`	—	`CategoryTheory.Limits.isZero_zero`
`instContainsZeroIsoClosure` 📖	mathematical	—	`ContainsZero` `isoClosure`	—	`exists_prop_of_containsZero` `le_isoClosure`
`instContainsZeroMapOfPreservesZeroMorphisms` 📖	mathematical	—	`ContainsZero` `map`	—	`exists_prop_of_containsZero` `CategoryTheory.Functor.map_isZero` `prop_map_obj`
`instContainsZeroMinOfIsClosedUnderIsomorphisms` 📖	mathematical	—	`ContainsZero` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	`exists_prop_of_containsZero` `prop_of_isZero`
`instContainsZeroOppositeOp` 📖	mathematical	—	`ContainsZero` `Opposite` `CategoryTheory.Category.opposite` `op` `CategoryTheory.Category.toCategoryStruct`	—	`exists_prop_of_containsZero` `CategoryTheory.Limits.IsZero.op`
`instContainsZeroTopOfHasZeroObject` 📖	mathematical	—	`ContainsZero` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`CategoryTheory.Limits.isZero_zero`
`instContainsZeroUnopOfOpposite` 📖	mathematical	—	`ContainsZero` `unop` `CategoryTheory.Category.toCategoryStruct`	—	`exists_prop_of_containsZero` `CategoryTheory.Limits.IsZero.unop`
`instHasZeroObjectFullSubcategoryOfContainsZero` 📖	mathematical	—	`CategoryTheory.Limits.HasZeroObject` `FullSubcategory` `FullSubcategory.category`	—	`exists_prop_of_containsZero` `CategoryTheory.Limits.IsZero.of_full_of_faithful_of_isZero` `full_ι` `faithful_ι`
`prop_of_isZero` 📖	—	`CategoryTheory.Limits.IsZero`	—	—	`exists_prop_of_containsZero` `prop_of_iso`
`prop_zero` 📖	mathematical	—	`CategoryTheory.Limits.HasZeroObject.zero'`	—	`prop_of_isZero` `CategoryTheory.Limits.isZero_zero`

CategoryTheory.ObjectProperty.ContainsZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_zero` 📖	mathematical	—	`CategoryTheory.Limits.IsZero`	—	—

---

← Back to Index