A new formulation of Nakayama's lemma [stacks 00DV (8)]

Stream: mathlib4

[Xingyu Zhong]

Hello everyone, I've just formalized a version of Nakayama's Lemma (stacks 00DV (8), note that several other forms are already in Mathlib/RingTheory/Nakayama.lean). Wondering if it deserves my first contribution to Mathlib.

Mathematically it says that for a commutative ring $R$, an ideal $I$ of $R$ contained in the Jacobson radical of $R$, and a finitely generated $R$-module $N$, if $x_1, \dots, x_n \in N$ generate $N / I \cdot N$, then they also generate $N$. Below is the (slightly modified) formalized statement:

import Mathlib.RingTheory.Finiteness.Basic
import Mathlib.RingTheory.Finiteness.Nakayama
import Mathlib.RingTheory.Jacobson.Ideal

variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
open Ideal
namespace Submodule
/-- **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
  sorry

Would this formulation be a good candidate for a PR?

[Kenny Lau]

what is the role of M?

[Xingyu Zhong]

I just follow the current practice in Mathlib/RingTheory/Nakayama.lean. In my view it serve as a common ambient space, for example $M$ can be a local ring $A$ and $I$ & $N$ be its maximal ideal $\mathfrak m$.

[Xingyu Zhong]

opened PR #28641

[Antoine Chambert-Loir]

(deleted)