mapCocone_iff — Mathlib

English

For G an equivalence, IsVanKampenColimit (G.mapCocone c) is equivalent to IsVanKampenColimit c.

Русский

Для эквивалентности G свойство IsVanKampenColimit(G.mapCocone c) эквивалентно IsVanKampenColimit c.

LaTeX

$$$[G.IsEquivalence] \\Rightarrow IsVanKampenColimit(G.mapCocone c) \\iff IsVanKampenColimit(c)$$$

Lean4

theorem mapCocone_iff (G : C ⥤ D) {F : J ⥤ C} {c : Cocone F} [G.IsEquivalence] :
    IsVanKampenColimit (G.mapCocone c) ↔ IsVanKampenColimit c :=
  ⟨IsVanKampenColimit.of_mapCocone G, fun hc ↦
    by
    let e : F ⋙ G ⋙ Functor.inv G ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
    apply IsVanKampenColimit.of_mapCocone G.inv
    apply (IsVanKampenColimit.precompose_isIso_iff e.inv).mp
    exact hc.of_iso (Cocones.ext (G.asEquivalence.unitIso.app c.pt) (fun j => (by simp [e])))⟩

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