English
If α: F ⟶ G is an isomorphism, then precomposition with α preserves Van Kampen colimits: IsVanKampenColimit ((Cocones.precompose α).obj c).
Русский
Если α: F ⟶ G — изоморфизм, то предобразование по α сохраняет колимит Ван-Кампена.
LaTeX
$$$[IsIso(\\alpha)] \\Rightarrow IsVanKampenColimit((\\mathrm{Cocones.precompose}(\\alpha)).{ }_{{}}\\!\\!\\!\\!\\!\\!.obj c)$$$
Lean4
theorem precompose_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] {c : Cocone G} (hc : IsVanKampenColimit c) :
IsVanKampenColimit ((Cocones.precompose α).obj c) :=
by
intro F' c' α' f e hα
refine (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) (hα.comp (NatTrans.equifibered_of_isIso _))).trans ?_
apply forall_congr'
intro j
simp only [Functor.const_obj_obj, NatTrans.comp_app, Cocones.precompose_obj_pt, Cocones.precompose_obj_ι]
have : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 _) (c.ι.app j) := IsPullback.of_vert_isIso ⟨Category.comp_id _⟩
rw [← IsPullback.paste_vert_iff this _, Category.comp_id]
exact (congr_app e j).symm
