Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-16 08:00 ff84bf47

View on Github →

feat(category_theory/monad/limits): forgetful creates colimits (#2138)

forgetful creates colimits
tidy up proofs
add docs
suggestions from review

Estimated changes

Modified src/category_theory/monad/limits.lean

added def category_theory.monad.forget_creates_colimits.c

added def category_theory.monad.forget_creates_colimits.cocone_point

added theorem category_theory.monad.forget_creates_colimits.commuting

added def category_theory.monad.forget_creates_colimits.lambda

added def category_theory.monad.forget_creates_colimits.γ

added def category_theory.monad.forget_creates_colimits_of_monad_preserves

modified def category_theory.monad.forget_creates_limits