Documentation

Mathlib.CategoryTheory.Monad.Limits

Limits and colimits in the category of algebras #

This file shows that the forgetful functor forget T : Algebra T ⥤ C for a monad T : C ⥤ C creates limits and creates any colimits which T preserves. This is used to show that Algebra T has any limits which C has, and any colimits which C has and T preserves. This is generalised to the case of a monadic functor D ⥤ C.

TODO #

Dualise for the category of coalgebras and comonadic left adjoints.

@[simp]
theorem CategoryTheory.Monad.ForgetCreatesColimits.γ_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J (CategoryTheory.Monad.Algebra T)} (j : J) :
CategoryTheory.Monad.ForgetCreatesColimits.γ.app j = (D.obj j).a

(Impl) The natural transformation given by the algebra structure maps, used to construct a cocone c with apex colimit (D ⋙ forget T).

Instances For
    @[reducible]

    (Impl) Define the map λ : TL ⟶ L, which will serve as the structure of the coalgebra on L, and we will show is the colimiting object. We use the cocone constructed by c and the fact that T preserves colimits to produce this morphism.

    Instances For