mono_iff_ker_eq_bot — Mathlib

English

In ModuleCat, a morphism is mono if and only if its underlying linear map has trivial kernel.

Русский

В ModuleCat морфизм моно тогда и только тогда, когда его лежащее линейное отображение имеет тривиальное ядро.

LaTeX

$$$\\text{Mono}(f) \\iff \\ker(f.hom) = \\bot$$$

Lean4

theorem mono_iff_ker_eq_bot : Mono f ↔ LinearMap.ker f.hom = ⊥ :=
  ⟨fun _ => ker_eq_bot_of_mono _, fun hf =>
    ConcreteCategory.mono_of_injective _ <| by convert LinearMap.ker_eq_bot.1 hf⟩

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