English
For a diagram F: J ⥤ Comma L R, if HasColimit of F ⋙ fst L R and HasColimit of F ⋙ snd L R, and the colimit of F ⋙ fst L R is preserved by L, then F has a colimit in Comma L R.
Русский
Для диаграммы F: J ⥤ Comma L R, если существует колимит F ⋙ fst L R и колимит F ⋙ snd L R, и колимит F ⋙ fst L R сохраняется L, тогда F имеет колимит в Comma L R.
LaTeX
$$$\\operatorname{HasColimit}(F) \\quad\\text{при условиях } \\operatorname{HasColimit}(F\\circ \\mathrm{fst}(L,R)) , \\operatorname{HasColimit}(F\\circ \\mathrm{snd}(L,R)) , \\operatorname{PreservesColimit}(F\\circ \\mathrm{fst}(L,R),L)$$$
Lean4
instance hasColimit (F : J ⥤ Comma L R) [HasColimit (F ⋙ fst L R)] [HasColimit (F ⋙ snd L R)]
[PreservesColimit (F ⋙ fst L R) L] : HasColimit F :=
HasColimit.mk ⟨_, coconeOfPreservesIsColimit _ (colimit.isColimit _) (colimit.isColimit _)⟩
