English
The functor Comma.snd L R preserves colimits of shape J, given A,B have J-shaped colimits and L preserves J-shaped colimits.
Русский
Функтор Comma.snd L R сохраняет колимиты формы J, если A и B имеют колимиты формы J, и L сохраняет колимиты формы J.
LaTeX
$$$\\operatorname{HasColimitsOfShape}(J,A) \\land \\operatorname{HasColimitsOfShape}(J,B) \\land \\operatorname{PreservesColimitsOfShape}(J,L) \\Rightarrow \\operatorname{PreservesColimitsOfShape}(J, \\mathrm{Comma}(L,R) \\mathrm{snd})$$$
Lean4
instance preservesColimitsOfShape_snd [HasColimitsOfShape J A] [HasColimitsOfShape J B] [PreservesColimitsOfShape J L] :
PreservesColimitsOfShape J (Comma.snd L R) where
preservesColimit :=
preservesColimit_of_preserves_colimit_cocone
(coconeOfPreservesIsColimit _ (colimit.isColimit _) (colimit.isColimit _)) (colimit.isColimit _)
