Lean4
/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit
which the comonad itself preserves.
-/
noncomputable def comonadicCreatesLimitOfPreservesLimit (R : D ⥤ C) (K : J ⥤ D) [ComonadicLeftAdjoint R]
[PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)]
[PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)] : CreatesLimit K R :=
by
letI A := Comonad.comparison (comonadicAdjunction R)
letI B := Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))
let i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _ ≅ K ⋙ R :=
Functor.associator _ _ _ ≪≫ isoWhiskerLeft K (Comonad.comparisonForget (comonadicAdjunction R))
letI :
PreservesLimit ((K ⋙ A) ⋙ Comonad.forget (Adjunction.toComonad (comonadicAdjunction R)))
(Adjunction.toComonad (comonadicAdjunction R)).toFunctor :=
by
dsimp
exact preservesLimit_of_iso_diagram _ i.symm
letI :
PreservesLimit
(((K ⋙ A) ⋙ Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))) ⋙
(Adjunction.toComonad (comonadicAdjunction R)).toFunctor)
(Adjunction.toComonad (comonadicAdjunction R)).toFunctor :=
by
dsimp
exact preservesLimit_of_iso_diagram _ (isoWhiskerRight i (comonadicRightAdjoint R ⋙ R)).symm
letI : CreatesLimit (K ⋙ A) B := CategoryTheory.Comonad.forgetCreatesLimit _
letI : CreatesLimit K (A ⋙ B) := CategoryTheory.compCreatesLimit _ _
let e := Comonad.comparisonForget (comonadicAdjunction R)
apply createsLimitOfNatIso e
