GrothendieckAbelian

📁 Source: Mathlib/Algebra/Homology/GrothendieckAbelian.lean

Statistics

Metric	Count
Definitions	0
Theorems ab5OfSize, hasExactColimitsOfShape, instHasFilteredColimitsOfSize, isGrothendieckAbelian, locallySmall	5
Total	5

HomologicalComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ab5OfSize 📖	mathematical	—	CategoryTheory.AB5OfSize HomologicalComplex instCategory instHasFilteredColimitsOfSize	—	instHasFilteredColimitsOfSize CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits hasExactColimitsOfShape CategoryTheory.AB5OfSize.ofShape
hasExactColimitsOfShape 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape HomologicalComplex instCategory instHasColimitsOfShape	—	instHasColimitsOfShape instPreservesColimitsOfShapeEvalOfHasColimitsOfShape CategoryTheory.Limits.comp_preservesLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.whiskeringRight_preservesLimitsOfShape instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits instPreservesLimitsOfShapeEvalOfHasLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits CategoryTheory.NatIso.naturality_2
instHasFilteredColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasFilteredColimitsOfSize HomologicalComplex instCategory	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits
isGrothendieckAbelian 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instAbelian	—	locallySmall CategoryTheory.IsGrothendieckAbelian.locallySmall instHasFilteredColimitsOfSize CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize ab5OfSize CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.IsGrothendieckAbelian.ab5OfSize CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.IsGrothendieckAbelian.hasColimits instHasSeparator CategoryTheory.Abelian.hasZeroObject CategoryTheory.IsGrothendieckAbelian.hasSeparator
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall HomologicalComplex instCategory	—	CategoryTheory.instSmallHomOfLocallySmall hom_ext Equiv.surjective EquivLike.toEmbeddingLike small_of_injective small_Pi UnivLE.small univLE_of_max UnivLE.self

---

← Back to Index