English
If J is connected and C has pushouts, limits of shape J exist and are exact, then the pushout along the limit projections yields a new limit cone; i.e., pushouts preserve exactness in a connected shape.
Русский
Если J соединён и в C существуют пуш-ауты, пределы формы J существуют и точны, тогда вытягивание вдоль проекций предела даёт новый предел-конус; точность сохраняется для связной формы.
LaTeX
$$$\text{pushoutOfHasExactLimitsOfShape}\, (F,c) \Rightarrow \text{IsLimit}(\text{Cone})$$$
Lean4
/-- If `c` is a cone over a functor `J ⥤ C` and `f : c.pt ⟶ X`, then for every `j : J` we can take
the pushout of `c.π.app j` and `f`. This gives a new cone with cone point `X`, and this cone is
again a limit cone as long as `J` is connected and `C` has exact limits of shape `J`.
-/
noncomputable def pushoutOfHasExactLimitsOfShape [HasPushouts C] [HasLimitsOfShape J C] [HasExactLimitsOfShape J C]
{F : J ⥤ C} {c : Cone F} (hc : IsLimit c) {X : C} (f : c.pt ⟶ X) :
IsLimit (Cone.mk _ (pushout.inr c.π ((Functor.const J).map f))) :=
by
suffices IsIso (limMap (pushout.inr c.π ((Functor.const J).map f))) from Cone.isLimitOfIsIsoLimMapπ _
have hpush := lim.map_isPushout (IsPushout.of_hasPushout c.π ((Functor.const J).map f))
dsimp only [lim_obj, lim_map] at hpush
have := hc.isIso_limMap_π
apply hpush.isIso_inr_of_isIso
