English
If F: J ⥤ C and c: Cocone F with suitable preservation/reflecting properties by G, and G.mapCocone c is Van Kampen, then c is Van Kampen.
Русский
Пусть F: J ⥤ C и кокон c над F обладает нужными свойствами сохранения и отражения пределов через G; если G.mapCocone c — колимит Ван-Кампена, то и c — ван kampen колимит.
LaTeX
$$$(PreservesLimitsOfShape..) \\Rightarrow IsVanKampenColimit(G.mapCocone c) \\Rightarrow IsVanKampenColimit(c)$$$
Lean4
theorem of_mapCocone (G : C ⥤ D) {F : J ⥤ C} {c : Cocone F} [PreservesLimitsOfShape WalkingCospan G]
[ReflectsColimitsOfShape J G] (hc : IsUniversalColimit (G.mapCocone c)) : IsUniversalColimit c :=
fun F' c' α f h hα H ↦
⟨isColimitOfReflects _
(hc (G.mapCocone c') (whiskerRight α G) (G.map f) (by ext j; simpa using G.congr_map (NatTrans.congr_app h j))
(hα.whiskerRight G) (fun j ↦ (H j).map G)).some⟩
