English
Let I ⊆ jacobson(0) and N finitely generated. If map((I·N).mkQ,N) ≤ map((I·N).mkQ, span R t) then N ≤ span R t.
Русский
Пусть I ⊆ jacobson(0) и N — конечно порождённый подмодуль. Если индуцированная карта из N через (I·N) в N удовлетворяет неравенству, то N лежит в линейной оболочке span R t.
LaTeX
$$$ N.FG \\land I \\le \\operatorname{jacobson}(\\{0\\}) \\land \\bigl( (I \\cdot N).mkQ \\; N \\le (I \\cdot N).mkQ \\bigl( \\operatorname{span} R t \\bigr) \\bigr) \\Rightarrow N \\le \\operatorname{span} R t $$$
Lean4
/-- **Nakayama's Lemma** - Statement (8) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). -/
@[stacks 00DV "(8)"]
theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot {I : Ideal R} {N : Submodule R M} {t : Set M} (hN : N.FG)
(hIjac : I ≤ jacobson ⊥) (htspan : map (I • N).mkQ N ≤ map (I • N).mkQ (span R t)) : N ≤ span R t :=
by
apply le_of_le_smul_of_le_jacobson_bot hN hIjac
apply_fun comap (I • N).mkQ at htspan
on_goal 2 => apply Submodule.comap_mono
simp only [comap_map_mkQ] at htspan
grw [sup_comm, ← htspan]
simp only [le_sup_right]
