isPullback_initial_to_of_isVanKampen

English

Alternative construction of a van kampen cofan from cones and pullbacks.

Русский

Альтернативная конструция ван kampen кофана из конусов и пуллбаэков.

LaTeX

$$$BinaryCofan.isVanKampen_mk\\, (X,Y,c) \\Rightarrow IsVanKampenColimit c$$$

Lean4

theorem isPullback_initial_to_of_isVanKampen [HasInitial C] {c : BinaryCofan X Y} (h : IsVanKampenColimit c) :
    IsPullback (initial.to _) (initial.to _) c.inl c.inr :=
  by
  refine
    ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_ (mapPair_equifibered _)).mp ⟨?_⟩
        ⟨WalkingPair.left⟩).flip
  · ext ⟨⟨⟩⟩ <;> simp
  ·
    exact
      ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr
          (by
            dsimp
            infer_instance)).some

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