binaryCofan_inr — Mathlib

English

In a MonoCoprod C, for any binary cofan c of A,B with a colimit hc, the right leg c.inr is mono.

Русский

В моно-копродукции C для бинарной ко-фана c:A,B — c.inr мономорфизм при наличии колимита hc.

LaTeX

$$$\\forall \\; A,B,\\; [MonoCoprod C], \\; (c:\\text{BinaryCofan } A B), (hc: IsColimit c) \\Rightarrow Mono(c.inr).$$$

Lean4

theorem binaryCofan_inr {A B : C} [MonoCoprod C] (c : BinaryCofan A B) (hc : IsColimit c) : Mono c.inr :=
  by
  haveI hc' : IsColimit (BinaryCofan.mk c.inr c.inl) :=
    BinaryCofan.IsColimit.mk _ (fun f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁)) (by simp) (by simp)
      (fun f₁ f₂ m h₁ h₂ => BinaryCofan.IsColimit.hom_ext hc (by cat_disch) (by cat_disch))
  exact binaryCofan_inl _ hc'

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