Limits

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

Statistics

Metric	Count
Definitions limitCone, limitConeIsLimit, addCommGroupObj, directLimitCocone, directLimitDiagram, directLimitIsColimit, forget₂AddCommGroup_preservesLimitsAux, instAddCommMonoidElemForallObjCompForgetLinearMapIdCarrierSections, instModuleElemForallObjCompForgetLinearMapIdCarrierSections, limitAddCommGroup, limitAddCommMonoid, limitModule, limitπLinearMap, moduleObj, sectionsSubmodule	15
Theorems directLimitCocone_pt_carrier, directLimitCocone_pt_isAddCommGroup, directLimitCocone_pt_isModule, directLimitCocone_ι_app, directLimitDiagram_map, directLimitDiagram_obj_carrier, directLimitDiagram_obj_isAddCommGroup, directLimitDiagram_obj_isModule, directLimitIsColimit_desc, forget_preservesLimits, forget_preservesLimitsOfSize, forget₂AddCommGroup_preservesLimit, forget₂AddCommGroup_preservesLimits, forget₂AddCommGroup_preservesLimitsOfSize, forget₂AddCommGroup_reflectsLimit, forget₂AddCommGroup_reflectsLimitOfShape, forget₂AddCommGroup_reflectsLimitOfSize, hasLimit, hasLimits, hasLimits', hasLimitsOfShape, hasLimitsOfSize, instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule	23
Total	38

ModuleCat

Definitions

Name	Category	Theorems
addCommGroupObj 📖	CompOp	—
directLimitCocone 📖	CompOp	5 math math: directLimitCocone_pt_carrier, directLimitIsColimit_desc, directLimitCocone_pt_isAddCommGroup, directLimitCocone_ι_app, directLimitCocone_pt_isModule
directLimitDiagram 📖	CompOp	9 math math: directLimitDiagram_obj_isModule, directLimitCocone_pt_carrier, directLimitIsColimit_desc, directLimitCocone_pt_isAddCommGroup, directLimitDiagram_obj_isAddCommGroup, directLimitDiagram_obj_carrier, directLimitCocone_ι_app, directLimitCocone_pt_isModule, directLimitDiagram_map
directLimitIsColimit 📖	CompOp	1 math math: directLimitIsColimit_desc
forget₂AddCommGroup_preservesLimitsAux 📖	CompOp	—
instAddCommMonoidElemForallObjCompForgetLinearMapIdCarrierSections 📖	CompOp	—
instModuleElemForallObjCompForgetLinearMapIdCarrierSections 📖	CompOp	—
limitAddCommGroup 📖	CompOp	—
limitAddCommMonoid 📖	CompOp	—
limitModule 📖	CompOp	—
limitπLinearMap 📖	CompOp	—
moduleObj 📖	CompOp	—
sectionsSubmodule 📖	CompOp	1 math math: instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directLimitCocone_pt_carrier 📖	mathematical	—	carrier CategoryTheory.Limits.Cocone.pt Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram directLimitCocone Module.DirectLimit Ring.toSemiring AddCommGroup.toAddCommMonoid	—	—
directLimitCocone_pt_isAddCommGroup 📖	mathematical	—	isAddCommGroup CategoryTheory.Limits.Cocone.pt Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram directLimitCocone Module.DirectLimit.addCommGroup Ring.toSemiring	—	—
directLimitCocone_pt_isModule 📖	mathematical	—	isModule CategoryTheory.Limits.Cocone.pt Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram directLimitCocone Module.DirectLimit.module Ring.toSemiring AddCommGroup.toAddCommMonoid	—	—
directLimitCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const of Module.DirectLimit Ring.toSemiring AddCommGroup.toAddCommMonoid Module.DirectLimit.addCommGroup Module.DirectLimit.module CategoryTheory.Limits.Cocone.ι directLimitCocone ofHom Module.DirectLimit.of	—	—
directLimitDiagram_map 📖	mathematical	—	CategoryTheory.Functor.map Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram ofHom Quiver.Hom.le	—	—
directLimitDiagram_obj_carrier 📖	mathematical	—	carrier CategoryTheory.Functor.obj Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram	—	—
directLimitDiagram_obj_isAddCommGroup 📖	mathematical	—	isAddCommGroup CategoryTheory.Functor.obj Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram	—	—
directLimitDiagram_obj_isModule 📖	mathematical	—	isModule CategoryTheory.Functor.obj Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram	—	—
directLimitIsColimit_desc 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc Preorder.smallCategory ModuleCat moduleCategory directLimitDiagram directLimitCocone directLimitIsColimit ofHom Module.DirectLimit Ring.toSemiring AddCommGroup.toAddCommMonoid carrier Module.DirectLimit.addCommGroup Module.DirectLimit.module isAddCommGroup isModule Module.DirectLimit.lift Hom.hom CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	—
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits ModuleCat moduleCategory CategoryTheory.types CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier	—	forget_preservesLimitsOfSize univLE_of_max UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize ModuleCat moduleCategory CategoryTheory.types CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget₂AddCommGroup_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
forget₂AddCommGroup_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	forget₂AddCommGroup_preservesLimitsOfSize univLE_of_max UnivLE.self
forget₂AddCommGroup_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	forget₂AddCommGroup_preservesLimit small_subtype small_Pi UnivLE.small UnivLE.self
forget₂AddCommGroup_reflectsLimit 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimit ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier hasLimit forget₂AddCommGroup_preservesLimit
forget₂AddCommGroup_reflectsLimitOfShape 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfShape ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	forget₂AddCommGroup_reflectsLimit
forget₂AddCommGroup_reflectsLimitOfSize 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfSize ModuleCat moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	forget₂AddCommGroup_reflectsLimitOfShape
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit ModuleCat moduleCategory	—	—
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits ModuleCat moduleCategory	—	hasLimitsOfSize UnivLE.self
hasLimits' 📖	mathematical	—	CategoryTheory.Limits.HasLimits ModuleCat moduleCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape ModuleCat moduleCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize ModuleCat moduleCategory	—	hasLimitsOfShape UnivLE.small
instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule 📖	mathematical	—	Small Submodule Ring.toSemiring Pi.addCommMonoid carrier CategoryTheory.Functor.obj ModuleCat moduleCategory AddCommGroup.toAddCommMonoid isAddCommGroup Pi.module isModule SetLike.instMembership Submodule.setLike sectionsSubmodule	—	—

ModuleCat.HasLimits

Definitions

Name	Category	Theorems
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—

---

← Back to Index