instMonoInl — Mathlib

English

In a category with MonoCoprod and HasBinaryCoproduct A,B, the left coproduct injection coprod.inl: A → A ⨿ B is mono.

Русский

В категории с MonoCoprod и HasBinaryCoproduct A,B левое включение coprod.inl: A → A ⨿ B мономорфизм.

LaTeX

$$$[MonoCoprod C] \\Rightarrow [HasBinaryCoproduct A B] \\Rightarrow Mono (coprod.inl: A \\to A ⨿ B).$$$

Lean4

instance {A B : C} [MonoCoprod C] [HasBinaryCoproduct A B] : Mono (coprod.inl : A ⟶ A ⨿ B) :=
  binaryCofan_inl _ (colimit.isColimit _)

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