English
If J is connected and C has pullbacks, colimits of shape J exist in C and exact colimits of shape J exist, then pulling back a colimit cocone along any morphism f: X → c.pt yields a new colimit cocone; i.e., the pullback of a colimit diagram along a morphism preserves the colimit property when the shape is connected.
Русский
Если J соединён и в C существуют вытягивания по асимптотам, а также колимиты формы J, то вытягивание колонолита вдоль любого отображения f: X → c.pt образует новый колимитный кокон; т.е. вытягивание сохраняет свойство колимита при связной форме.
LaTeX
$$$\text{pullbackOfHasExactColimitsOfShape} \, (F,c)\Rightarrow \mathrm{IsColimit}(\text{Cocone}(\cdot)).$$$
Lean4
/-- If `c` is a cocone over a functor `J ⥤ C` and `f : X ⟶ c.pt`, then for every `j : J` we can take
the pullback of `c.ι.app j` and `f`. This gives a new cocone with cone point `X`, and this cocone
is again a colimit cocone as long as `J` is connected and `C` has exact colimits of shape `J`.
-/
noncomputable def pullbackOfHasExactColimitsOfShape [HasPullbacks C] [HasColimitsOfShape J C]
[HasExactColimitsOfShape J C] {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c) {X : C} (f : X ⟶ c.pt) :
IsColimit (Cocone.mk _ (pullback.snd c.ι ((Functor.const J).map f))) :=
by
suffices IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f))) from Cocone.isColimitOfIsIsoColimMapι _
have hpull := colim.map_isPullback (IsPullback.of_hasPullback c.ι ((Functor.const J).map f))
dsimp only [colim_obj, colim_map] at hpull
have := hc.isIso_colimMap_ι
apply hpull.isIso_snd_of_isIso
