Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/Abelian/SerreClass/Basic.lean

Statistics

Metric	Count
Definitions `IsSerreClass`	1
Theorems `toContainsZero`, `toIsClosedUnderExtensions`, `toIsClosedUnderQuotients`, `toIsClosedUnderSubobjects`, `instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits`, `instIsSerreClassIsZero`, `instIsSerreClassTop`, `prop_X₂_of_exact`, `prop_iff_of_shortExact`	9
Total	10

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsSerreClass` 📖	CompData	4 math math: `instIsSerreClassIsZero`, `instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits`, `instIsSerreClassTop`, `AddCommGrpCat.instIsSerreClassIsFinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits` 📖	mathematical	—	`IsSerreClass` `inverseImage`	—	`instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject` `IsSerreClass.toContainsZero` `instIsClosedUnderIsomorphisms_1` `IsSerreClass.toIsClosedUnderQuotients` `CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `instIsClosedUnderSubobjectsInverseImageOfPreservesMonomorphisms` `IsSerreClass.toIsClosedUnderSubobjects` `CategoryTheory.Functor.instPreservesMonomorphisms` `CategoryTheory.Functor.preservesHomologyOfExact` `instIsClosedUnderQuotientsInverseImageOfPreservesEpimorphisms` `CategoryTheory.Functor.instPreservesEpimorphisms` `instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits` `IsSerreClass.toIsClosedUnderExtensions`
`instIsSerreClassIsZero` 📖	mathematical	—	`IsSerreClass` `CategoryTheory.Limits.IsZero`	—	`instContainsZeroIsZeroOfHasZeroObject` `CategoryTheory.Abelian.hasZeroObject` `instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms` `instIsClosedUnderQuotientsIsZeroOfHasZeroMorphisms` `instIsClosedUnderExtensionsIsZero`
`instIsSerreClassTop` 📖	mathematical	—	`IsSerreClass` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`instContainsZeroTopOfHasZeroObject` `CategoryTheory.Abelian.hasZeroObject` `instIsClosedUnderSubobjectsTop` `instIsClosedUnderQuotientsTop` `instIsClosedUnderExtensionsTop`
`prop_X₂_of_exact` 📖	mathematical	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₃`	`CategoryTheory.ShortComplex.X₂`	—	`CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.ShortComplex.Exact.epi_f'` `CategoryTheory.ShortComplex.Exact.mono_g'` `prop_X₂_of_shortExact` `IsSerreClass.toIsClosedUnderExtensions` `CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero` `CategoryTheory.ShortComplex.Exact.shortExact` `prop_of_epi` `IsSerreClass.toIsClosedUnderQuotients` `prop_of_mono` `IsSerreClass.toIsClosedUnderSubobjects`
`prop_iff_of_shortExact` 📖	mathematical	`CategoryTheory.ShortComplex.ShortExact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	`CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.ShortComplex.X₃`	—	`prop_X₁_of_shortExact` `IsSerreClass.toIsClosedUnderSubobjects` `prop_X₃_of_shortExact` `IsSerreClass.toIsClosedUnderQuotients` `prop_X₂_of_shortExact` `IsSerreClass.toIsClosedUnderExtensions`

CategoryTheory.ObjectProperty.IsSerreClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toContainsZero` 📖	mathematical	—	`CategoryTheory.ObjectProperty.ContainsZero`	—	—
`toIsClosedUnderExtensions` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderExtensions` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	—
`toIsClosedUnderQuotients` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderQuotients`	—	—
`toIsClosedUnderSubobjects` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderSubobjects`	—	—

---

← Back to Index