Documentation Verification Report

Limits

📁 Source: Mathlib/CategoryTheory/Monad/Limits.lean

Statistics

Metric	Count
Definitions `coconePoint`, `liftedCocone`, `liftedCoconeIsColimit`, `newCocone`, `γ`, `conePoint`, `lambda`, `liftedCone`, `liftedConeIsLimit`, `newCone`, `γ`, `forgetCreatesColimit`, `forgetCreatesLimit`, `forgetCreatesLimits`, `forgetCreatesLimitsOfShape`, `coconePoint`, `lambda`, `liftedCocone`, `liftedCoconeIsColimit`, `newCocone`, `γ`, `conePoint`, `liftedCone`, `liftedConeIsLimit`, `newCone`, `γ`, `forgetCreatesColimit`, `forgetCreatesColimits`, `forgetCreatesColimitsOfShape`, `forgetCreatesLimits`, `comonadicCreatesColimits`, `comonadicCreatesLimitOfPreservesLimit`, `comonadicCreatesLimitsOfPreservesLimits`, `comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape`, `monadicCreatesColimitOfPreservesColimit`, `monadicCreatesColimitsOfPreservesColimits`, `monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape`, `monadicCreatesLimits`	38
Theorems `coconePoint_A`, `coconePoint_a`, `liftedCoconeIsColimit_desc_f`, `liftedCocone_pt`, `liftedCocone_ι_app_f`, `newCocone_ι_app`, `γ_app`, `commuting`, `conePoint_A`, `conePoint_a`, `liftedConeIsLimit_lift_f`, `liftedCone_pt`, `liftedCone_π_app_f`, `newCone_pt`, `newCone_π`, `γ_app`, `forget_creates_limits_of_comonad_preserves`, `hasColimit_of_comp_forget_hasColimit`, `coconePoint_A`, `coconePoint_a`, `commuting`, `liftedCoconeIsColimit_desc_f`, `liftedCocone_pt`, `liftedCocone_ι_app_f`, `newCocone_pt`, `newCocone_ι`, `γ_app`, `conePoint_A`, `conePoint_a`, `liftedConeIsLimit_lift_f`, `liftedCone_pt`, `liftedCone_π_app_f`, `newCone_π_app`, `γ_app`, `forget_creates_colimits_of_monad_preserves`, `hasLimit_of_comp_forget_hasLimit`, `comp_comparison_forget_hasColimit`, `comp_comparison_forget_hasLimit`, `comp_comparison_hasColimit`, `comp_comparison_hasLimit`, `hasColimit_of_coreflective`, `hasColimitsOfShape_of_coreflective`, `hasColimitsOfShape_of_reflective`, `hasColimits_of_coreflective`, `hasColimits_of_reflective`, `hasLimit_of_reflective`, `hasLimitsOfShape_of_coreflective`, `hasLimitsOfShape_of_reflective`, `hasLimits_of_coreflective`, `hasLimits_of_reflective`, `leftAdjoint_preservesTerminal_of_reflective`, `rightAdjoint_preservesInitial_of_coreflective`	52
Total	90

CategoryTheory

Definitions

