mono_of_mono_left — Mathlib

English

If k is a morphism in Over X and k is mono, then k.left is mono.

Русский

Пусть k — морфизм в Over X; если он моно, то моно и его левый компонент.

LaTeX

$$$\\operatorname{Mono}(k) \\Rightarrow \\operatorname{Mono}(k.\\text{left})$$$

Lean4

/-- If `k.left` is a monomorphism, then `k` is a monomorphism. In other words, `Over.forget X` reflects
monomorphisms.
The converse of `CategoryTheory.Over.mono_left_of_mono`.

This lemma is not an instance, to avoid loops in type class inference.
-/
theorem mono_of_mono_left {f g : Over X} (k : f ⟶ g) [hk : Mono k.left] : Mono k :=
  (forget X).mono_of_mono_map hk

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