English
Under a collection of preservation/reflects conditions for limits along C, and with H: IsVanKampenColimit (G.mapCocone c), one obtains IsVanKampenColimit c.
Русский
При наборе условий сохранения и отражения пределов и наличии H: IsVanKampenColimit(G.mapCocone c), получаем IsVanKampenColimit c.
LaTeX
$$$\\Big( PreservesLimitsOfShape.. \\wedge ReflectsColimitsOfShape .. \\wedge (H) \\Big) \\Rightarrow IsVanKampenColimit(c)$$$
Lean4
theorem of_mapCocone (G : C ⥤ D) {F : J ⥤ C} {c : Cocone F}
[∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G]
[∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G] [ReflectsLimitsOfShape WalkingCospan G]
[PreservesColimitsOfShape J G] [ReflectsColimitsOfShape J G] (H : IsVanKampenColimit (G.mapCocone c)) :
IsVanKampenColimit c := by
intro F' c' α f h hα
refine
(Iff.trans ?_
(H (G.mapCocone c') (whiskerRight α G) (G.map f) (by ext j; simpa using G.congr_map (NatTrans.congr_app h j))
(hα.whiskerRight G))).trans
(forall_congr' fun j => ?_)
· exact ⟨fun h => ⟨isColimitOfPreserves G h.some⟩, fun h => ⟨isColimitOfReflects G h.some⟩⟩
· exact IsPullback.map_iff G (NatTrans.congr_app h.symm j)