Name	Category	Theorems
`comonadicCreatesColimits` 📖	CompOp	—
`comonadicCreatesLimitOfPreservesLimit` 📖	CompOp	—
`comonadicCreatesLimitsOfPreservesLimits` 📖	CompOp	—
`comonadicCreatesLimitsOfShapeOfPreservesLimitsOfShape` 📖	CompOp	—
`monadicCreatesColimitOfPreservesColimit` 📖	CompOp	—
`monadicCreatesColimitsOfPreservesColimits` 📖	CompOp	—
`monadicCreatesColimitsOfShapeOfPreservesColimitsOfShape` 📖	CompOp	—
`monadicCreatesLimits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_comparison_forget_hasColimit` 📖	mathematical	—	`Limits.HasColimit` `Functor.comp` `Comonad.Coalgebra` `Adjunction.toComonad` `comonadicRightAdjoint` `comonadicAdjunction` `Comonad.Coalgebra.eilenbergMoore` `Comonad.comparison` `Comonad.forget`	—	—
`comp_comparison_forget_hasLimit` 📖	mathematical	—	`Limits.HasLimit` `Functor.comp` `Monad.Algebra` `Adjunction.toMonad` `monadicLeftAdjoint` `monadicAdjunction` `Monad.Algebra.eilenbergMoore` `Monad.comparison` `Monad.forget`	—	—
`comp_comparison_hasColimit` 📖	mathematical	—	`Limits.HasColimit` `Comonad.Coalgebra` `Adjunction.toComonad` `comonadicRightAdjoint` `comonadicAdjunction` `Comonad.Coalgebra.eilenbergMoore` `Functor.comp` `Comonad.comparison`	—	`Comonad.hasColimit_of_comp_forget_hasColimit` `comp_comparison_forget_hasColimit`
`comp_comparison_hasLimit` 📖	mathematical	—	`Limits.HasLimit` `Monad.Algebra` `Adjunction.toMonad` `monadicLeftAdjoint` `monadicAdjunction` `Monad.Algebra.eilenbergMoore` `Functor.comp` `Monad.comparison`	—	`Monad.hasLimit_of_comp_forget_hasLimit` `comp_comparison_forget_hasLimit`
`hasColimit_of_coreflective` 📖	mathematical	—	`Limits.HasColimit`	—	`hasColimit_of_created`
`hasColimitsOfShape_of_coreflective` 📖	mathematical	—	`Limits.HasColimitsOfShape`	—	`hasColimit_of_coreflective` `Limits.hasColimitOfHasColimitsOfShape`
`hasColimitsOfShape_of_reflective` 📖	mathematical	—	`Limits.HasColimitsOfShape`	—	`Limits.hasColimitOfHasColimitsOfShape` `Limits.PreservesColimitsOfShape.preservesColimit` `Limits.PreservesColimitsOfSize.preservesColimitsOfShape` `Adjunction.leftAdjoint_preservesColimits` `Adjunction.counit_isIso_of_R_fully_faithful` `Reflective.toFull` `Reflective.toFaithful`
`hasColimits_of_coreflective` 📖	mathematical	—	`Limits.HasColimitsOfSize`	—	`hasColimitsOfShape_of_coreflective` `Limits.hasColimitsOfShapeOfHasColimitsOfSize`
`hasColimits_of_reflective` 📖	mathematical	—	`Limits.HasColimitsOfSize`	—	`hasColimitsOfShape_of_reflective` `Limits.hasColimitsOfShapeOfHasColimitsOfSize`
`hasLimit_of_reflective` 📖	mathematical	—	`Limits.HasLimit`	—	`hasLimit_of_created`
`hasLimitsOfShape_of_coreflective` 📖	mathematical	—	`Limits.HasLimitsOfShape`	—	`Limits.hasLimitOfHasLimitsOfShape` `Limits.PreservesLimitsOfShape.preservesLimit` `Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `Adjunction.rightAdjoint_preservesLimits` `Adjunction.unit_isIso_of_L_fully_faithful` `Coreflective.toFull` `Coreflective.toFaithful`
`hasLimitsOfShape_of_reflective` 📖	mathematical	—	`Limits.HasLimitsOfShape`	—	`hasLimit_of_reflective` `Limits.hasLimitOfHasLimitsOfShape`
`hasLimits_of_coreflective` 📖	mathematical	—	`Limits.HasLimitsOfSize`	—	`hasLimitsOfShape_of_coreflective` `Limits.hasLimitsOfShapeOfHasLimits`
`hasLimits_of_reflective` 📖	mathematical	—	`Limits.HasLimitsOfSize`	—	`hasLimitsOfShape_of_reflective` `Limits.hasLimitsOfShapeOfHasLimits`
`leftAdjoint_preservesTerminal_of_reflective` 📖	mathematical	—	`Limits.PreservesLimitsOfShape` `Discrete` `discreteCategory` `monadicLeftAdjoint` `monadicOfReflective`	—	`Limits.preservesLimit_of_iso_diagram` `hasLimit_of_reflective` `Adjunction.instIsIsoAppCounitOfFullOfFaithful` `Reflective.toFull` `Reflective.toFaithful` `preservesLimit_of_createsLimit_and_hasLimit`
`rightAdjoint_preservesInitial_of_coreflective` 📖	mathematical	—	`Limits.PreservesColimitsOfShape` `Discrete` `discreteCategory` `comonadicRightAdjoint` `comonadicOfCoreflective`	—	`Limits.preservesColimit_of_iso_diagram` `hasColimit_of_coreflective` `Adjunction.instIsIsoAppUnitOfFullOfFaithful` `Coreflective.toFull` `Coreflective.toFaithful` `preservesColimit_of_createsColimit_and_hasColimit`

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
`forgetCreatesColimit` 📖	CompOp	—
`forgetCreatesLimit` 📖	CompOp	—
`forgetCreatesLimits` 📖	CompOp	—
`forgetCreatesLimitsOfShape` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_creates_limits_of_comonad_preserves` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `Coalgebra` `Coalgebra.eilenbergMoore`	—	`CategoryTheory.hasLimit_of_created` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit`
`hasColimit_of_comp_forget_hasColimit` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `Coalgebra` `Coalgebra.eilenbergMoore`	—	`CategoryTheory.hasColimit_of_created`

CategoryTheory.Comonad.ForgetCreatesColimits'

Definitions

Name	Category	Theorems
`coconePoint` 📖	CompOp	4 math math: `liftedCocone_pt`, `coconePoint_a`, `coconePoint_A`, `liftedCocone_ι_app_f`
`liftedCocone` 📖	CompOp	3 math math: `liftedCocone_pt`, `liftedCoconeIsColimit_desc_f`, `liftedCocone_ι_app_f`
`liftedCoconeIsColimit` 📖	CompOp	1 math math: `liftedCoconeIsColimit_desc_f`
`newCocone` 📖	CompOp	2 math math: `newCocone_ι_app`, `coconePoint_a`
`γ` 📖	CompOp	1 math math: `γ_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coconePoint_A` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.A` `coconePoint` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget`	—	—
`coconePoint_a` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.a` `coconePoint` `CategoryTheory.Limits.IsColimit.desc` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget` `newCocone`	—	—
`liftedCoconeIsColimit_desc_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `liftedCocone` `CategoryTheory.Limits.IsColimit.desc` `liftedCoconeIsColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.forget` `CategoryTheory.Functor.mapCocone`	—	—
`liftedCocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `liftedCocone` `coconePoint`	—	—
`liftedCocone_ι_app_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `coconePoint` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `liftedCocone` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.forget` `CategoryTheory.Limits.Cocone.pt`	—	—
`newCocone_ι_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.Cocone.ι` `newCocone` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id`
`γ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget` `CategoryTheory.Comonad.toFunctor` `γ` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.Comonad.ForgetCreatesLimits'

