Limits

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

Statistics

Metric	Count
Definitions addCommMonoidObj, forget_createsLimit, forget_createsLimits, forget_createsLimitsOfShape, forget_createsLimitsOfSize, forget₂CreatesLimit, limitAddCommMonoid, limitCone, limitConeIsLimit, limitCone, limitConeIsLimit, addMonoidObj, forget_createsLimit, forget_createsLimits, forget_createsLimitsOfShape, forget_createsLimitsOfSize, limitAddMonoid, limitπAddMonoidHom, sectionsAddMonoid, sectionsAddSubmonoid, commMonoidObj, forget_createsLimit, forget_createsLimits, forget_createsLimitsOfShape, forget_createsLimitsOfSize, forget₂CreatesLimit, limitCommMonoid, limitCone, limitConeIsLimit, limitCone, limitConeIsLimit, forget_createsLimit, forget_createsLimits, forget_createsLimitsOfShape, forget_createsLimitsOfSize, limitMonoid, limitπMonoidHom, monoidObj, sectionsMonoid, sectionsSubmonoid	40
Theorems forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, forget₂AddMonPreservesLimitsOfSize, forget₂Mon_preservesLimits, hasLimit, hasLimits, hasLimitsOfShape, hasLimitsOfSize, instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections, hasLimit, hasLimitsOfShape, forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, hasLimits, hasLimitsOfSize, forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, forget₂Mon_preservesLimits, forget₂Mon_preservesLimitsOfSize, hasLimit, hasLimits, hasLimitsOfShape, hasLimitsOfSize, instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, hasLimit, hasLimitsOfShape, forget_preservesLimits, forget_preservesLimitsOfShape, forget_preservesLimitsOfSize, hasLimits, hasLimitsOfSize	34
Total	74

AddCommMonCat

Definitions

Name	Category	Theorems
addCommMonoidObj 📖	CompOp	—
forget_createsLimit 📖	CompOp	—
forget_createsLimits 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
forget₂CreatesLimit 📖	CompOp	—
limitAddCommMonoid 📖	CompOp	—
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AddCommMonCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	forget_preservesLimitsOfSize UnivLE.self
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddCommMonCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddCommMonCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit forget_preservesLimitsOfShape UnivLE.small
forget₂AddMonPreservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddCommMonCat instCategory AddMonCat AddMonCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddMonCat.carrier AddMonCat.str AddMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddMonCat	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit small_subtype small_Pi UnivLE.small UnivLE.self AddMonCat.HasLimits.hasLimit instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections
forget₂Mon_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AddCommMonCat instCategory AddMonCat AddMonCat.instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddMonCat.carrier AddMonCat.str AddMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddMonCat	—	forget₂AddMonPreservesLimitsOfSize UnivLE.self
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit AddCommMonCat instCategory	—	—
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits AddCommMonCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape AddCommMonCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize AddCommMonCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections 📖	mathematical	—	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp AddMonCat AddMonCat.instCategory CategoryTheory.types AddCommMonCat instCategory CategoryTheory.forget₂ AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier AddMonCat.carrier AddMonCat.str AddMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddMonCat CategoryTheory.forget	—	—

AddMonCat

Definitions

Name	Category	Theorems
addMonoidObj 📖	CompOp	—
forget_createsLimit 📖	CompOp	—
forget_createsLimits 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
limitAddMonoid 📖	CompOp	—
limitπAddMonoidHom 📖	CompOp	—
sectionsAddMonoid 📖	CompOp	—
sectionsAddSubmonoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits AddMonCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	forget_preservesLimitsOfSize UnivLE.self
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape AddMonCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize AddMonCat instCategory CategoryTheory.types CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit forget_preservesLimitsOfShape UnivLE.small
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits AddMonCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize AddMonCat instCategory	—	HasLimits.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self

AddMonCat.HasLimits

Definitions

Name	Category	Theorems
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit AddMonCat AddMonCat.instCategory	—	—
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape AddMonCat AddMonCat.instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self

CommMonCat

Definitions

Name	Category	Theorems
commMonoidObj 📖	CompOp	—
forget_createsLimit 📖	CompOp	—
forget_createsLimits 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
forget₂CreatesLimit 📖	CompOp	—
limitCommMonoid 📖	CompOp	—
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits CommMonCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	forget_preservesLimitsOfSize UnivLE.self
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CommMonCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CommMonCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit forget_preservesLimitsOfShape UnivLE.small
forget₂Mon_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits CommMonCat instCategory MonCat MonCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier hasForgetToMonCat	—	forget₂Mon_preservesLimitsOfSize UnivLE.self
forget₂Mon_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CommMonCat instCategory MonCat MonCat.instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier hasForgetToMonCat	—	CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit small_subtype small_Pi UnivLE.small UnivLE.self MonCat.HasLimits.hasLimit instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit CommMonCat instCategory	—	—
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CommMonCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CommMonCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CommMonCat instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections 📖	mathematical	—	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp MonCat MonCat.instCategory CategoryTheory.types CommMonCat instCategory CategoryTheory.forget₂ MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier hasForgetToMonCat CategoryTheory.forget	—	—

MonCat

Definitions

Name	Category	Theorems
forget_createsLimit 📖	CompOp	—
forget_createsLimits 📖	CompOp	—
forget_createsLimitsOfShape 📖	CompOp	—
forget_createsLimitsOfSize 📖	CompOp	—
limitMonoid 📖	CompOp	—
limitπMonoidHom 📖	CompOp	—
monoidObj 📖	CompOp	2 math math: CategoryTheory.MonObj.ofRepresentableBy_one, CategoryTheory.MonObj.ofRepresentableBy_mul
sectionsMonoid 📖	CompOp	—
sectionsSubmonoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits MonCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	forget_preservesLimitsOfSize UnivLE.self
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape MonCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone small_subtype small_Pi UnivLE.small UnivLE.self
forget_preservesLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize MonCat instCategory CategoryTheory.types CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier	—	CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit forget_preservesLimitsOfShape UnivLE.small
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits MonCat instCategory	—	hasLimitsOfSize UnivLE.self
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize MonCat instCategory	—	HasLimits.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self

MonCat.HasLimits

Definitions

Name	Category	Theorems
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit MonCat MonCat.instCategory	—	—
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape MonCat MonCat.instCategory	—	hasLimit small_subtype small_Pi UnivLE.small UnivLE.self

---

← Back to Index