English
A Nakayama-type lemma for modules over noncommutative rings: if a FG submodule N satisfies N ⊆ Jac(R) • N, then N = 0 under mild hypotheses.
Русский
Типовая лемма Накема для модулей над некоммутативными кольцами: если FG-подмодуль N удовлетворяет N ⊆ Jac(R) • N, то при удовлетворяющих предпосылках N = 0.
LaTeX
$$$N \\text{ FG} \\; \\wedge\\; N \\le \\operatorname{Jac}(R) \\cdot N \\Rightarrow N = 0.$$$
Lean4
theorem jacobson_smul_lt {N : Submodule R M} (ne_bot : N ≠ ⊥) (fg : N.FG) : Ring.jacobson R • N < N :=
by
rw [← Module.Finite.iff_fg] at fg
rw [← nontrivial_iff_ne_bot] at ne_bot
convert map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)
on_goal 1 => rw [map_smul'']
all_goals rw [Submodule.map_top, range_subtype]
