1.1 Nakayama’s Lemma and Corollaries
State Nakayama’s Lemma here.
The proof of this is already in Mathlib
Let \((R,\mathfrak {m},k)\) be a local ring. Let \(M\) be an \(R\)-module. If the elements \(x_1, \ldots , x_n\) are elements in \(M\) that form a basis in the projection \(M / \mathfrak {m} M\), then \(x_1, ldots, x_n\) generate \(M\).
See Atiyah-MacDonald Corollary 2.8
The following lemma is used by user6:
A finitely generated projective module over a regular local ring is free
A proof of this theorem can be pieced together from this stack exchange answer: https://math.stackexchange.com/questions/3362463/projective-modules-over-local-rings-are-free-matsumuras-proof This proof needs
Nakayama’s lemma
Equivalent definitions of projective modules
Let \(f : M \to M\) be a surjection of modules (over a local ring?). Then \(f\) is an isomorphism.
I think this uses the Corollary 2.8 version of Nakayama’s Lemma