isVanKampen_mk — Mathlib

English

A binary cofan c is Van Kampen if and only if, for all X', Y', c' and morphisms αX, αY with compatibility, a certain equivalence holds between nonempty colimits and pullbacks.

Русский

Два входящих узла c является ван kampen точно тогда, когда для любых X',Y', c' и совместимых морфизмов αX, αY выполняется эквивалентность между существованием колимита и условием равнопереплетения (pullback).

LaTeX

$$$IsVanKampenColimit(c) \\iff \\forall X',Y',c',αX,αY,f, (αX ≫ c.inl = c'.inl ≫ f) \, (αY ≫ c.inr = c'.inr ≫ f) \\Rightarrow (Nonempty(IsColimit(c')) \\iff IsPullback(c'.inl, αX, f, c.inl) \\land IsPullback(c'.inr, αY, f, c.inr))$$$

Lean4

theorem isVanKampen_mk {X Y : C} (c : BinaryCofan X Y) (cofans : ∀ X Y : C, BinaryCofan X Y)
    (colimits : ∀ X Y, IsColimit (cofans X Y)) (cones : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PullbackCone f g)
    (limits : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), IsLimit (cones f g))
    (h₁ :
      ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt) (_ : αX ≫ c.inl = (cofans X' Y').inl ≫ f)
        (_ : αY ≫ c.inr = (cofans X' Y').inr ≫ f),
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr)
    (h₂ : ∀ {Z : C} (f : Z ⟶ c.pt), IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)) :
    IsVanKampenColimit c := by
  rw [BinaryCofan.isVanKampen_iff]
  introv hX hY
  constructor
  · rintro ⟨h⟩
    let e := h.coconePointUniqueUpToIso (colimits _ _)
    obtain ⟨hl, hr⟩ := h₁ αX αY (e.inv ≫ f) (by simp [e, hX]) (by simp [e, hY])
    constructor
    · rw [← Category.id_comp αX, ← Iso.hom_inv_id_assoc e f]
      haveI : IsIso (𝟙 X') := inferInstance
      have : c'.inl ≫ e.hom = 𝟙 X' ≫ (cofans X' Y').inl :=
        by
        dsimp [e]
        simp
      exact (IsPullback.of_vert_isIso ⟨this⟩).paste_vert hl
    · rw [← Category.id_comp αY, ← Iso.hom_inv_id_assoc e f]
      haveI : IsIso (𝟙 Y') := inferInstance
      have : c'.inr ≫ e.hom = 𝟙 Y' ≫ (cofans X' Y').inr :=
        by
        dsimp [e]
        simp
      exact (IsPullback.of_vert_isIso ⟨this⟩).paste_vert hr
  · rintro ⟨H₁, H₂⟩
    refine ⟨IsColimit.ofIsoColimit ?_ <| (isoBinaryCofanMk _).symm⟩
    let e₁ : X' ≅ _ := H₁.isLimit.conePointUniqueUpToIso (limits _ _)
    let e₂ : Y' ≅ _ := H₂.isLimit.conePointUniqueUpToIso (limits _ _)
    have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst := by simp [e₁]
    have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst := by simp [e₂]
    rw [he₁, he₂]
    exact (BinaryCofan.mk _ _).isColimitCompRightIso e₂.hom ((BinaryCofan.mk _ _).isColimitCompLeftIso e₁.hom (h₂ f))

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