Definitions

Name	Category	Theorems
`conePoint` 📖	CompOp	4 math math: `liftedCone_π_app_f`, `conePoint_a`, `conePoint_A`, `liftedCone_pt`
`lambda` 📖	CompOp	2 math math: `conePoint_a`, `commuting`
`liftedCone` 📖	CompOp	3 math math: `liftedCone_π_app_f`, `liftedConeIsLimit_lift_f`, `liftedCone_pt`
`liftedConeIsLimit` 📖	CompOp	1 math math: `liftedConeIsLimit_lift_f`
`newCone` 📖	CompOp	2 math math: `newCone_pt`, `newCone_π`
`γ` 📖	CompOp	2 math math: `γ_app`, `newCone_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commuting` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget` `CategoryTheory.Comonad.toFunctor` `CategoryTheory.Functor.mapCone` `CategoryTheory.Functor.obj` `lambda` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.π` `CategoryTheory.Comonad.Coalgebra.A` `CategoryTheory.Comonad.Coalgebra.a`	—	`CategoryTheory.Limits.IsLimit.fac`
`conePoint_A` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.A` `conePoint` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget`	—	—
`conePoint_a` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.a` `conePoint` `lambda`	—	—
`liftedConeIsLimit_lift_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `liftedCone` `CategoryTheory.Limits.IsLimit.lift` `liftedConeIsLimit` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.forget` `CategoryTheory.Functor.mapCone`	—	—
`liftedCone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `liftedCone` `conePoint`	—	—
`liftedCone_π_app_f` 📖	mathematical	—	`CategoryTheory.Comonad.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `conePoint` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π` `liftedCone` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.forget`	—	—
`newCone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget` `CategoryTheory.Comonad.toFunctor` `newCone`	—	—
`newCone_π` 📖	mathematical	—	`CategoryTheory.Limits.Cone.π` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget` `CategoryTheory.Comonad.toFunctor` `newCone` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `γ`	—	—
`γ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Comonad.Coalgebra` `CategoryTheory.Comonad.Coalgebra.eilenbergMoore` `CategoryTheory.Comonad.forget` `CategoryTheory.Comonad.toFunctor` `γ` `CategoryTheory.Comonad.Coalgebra.a` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.Monad

Definitions

