mono_binaryCofanSum_inl' — Mathlib

English

Variant stating mono for inl in a colonne with colimits hc hc1 hc2

Русский

Вариант утверждает моно для inl в связке с колимитами hc hc1 hc2

LaTeX

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

Lean4

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

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