Commit 2023-04-20 18:32 9d37e735

View on Github →

feat: Port CategoryTheory.Monad.Limits (#3533)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monad/Limits.lean

added def CategoryTheory.Monad.ForgetCreatesColimits.coconePoint

added theorem CategoryTheory.Monad.ForgetCreatesColimits.commuting

added def CategoryTheory.Monad.ForgetCreatesColimits.lambda

added def CategoryTheory.Monad.ForgetCreatesColimits.liftedCocone

added def CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit

added def CategoryTheory.Monad.ForgetCreatesColimits.newCocone

added def CategoryTheory.Monad.ForgetCreatesColimits.γ

added def CategoryTheory.Monad.ForgetCreatesLimits.conePoint

added def CategoryTheory.Monad.ForgetCreatesLimits.liftedCone

added def CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit

added def CategoryTheory.Monad.ForgetCreatesLimits.newCone

added def CategoryTheory.Monad.ForgetCreatesLimits.γ

added theorem CategoryTheory.Monad.forget_creates_colimits_of_monad_preserves

added theorem CategoryTheory.Monad.hasLimit_of_comp_forget_hasLimit

added theorem CategoryTheory.hasColimitsOfShape_of_reflective

added theorem CategoryTheory.hasLimit_of_reflective

added theorem CategoryTheory.hasLimitsOfShape_of_reflective

added theorem CategoryTheory.has_colimits_of_reflective

added theorem CategoryTheory.has_limits_of_reflective