English
If a finitely generated submodule N is equal to I·N for some ideal I contained in the Jacobson radical of a ring, then N is trivial (0).
Русский
Если порожденный порождающий подмодуль N удовлетворяет N = I·N для некоторой идеала I, содержащегося в Jacobson радикале кольца, то N тривиален (нулевой).
LaTeX
$$$$ \\text{If } N \\text{ is FG and } N = I \\cdot N \\text{ with } I \\le \operatorname{jacobson}(J), \\text{ then } N = 0. $$$$
Lean4
/-- **Nakayama's Lemma** - A slightly more general version of (2) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `eq_bot_of_le_smul_of_le_jacobson_bot` for the special case when `J = ⊥`. -/
@[stacks 00DV "(2)"]
theorem eq_smul_of_le_smul_of_le_jacobson {I J : Ideal R} {N : Submodule R M} (hN : N.FG) (hIN : N ≤ I • N)
(hIjac : I ≤ jacobson J) : N = J • N :=
by
refine le_antisymm ?_ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)
intro n hn
obtain ⟨r, hr⟩ := Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN
obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r (hIjac hr.1)
have : n = -(s * r - 1) • n := by rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
rw [this]
exact Submodule.smul_mem_smul (Submodule.neg_mem _ hs) hn
