isVanKampen_iff — Mathlib

English

Under certain hypotheses (finitary extensive, pullbacks exist, etc.), a pushout is van Kampen; more precisely, H.IsVanKampen holds for the pushout square.

Русский

При заданных гипотезах (финитарная эксцентрированность, существуют предобразные), pushout обладает свойством ван-Кемпен; то есть H.IsVanKampen выполняется для квадрата прообраза.

LaTeX

$$$\text{FinitaryExtensive}\, C \land \text{HasPullbacks}\;\Rightarrow\; H.IsVanKampen$$

Lean4

theorem isVanKampen_iff (H : IsPushout f g h i) : H.IsVanKampen ↔ IsVanKampenColimit (PushoutCocone.mk h i H.w) :=
  by
  constructor
  · intro H F' c' α fα eα hα
    refine
      Iff.trans ?_
        ((H (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app _) (c'.ι.app _) (α.app _) (α.app _)
              (α.app _) fα (by convert hα WalkingSpan.Hom.fst) (by convert hα WalkingSpan.Hom.snd) ?_ ?_ ?_).trans
          ?_)
    · have :
        F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left =
          F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right :=
        by simp only [Cocone.w]
      rw [(IsColimit.equivOfNatIsoOfIso (diagramIsoSpan F') c' (PushoutCocone.mk _ _ this) _).nonempty_congr]
      · exact ⟨fun h => ⟨⟨this⟩, h⟩, fun h => h.2⟩
      · refine Cocones.ext (Iso.refl c'.pt) ?_
        rintro (_ | _ | _) <;> dsimp <;> simp only [c'.w, Category.id_comp, Category.comp_id]
    · exact ⟨NatTrans.congr_app eα.symm _⟩
    · exact ⟨NatTrans.congr_app eα.symm _⟩
    · exact ⟨by simp⟩
    constructor
    · rintro ⟨h₁, h₂⟩ (_ | _ | _)
      · rw [← c'.w WalkingSpan.Hom.fst]; exact (hα WalkingSpan.Hom.fst).paste_horiz h₁
      exacts [h₁, h₂]
    · intro h; exact ⟨h _, h _⟩
  · introv H W' hf hg hh hi w
    refine Iff.trans ?_ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], ?_⟩ αZ ?_ ?_).trans ?_)
    rotate_left
    · rintro i _ (_ | _ | _)
      · dsimp; simp only [Functor.map_id, Category.comp_id, Category.id_comp]
      exacts [hf.w, hg.w]
    · ext (_ | _ | _)
      · dsimp
        rw [PushoutCocone.condition_zero, Category.assoc]
        erw [hh.w]
        rw [hf.w_assoc]
      exacts [hh.w.symm, hi.w.symm]
    · rintro i _ (_ | _ | _)
      · dsimp; simp_rw [Functor.map_id]
        exact IsPullback.of_horiz_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩
      exacts [hf, hg]
    · constructor
      · intro h; exact ⟨h WalkingCospan.left, h WalkingCospan.right⟩
      · rintro ⟨h₁, h₂⟩ (_ | _ | _)
        · dsimp; rw [PushoutCocone.condition_zero]; exact hf.paste_horiz h₁
        exacts [h₁, h₂]
    · exact ⟨fun h => h.2, fun h => ⟨w, h⟩⟩

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