comp_comparison_hasColimit — Mathlib

English

If F: J ⥤ D and R: D ⥤ C with a comonadic left adjoint and HasColimit(F ⋙ R), then HasColimit(F ⋙ Comonad.comparison(...)).

Русский

Если F: J ⥤ D и R: D ⥤ C с левым сопряжением комонады и HasColimit(F ⋙ R), то HasColimit(F ⋙ Comonad.comparison(...)).

LaTeX

$$$\\text{HasColimit}(F) \\Rightarrow \\text{HasColimit}\\bigl(F \\circ \\mathrm{comparison}(\\mathrm{comonadicAdjunction}\\,R)\\bigr).$$$

Lean4

instance comp_comparison_hasColimit (F : J ⥤ D) (R : D ⥤ C) [ComonadicLeftAdjoint R] [HasColimit (F ⋙ R)] :
    HasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R)) :=
  Comonad.hasColimit_of_comp_forget_hasColimit (F ⋙ Comonad.comparison (comonadicAdjunction R))

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