injective_of_surjective_of_submodule

English

Any surjective endomorphism of a Noetherian module is injective.

Русский

Любой сюръективный эндоморфизм Нётерова модуля инъективен.

LaTeX

$$$\\text{If } f: M \\to M \\text{ is surjective and } M \\text{ is Noetherian}, \\text{ then } f\\text{ is injective}$$$

Lean4

/-- **Orzech's theorem** for Noetherian modules: if `R` is a ring (not necessarily commutative),
`M` is a Noetherian `R`-module, `N` is a submodule, `f : N →ₗ[R] M` is surjective, then `f` is also
injective. -/
theorem injective_of_surjective_of_submodule {N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f :=
  IsNoetherian.injective_of_surjective_of_injective N.subtype f N.injective_subtype hf

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