mono_binaryCofanSum_inr' — Mathlib

English

Variant asserting mono for inr in binaryCofanSum

Русский

Вариант утверждает моно для inr в binaryCofanSum

LaTeX

$$[MonoCoprod C] (binaryCofanSum c c1 c2 hc1 hc2).inr is mono$$

Lean4

theorem mono_binaryCofanSum_inr' [MonoCoprod C] (inr : c₂.pt ⟶ c.pt)
    (hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)) : Mono inr :=
  by
  suffices inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr by
    rw [this]
    exact MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)
  exact Cofan.IsColimit.hom_ext hc₂ _ _ (by simpa using hinr)

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