forget_creates_limits_of_comonad_preserves

English

For D ⥤ C with coreflective R, if C has colimits of shape J, then D has colimits of shape J.

Русский

Для D ⥤ C с ядромcoreflective R, если C имеет колимиты по форме J, то D имеет колимиты по форме J.

LaTeX

$$$\\operatorname{HasColimitsOfShape} J C \\Rightarrow (\\text{Coreflective } R \\Rightarrow \\operatorname{HasColimitsOfShape} J D).$$$

Lean4

/-- For `D : J ⥤ Coalgebra T`, `D ⋙ forget T` has a limit, then `D` has a limit provided limits
of shape `J` are preserved by `T`.
-/
theorem forget_creates_limits_of_comonad_preserves [PreservesLimitsOfShape J (T : C ⥤ C)] (D : J ⥤ Coalgebra T)
    [HasLimit (D ⋙ forget T)] : HasLimit D :=
  hasLimit_of_created D (forget T)

Похожие утверждения