mono_of_mono_right — Mathlib

English

If k.right is a monomorphism, then k is a monomorphism.

Русский

Если правый компонент k.right моно, то и k моно.

LaTeX

$$k.right is Mono implies k is Mono$$

Lean4

/-- If `k.right` is a monomorphism, then `k` is a monomorphism. In other words, `Under.forget X`
reflects epimorphisms.
The converse does not hold without additional assumptions on the underlying category, see
`CategoryTheory.Under.mono_right_of_mono`.
-/
theorem mono_of_mono_right {f g : Under X} (k : f ⟶ g) [hk : Mono k.right] : Mono k :=
  (forget X).mono_of_mono_map hk

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