mono_iff_ker_eq_bot — Mathlib

English

A morphism f is mono if and only if its kernel is trivial: Mono f ↔ f.hom.ker = ⊥.

Русский

Морфизм f является мономорфизмом тогда и только тогда, когда его ядро тривиально: Mono f ↔ f.hom.ker = ⊥.

LaTeX

$$$ \mathrm{Mono}\, f \;\iff\; f.\mathrm{hom}.\ker = \top^{-1} $$$

Lean4

@[to_additive]
theorem mono_iff_ker_eq_bot : Mono f ↔ f.hom.ker = ⊥ :=
  ⟨fun _ => ker_eq_bot_of_mono f, fun h => ConcreteCategory.mono_of_injective _ <| (MonoidHom.ker_eq_bot_iff f.hom).1 h⟩

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