Lean4
/-- The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit
which the monad itself preserves.
-/
noncomputable def monadicCreatesColimitOfPreservesColimit (R : D ⥤ C) (K : J ⥤ D) [MonadicRightAdjoint R]
[PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)]
[PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)] : CreatesColimit K R := by
-- Porting note: It would be nice to have a variant of apply which introduces goals for missing
-- instances.
letI A := Monad.comparison (monadicAdjunction R)
letI B := Monad.forget (Adjunction.toMonad (monadicAdjunction R))
let i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ Monad.forget _ ≅ K ⋙ R :=
Functor.associator _ _ _ ≪≫ isoWhiskerLeft K (Monad.comparisonForget (monadicAdjunction R))
letI :
PreservesColimit ((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (monadicAdjunction R)))
(Adjunction.toMonad (monadicAdjunction R)).toFunctor :=
by
dsimp
exact preservesColimit_of_iso_diagram _ i.symm
letI :
PreservesColimit
(((K ⋙ A) ⋙ Monad.forget (Adjunction.toMonad (monadicAdjunction R))) ⋙
(Adjunction.toMonad (monadicAdjunction R)).toFunctor)
(Adjunction.toMonad (monadicAdjunction R)).toFunctor :=
by
dsimp
exact preservesColimit_of_iso_diagram _ (isoWhiskerRight i (monadicLeftAdjoint R ⋙ R)).symm
letI : CreatesColimit (K ⋙ A) B := CategoryTheory.Monad.forgetCreatesColimit _
letI : CreatesColimit K (A ⋙ B) := CategoryTheory.compCreatesColimit _ _
let e := Monad.comparisonForget (monadicAdjunction R)
apply createsColimitOfNatIso e
