of_iso — Mathlib

English

If c is a Van Kampen colimit and e: c ≅ c' is an isomorphism, then c' is also a Van Kampen colimit.

Русский

Если кокон c является колимитом Ван-Кампена и существует изоморфизм e: c ≅ c', то и c' является колимитом Ван-Кампена.

LaTeX

$$$\\IsVanKampenColimit(c) \\Rightarrow \\IsVanKampenColimit(c')$ for $c' \\cong c$$$

Lean4

theorem of_iso {F : J ⥤ C} {c c' : Cocone F} (hc : IsUniversalColimit c) (e : c ≅ c') : IsUniversalColimit c' :=
  by
  intro F' c'' α f h hα H
  have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
    ext j
    exact e.inv.2 j
  apply hc c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα
  intro j
  rw [← Category.comp_id (α.app j)]
  exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨by simp⟩)

Похожие утверждения