forgetCreatesLimit — Mathlib

Lean4
/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit
which the comonad itself preserves.
-/
noncomputable instance forgetCreatesLimit (D : J ⥤ Coalgebra T) [PreservesLimit (D ⋙ forget T) (T : C ⥤ C)]
    [PreservesLimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] : CreatesLimit D (forget T) :=
  createsLimitOfReflectsIso fun c t =>
    { liftedCone :=
        { pt := conePoint c t
          π :=
            { app := fun j =>
                { f := c.π.app j
                  h := commuting _ _ _ }
              naturality := fun A B f => by
                ext1
                simpa using (c.w f).symm } }
      validLift := Cones.ext (Iso.refl _)
      makesLimit := liftedConeIsLimit _ _ }
Похожие утверждения