mono_inr_of_isVanKampen — Mathlib

English

A constructive criterion to build a Van Kampen cofan from smaller van Kampen data and specified isomorphisms.

Русский

Построение ван kampen кофана из меньших данных ван kampen и заданных изоморфизмов.

LaTeX

$$$(BinaryCofan.isVanKampen_mk\\, c\\, cofans\\, colimits\\, cones\\, limits\\, h_1\\, h_2) \\Rightarrow IsVanKampenColimit c$$$

Lean4

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

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