mono_comp — Mathlib

English

The composition of monomorphisms is a monomorphism: if f and g are monos, then f ≫ g is mono.

Русский

Композиция монооморфизмов является монооморфизмом: если f и g моно, то f ≫ g моно.

LaTeX

$$$ {f:X\\to Y} [\\mathrm{Mono} f] (g:Y\\to Z) [\\mathrm{Mono} g]: \\mathrm{Mono}(f\\circ g) $$$

Lean4

/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
`Mono g` as typeclass arguments. For a version taking them as explicit arguments, see `mono_comp'`.
-/
instance mono_comp {X Y Z : C} (f : X ⟶ Y) [Mono f] (g : Y ⟶ Z) [Mono g] : Mono (f ≫ g) :=
  ⟨fun _ _ w => (cancel_mono f).1 <| (cancel_mono_assoc_iff g).1 w⟩

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