English
If M ⊕ N embeds into M and M is Noetherian, then N is trivial; in fact, N is linearly isomorphic to the one-point module PUnit.
Русский
Если прямая сумма M ⊕ N встроена в M и M Нётеров, тогда N тривиально; фактически существует линейное эквивалентное отображение N ≃ PUnit.
LaTeX
$$$\\text{If } f: M \\times N \\to M \\text{ is injective and } M \\text{ is Noetherian, then } N \\cong_R PUnit$$$
Lean4
/-- **Orzech's theorem** for Noetherian modules: if `R` is a ring (not necessarily commutative),
`M` and `N` are `R`-modules, `M` is Noetherian, `i : N →ₗ[R] M` is injective,
`f : N →ₗ[R] M` is surjective, then `f` is also injective. The proof here is adapted from
Djoković's paper *Epimorphisms of modules which must be isomorphisms* [djokovic1973],
utilizing `LinearMap.iterateMapComap`.
See also Orzech's original paper: *Onto endomorphisms are isomorphisms* [orzech1971]. -/
theorem injective_of_surjective_of_injective (i f : N →ₗ[R] M) (hi : Injective i) (hf : Surjective f) : Injective f :=
by
haveI := isNoetherian_of_injective i hi
obtain ⟨n, H⟩ :=
monotone_stabilizes_iff_noetherian.2 ‹_› ⟨_, monotone_nat_of_le_succ <| f.iterateMapComap_le_succ i ⊥ (by simp)⟩
exact LinearMap.ker_eq_bot.1 <| bot_unique <| f.ker_le_of_iterateMapComap_eq_succ i ⊥ n (H _ (Nat.le_succ _)) hf hi
