English
If c is a Van Kampen colimit and e: c ≅ c' is an isomorphism, then c' is Van Kampen; together with a canonical isomorphism, this yields an equivalence.
Русский
Если c — колимит Ван-Кампена и существует изоморфизм e: c ≅ c', то c' тоже является ван kampen колимитом; вместе с каноническим изоморфизмом получаем эквивалентность.
LaTeX
$$$\\IsVanKampenColimit(c) \\Rightarrow \\IsVanKampenColimit(c')$ for $c' \\cong c$$$
Lean4
theorem precompose_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] {c : Cocone G} (hc : IsUniversalColimit c) :
IsUniversalColimit ((Cocones.precompose α).obj c) :=
by
intro F' c' α' f e hα H
apply (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) (hα.comp (NatTrans.equifibered_of_isIso _)))
intro j
simp only [Functor.const_obj_obj, NatTrans.comp_app]
rw [← Category.comp_id f]
exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨Category.comp_id _⟩)
