English
If F ⟶ G and H is Van Kampen colimit, then the precomposition with an isomorphism preserves Van Kampen property: IsVanKampenColimit((Cocones.precompose α).obj c).
Русский
Если имеется отображение F ⟶ G и кокон c является колимитом Ван-Кампена, то предобразование по изоморфизму сохраняет это свойство: IsVanKampenColimit((Cocones.precompose α).obj c).
LaTeX
$$$\\IsVanKampenColimit(c) \\Rightarrow \\IsVanKampenColimit((\\mathrm{Cocones.precompose}(\\alpha)).{ }_{{}}\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!.obj c)$$$
Lean4
theorem of_iso {F : J ⥤ C} {c c' : Cocone F} (H : IsVanKampenColimit c) (e : c ≅ c') : IsVanKampenColimit c' :=
by
intro F' c'' α f h hα
have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
ext j
exact e.inv.2 j
rw [H c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα]
apply forall_congr'
intro j
conv_lhs => rw [← Category.comp_id (α.app j)]
haveI : IsIso e.inv.hom := Functor.map_isIso (Cocones.forget _) e.inv
exact (IsPullback.of_vert_isIso ⟨by simp⟩).paste_vert_iff (NatTrans.congr_app h j).symm
