AB

📁 Source: Mathlib/Algebra/Category/ModuleCat/AB.lean

Statistics

Metric	Count
Definitions	0
Theorems isSeparator, instAB4ModuleCat, instAB4StarModuleCat, instAB5ModuleCat, instHasSeparatorModuleCatOfSmall, instIsGrothendieckAbelianModuleCat	6
Total	6

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparator 📖	mathematical	—	CategoryTheory.IsSeparator ModuleCat moduleCategory of Shrink Shrink.instAddCommGroup Ring.toAddCommGroup Shrink.instModule Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semiring.toModule	—	hom_ext LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids equivShrink_symm_one one_smul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAB4ModuleCat 📖	mathematical	—	CategoryTheory.AB4 ModuleCat ModuleCat.moduleCategory ModuleCat.hasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory AddCommGrpCat.hasColimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self	—	CategoryTheory.AB4.of_AB5 CategoryTheory.Abelian.hasFiniteBiproducts CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits ModuleCat.hasLimits' CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize UnivLE.self instAB5ModuleCat
instAB4StarModuleCat 📖	mathematical	—	CategoryTheory.AB4Star ModuleCat ModuleCat.moduleCategory CategoryTheory.Limits.hasProductsOfShape_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Discrete CategoryTheory.discreteCategory ModuleCat.hasLimits'	—	CategoryTheory.Limits.hasProductsOfShape_of_hasProducts CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits' CategoryTheory.HasExactLimitsOfShape.domain_of_functor AddCommGrpCat.hasLimitsOfShape CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self instHasExactLimitsOfShapeDiscreteAddCommGrpCat CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax AddCommGrpCat.hasColimitsOfSize univLE_of_max CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier ModuleCat.instHasFiniteColimits CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape ModuleCat.forget₂AddCommGroup_preservesLimits
instAB5ModuleCat 📖	mathematical	—	CategoryTheory.AB5 ModuleCat ModuleCat.moduleCategory CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize UnivLE.self	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize UnivLE.self CategoryTheory.HasExactColimitsOfShape.domain_of_functor CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits AddCommGrpCat.hasColimitsOfShape UnivLE.small CategoryTheory.AB5OfSize.ofShape instHasFilteredColimitsAddCommGrpCat instAB5AddCommGrpCat CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits ModuleCat.forget₂AddCommGroup_preservesLimits CategoryTheory.Limits.reflectsFiniteLimits_of_reflectsIsomorphisms ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits ModuleCat.hasLimits' ModuleCat.forget₂PreservesColimitsOfShape
instHasSeparatorModuleCatOfSmall 📖	mathematical	—	CategoryTheory.HasSeparator ModuleCat ModuleCat.moduleCategory	—	ModuleCat.isSeparator
instIsGrothendieckAbelianModuleCat 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian ModuleCat ModuleCat.moduleCategory ModuleCat.abelian	—	CategoryTheory.locallySmall_of_univLE UnivLE.self CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize instAB5ModuleCat instHasSeparatorModuleCatOfSmall UnivLE.small

---

← Back to Index