Limits

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

Statistics

Metric	Count
Definitions forgetMapConeLimitConeIso, instCreatesLimitForget, instCreatesLimitsForget, instCreatesLimitsOfShapeForget, instCreatesLimitsOfSizeForget, limit, limitCone, limitConeIsLimit, limitConeLiftsToLimit	9
Theorems forgetMapConeLimitConeIso_hom_hom, forgetMapConeLimitConeIso_inv_hom, instHasLimitsOfShape, instPreservesLimitsOfShapeForgetOfHasLimitsOfShape, limitConeIsLimit_lift_hom, limitCone_pt, limitCone_π_app_hom, limit_X, limit_mon_mul, limit_mon_one	10
Total	19

CategoryTheory.Mon

Definitions

Name	Category	Theorems
forgetMapConeLimitConeIso 📖	CompOp	2 math math: forgetMapConeLimitConeIso_inv_hom, forgetMapConeLimitConeIso_hom_hom
instCreatesLimitForget 📖	CompOp	—
instCreatesLimitsForget 📖	CompOp	—
instCreatesLimitsOfShapeForget 📖	CompOp	—
instCreatesLimitsOfSizeForget 📖	CompOp	—
limit 📖	CompOp	5 math math: limit_mon_mul, limitCone_π_app_hom, limit_X, limitCone_pt, limit_mon_one
limitCone 📖	CompOp	5 math math: forgetMapConeLimitConeIso_inv_hom, forgetMapConeLimitConeIso_hom_hom, limitConeIsLimit_lift_hom, limitCone_π_app_hom, limitCone_pt
limitConeIsLimit 📖	CompOp	1 math math: limitConeIsLimit_lift_hom
limitConeLiftsToLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forgetMapConeLimitConeIso_hom_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Mon instCategory forget CategoryTheory.Functor.mapCone limitCone CategoryTheory.Iso.hom CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category forgetMapConeLimitConeIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
forgetMapConeLimitConeIso_inv_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Mon instCategory forget CategoryTheory.Functor.mapCone limitCone CategoryTheory.Iso.inv CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category forgetMapConeLimitConeIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
instHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Mon instCategory	—	CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
instPreservesLimitsOfShapeForgetOfHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Mon instCategory forget	—	CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape
limitConeIsLimit_lift_hom 📖	mathematical	—	Hom.hom CategoryTheory.Limits.Cone.pt CategoryTheory.Mon instCategory limitCone CategoryTheory.Limits.IsLimit.lift limitConeIsLimit 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.Cone.pt CategoryTheory.Functor.comp forget	—	—
limit_X 📖	mathematical	—	X limit CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Mon instCategory forget	—	—
limit_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Mon instCategory forget mon limit CategoryTheory.Limits.IsLimit.lift CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	—
limit_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Mon instCategory forget mon limit CategoryTheory.Limits.IsLimit.lift CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const X	—	—

---

← Back to Index