mono_inl_iff — Mathlib

English

For two colimits c1,c2 of A,B, the left leg is mono for c1 iff it is mono for c2.

Русский

Если две кофункции (кофаны) c1,c2 для A,B имеют предел, то левый компонент моноинъекции одинаков для обеих: mono c1.inl ⇔ mono c2.inl.

LaTeX

$$$\\forall c_1,c_2\\ IsColimit c_1, IsColimit c_2:\\ Mono(c_1.inl) \\iff Mono(c_2.inl).$$$

Lean4

theorem mono_inl_iff {A B : C} {c₁ c₂ : BinaryCofan A B} (hc₁ : IsColimit c₁) (hc₂ : IsColimit c₂) :
    Mono c₁.inl ↔ Mono c₂.inl :=
  by
  suffices ∀ (c₁ c₂ : BinaryCofan A B) (_ : IsColimit c₁) (_ : IsColimit c₂) (_ : Mono c₁.inl), Mono c₂.inl by
    exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
  intro c₁ c₂ hc₁ hc₂ _
  simpa only [IsColimit.comp_coconePointUniqueUpToIso_hom] using mono_comp c₁.inl (hc₁.coconePointUniqueUpToIso hc₂).hom

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