comp_comparison_forget_hasColimit

English

The composite with the comonadic comparison has a colimit if F has a colimit after R.

Русский

Составной с комонадной сравнитель имеет колимит, если F имеет колимит после R.

LaTeX

$$$\\operatorname{HasColimit}(F \\circ R) \\Rightarrow \\operatorname{HasColimit}(F \\circ \\mathrm{comparison}(\\mathrm{comonadicAdjunction}\\;R)).$$$

Lean4

instance comp_comparison_forget_hasColimit (F : J ⥤ D) (R : D ⥤ C) [ComonadicLeftAdjoint R] [HasColimit (F ⋙ R)] :
    HasColimit ((F ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ Comonad.forget _) := by assumption

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