Basic

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

Statistics

Metric	Count
Definitions IsGrothendieckAbelian	1
Theorems ab4OfSize, ab5OfSize, hasColimits, hasFilteredColimitsOfSize, hasLimits, hasSeparator, locallySmall, of_equivalence, wellPowered, isGrothendieckAbelian	10
Total	11

CategoryTheory

Definitions

Name	Category	Theorems
IsGrothendieckAbelian 📖	CompData	8 math math: ShrinkHoms.isGrothendieckAbelian, Sheaf.instIsGrothendieckAbelian, Sheaf.isGrothendieckAbelian_of_essentiallySmall, Limits.isGrothendieckAbelian_ind, HomologicalComplex.isGrothendieckAbelian, IsGrothendieckAbelian.of_equivalence, instIsGrothendieckAbelianModuleCat, LightCondensed.instIsGrothendieckAbelianLightCondMod

CategoryTheory.IsGrothendieckAbelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ab4OfSize 📖	mathematical	—	CategoryTheory.AB4OfSize CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Discrete CategoryTheory.discreteCategory hasColimits	—	CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts CategoryTheory.Limits.hasFiniteProducts_of_hasCountableProducts CategoryTheory.Limits.hasCountableProducts_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits hasLimits CategoryTheory.AB4.of_AB5 CategoryTheory.Abelian.hasFiniteLimits hasFilteredColimitsOfSize ab5OfSize
ab5OfSize 📖	mathematical	—	CategoryTheory.AB5OfSize hasFilteredColimitsOfSize	—	—
hasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize	—	CategoryTheory.Limits.has_colimits_of_finite_and_filtered CategoryTheory.Abelian.hasFiniteColimits hasFilteredColimitsOfSize
hasFilteredColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasFilteredColimitsOfSize	—	—
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize	—	locallySmall CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator hasColimits CategoryTheory.ShrinkHoms.isGrothendieckAbelian hasSeparator CategoryTheory.Abelian.wellPowered_opposite CategoryTheory.HasSeparator.wellPowered CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.ShrinkHoms.hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Adjunction.has_limits_of_equivalence CategoryTheory.Equivalence.isEquivalence_functor
hasSeparator 📖	mathematical	—	CategoryTheory.HasSeparator	—	—
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall	—	—
of_equivalence 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian	—	CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits hasFilteredColimitsOfSize CategoryTheory.locallySmall_of_faithful CategoryTheory.Equivalence.faithful_inverse locallySmall CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence CategoryTheory.AB5OfSize.ofShape ab5OfSize CategoryTheory.HasSeparator.of_equivalence hasSeparator
wellPowered 📖	mathematical	—	CategoryTheory.WellPowered locallySmall	—	CategoryTheory.wellPowered_of_equiv locallySmall CategoryTheory.ShrinkHoms.isGrothendieckAbelian CategoryTheory.HasSeparator.wellPowered CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.ShrinkHoms.hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory hasSeparator

CategoryTheory.ShrinkHoms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGrothendieckAbelian 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian CategoryTheory.ShrinkHoms instCategory CategoryTheory.IsGrothendieckAbelian.locallySmall abelian	—	CategoryTheory.IsGrothendieckAbelian.of_equivalence CategoryTheory.IsGrothendieckAbelian.locallySmall

---

← Back to Index