English
The functor Comma.fst L R preserves colimits of shape J, provided A,B have J-shaped colimits and R preserves J-shaped limits.
Русский
Функтор Comma.fst L R сохраняет колимиты формы J, если у A и B есть колимиты формы J, и R сохраняет пределы формы 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{fst})$$$
Lean4
instance preservesColimitsOfShape_fst [HasColimitsOfShape J A] [HasColimitsOfShape J B] [PreservesColimitsOfShape J L] :
PreservesColimitsOfShape J (Comma.fst L R) where
preservesColimit :=
preservesColimit_of_preserves_colimit_cocone
(coconeOfPreservesIsColimit _ (colimit.isColimit _) (colimit.isColimit _)) (colimit.isColimit _)
