ker_eq_bot_of_mono — Mathlib

English

For a monomorphism f: X → Y in ModuleCat, the kernel of the underlying linear map is the zero submodule.

Русский

Для моно-гомоморфизма f: X → Y в ModuleCat ядро линейного отображения f равно нулевому подмодулю.

LaTeX

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

Lean4

theorem ker_eq_bot_of_mono [Mono f] : LinearMap.ker f.hom = ⊥ :=
  LinearMap.ker_eq_bot_of_cancel fun u v h =>
    ModuleCat.hom_ext_iff.mp <| (@cancel_mono _ _ _ _ _ f _ (↟u) (↟v)).1 <| ModuleCat.hom_ext_iff.mpr h

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