forget_creates_colimits_of_monad_preserves

English

If T preserves colimits of shape J and D ⋙ forget T has a colimit, then D has a colimit.

Русский

Если T сохраняет колимиты формы J и D ⋙ забыть T имеет колимит, то D имеет колимит.

LaTeX

$$$[PreservesColimitsOfShape J (T : C \to C)] \Rightarrow \, \Bigl[HasColimit (D \circ forget\ T) \Rightarrow HasColimit D\Bigr].$$$

Lean4

/-- For `D : J ⥤ Algebra T`, `D ⋙ forget T` has a colimit, then `D` has a colimit provided colimits
of shape `J` are preserved by `T`.
-/
theorem forget_creates_colimits_of_monad_preserves [PreservesColimitsOfShape J (T : C ⥤ C)] (D : J ⥤ Algebra T)
    [HasColimit (D ⋙ forget T)] : HasColimit D :=
  hasColimit_of_created D (forget T)

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