Name	Category	Theorems
`forgetCreatesColimit` 📖	CompOp	—
`forgetCreatesColimits` 📖	CompOp	—
`forgetCreatesColimitsOfShape` 📖	CompOp	—
`forgetCreatesLimits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_creates_colimits_of_monad_preserves` 📖	mathematical	—	`CategoryTheory.Limits.HasColimit` `Algebra` `Algebra.eilenbergMoore`	—	`CategoryTheory.hasColimit_of_created` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit`
`hasLimit_of_comp_forget_hasLimit` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `Algebra` `Algebra.eilenbergMoore`	—	`CategoryTheory.hasLimit_of_created`

CategoryTheory.Monad.ForgetCreatesColimits

Definitions

Name	Category	Theorems
`coconePoint` 📖	CompOp	4 math math: `coconePoint_a`, `liftedCocone_pt`, `coconePoint_A`, `liftedCocone_ι_app_f`
`lambda` 📖	CompOp	2 math math: `commuting`, `coconePoint_a`
`liftedCocone` 📖	CompOp	3 math math: `liftedCocone_pt`, `liftedCocone_ι_app_f`, `liftedCoconeIsColimit_desc_f`
`liftedCoconeIsColimit` 📖	CompOp	1 math math: `liftedCoconeIsColimit_desc_f`
`newCocone` 📖	CompOp	2 math math: `newCocone_pt`, `newCocone_ι`
`γ` 📖	CompOp	2 math math: `γ_app`, `newCocone_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coconePoint_A` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.A` `coconePoint` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget`	—	—
`coconePoint_a` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.a` `coconePoint` `lambda`	—	—
`commuting` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.toFunctor` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `lambda` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.Monad.Algebra.a`	—	`CategoryTheory.Limits.IsColimit.fac`
`liftedCoconeIsColimit_desc_f` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.Hom.f` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `liftedCocone` `CategoryTheory.Limits.IsColimit.desc` `liftedCoconeIsColimit` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.forget` `CategoryTheory.Functor.mapCocone`	—	—
`liftedCocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `liftedCocone` `coconePoint`	—	—
`liftedCocone_ι_app_f` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `coconePoint` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cocone.ι` `liftedCocone` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.forget` `CategoryTheory.Limits.Cocone.pt`	—	—
`newCocone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget` `CategoryTheory.Monad.toFunctor` `newCocone`	—	—
`newCocone_ι` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.ι` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget` `CategoryTheory.Monad.toFunctor` `newCocone` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `γ`	—	—
`γ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget` `CategoryTheory.Monad.toFunctor` `γ` `CategoryTheory.Monad.Algebra.a` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.Monad.ForgetCreatesLimits

Definitions

Name	Category	Theorems
`conePoint` 📖	CompOp	4 math math: `conePoint_a`, `liftedCone_pt`, `conePoint_A`, `liftedCone_π_app_f`
`liftedCone` 📖	CompOp	3 math math: `liftedConeIsLimit_lift_f`, `liftedCone_pt`, `liftedCone_π_app_f`
`liftedConeIsLimit` 📖	CompOp	1 math math: `liftedConeIsLimit_lift_f`
`newCone` 📖	CompOp	2 math math: `conePoint_a`, `newCone_π_app`
`γ` 📖	CompOp	1 math math: `γ_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conePoint_A` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.A` `conePoint` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget`	—	—
`conePoint_a` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.a` `conePoint` `CategoryTheory.Limits.IsLimit.lift` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget` `newCone`	—	—
`liftedConeIsLimit_lift_f` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.Hom.f` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `liftedCone` `CategoryTheory.Limits.IsLimit.lift` `liftedConeIsLimit` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.forget` `CategoryTheory.Functor.mapCone`	—	—
`liftedCone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `liftedCone` `conePoint`	—	—
`liftedCone_π_app_f` 📖	mathematical	—	`CategoryTheory.Monad.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `conePoint` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.Cone.π` `liftedCone` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.forget`	—	—
`newCone_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Monad.toFunctor` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget` `CategoryTheory.Limits.Cone.π` `newCone` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Monad.Algebra.A` `CategoryTheory.Functor.map` `CategoryTheory.Monad.Algebra.a`	—	`CategoryTheory.Category.id_comp`
`γ_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Monad.Algebra` `CategoryTheory.Monad.Algebra.eilenbergMoore` `CategoryTheory.Monad.forget` `CategoryTheory.Monad.toFunctor` `γ` `CategoryTheory.Monad.Algebra.a` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index