mono_iff_injective — Mathlib

English

Let f: A → B be a morphism in the category of commutative groups. Then f is a monomorphism if and only if the underlying function is injective.

Русский

Пусть f: A → B — морфизм в категории коммутативных групп. Тогда f является мономорфизмом тогда и только тогда, когда соответствующая функция инъективна.

LaTeX

$$$$ \mathrm{Mono}(f) \iff \mathrm{Function.Injective}(f) $$$$

Lean4

@[to_additive]
theorem mono_iff_injective : Mono f ↔ Function.Injective f :=
  Iff.trans (mono_iff_ker_eq_bot f) <| MonoidHom.ker_eq_bot_iff f.hom

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