AB

📁 Source: Mathlib/Condensed/Light/AB.lean

Statistics

Metric	Count
Definitions	0
Theorems instCountableAB4StarLightCondMod, instIsGrothendieckAbelianLightCondMod	2
Total	2

LightCondensed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountableAB4StarLightCondMod 📖	mathematical	—	CategoryTheory.CountableAB4Star LightCondMod instCategoryLightCondensed ModuleCat ModuleCat.moduleCategory CategoryTheory.Limits.hasCountableProducts_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Discrete CategoryTheory.discreteCategory instHasLimitsOfSizeLightCondMod	—	CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable CategoryTheory.Limits.hasCountableProducts_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits instHasLimitsOfSizeLightCondMod instCountableNat CategoryTheory.hasExactLimitsOfShape_of_preservesEpi instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat CategoryTheory.Abelian.hasFiniteBiproducts CategoryTheory.Abelian.hasFiniteColimits
instIsGrothendieckAbelianLightCondMod 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian LightCondMod instCategoryLightCondensed ModuleCat ModuleCat.moduleCategory instAbelianLightCondMod	—	CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall instEssentiallySmallLightProfinite instIsGrothendieckAbelianModuleCat CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.forget_preservesLimits CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits ModuleCat.hasLimits'

---

← Back to Index