Limits

📁 Source: Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

Statistics

Metric	Count
Definitions forgetMapConeLimitConeIso, limit, limitCone, limitConeIsLimit	4
Theorems forget_preservesLimitsOfShape, hasLimitsOfShape, limitConeIsLimit_lift_hom, limitCone_pt, limitCone_π_app_hom, limit_X, limit_mon_mul, limit_mon_one	8
Total	12

CategoryTheory.Mon

Definitions

Name	Category	Theorems
forgetMapConeLimitConeIso 📖	CompOp	—
limit 📖	CompOp	5 math math: limit_mon_mul, limitCone_π_app_hom, limit_X, limitCone_pt, limit_mon_one
limitCone 📖	CompOp	3 math math: limitConeIsLimit_lift_hom, limitCone_π_app_hom, limitCone_pt
limitConeIsLimit 📖	CompOp	1 math math: limitConeIsLimit_lift_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Mon instCategory forget	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Mon instCategory	—	—
limitConeIsLimit_lift_hom 📖	mathematical	—	Hom.hom CategoryTheory.Limits.Cone.pt CategoryTheory.Mon instCategory limitCone CategoryTheory.Limits.IsLimit.lift limitConeIsLimit CategoryTheory.Limits.limit.lift CategoryTheory.Functor.comp forget CategoryTheory.Functor.mapCone	—	—
limitCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Mon instCategory limitCone limit	—	—
limitCone_π_app_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj CategoryTheory.Mon instCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const limit CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π limitCone CategoryTheory.Limits.limit.π CategoryTheory.Functor.comp forget	—	—
limit_X 📖	mathematical	—	X limit CategoryTheory.Limits.limit CategoryTheory.Functor.comp CategoryTheory.Mon instCategory forget CategoryTheory.Limits.hasLimitOfHasLimitsOfShape	—	—
limit_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.lim X CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Mon instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Monoidal.monFunctorCategoryEquivalence mon limit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.limit CategoryTheory.Functor.comp forget CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.instLaxMonoidalFunctorLim CategoryTheory.Limits.limMap CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj	—	—
limit_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.lim X CategoryTheory.Monoidal.functorCategoryMonoidal CategoryTheory.Mon instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Monoidal.monFunctorCategoryEquivalence mon limit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.limit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.comp forget CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.instLaxMonoidalFunctorLim CategoryTheory.Limits.limMap CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj	—	—

---

← Back to Index