Nakayama's lemma with weighted generators, over ℤ, and at a point

Let M be a module over a commutative ring R, spanned by a finite family b, and let I be an ideal. Mathlib's Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul says that if M = I • M, some r ≡ 1 (mod I) kills M. This file proves the weighted form: if e i • b i lies in I • M for each i, then some r ≡ ∏ᵢ e i (mod I) kills M (Submodule.exists_sub_prod_mem_and_smul_eq_zero). The case e = 1 recovers Nakayama's lemma for a finite spanning family.

The proof is the determinant trick: writing e i • b i = ∑ⱼ θ i j • b j with θ i j ∈ I, the determinant of diag e - θ kills every b k, and it is ∏ᵢ e i modulo I.

This is the commutative-algebra step of the proof, due to Artin and Tate, that the transfer of a finite group into its commutator subgroup is trivial: there R is the integral group ring of a finite abelian group, I its augmentation ideal and e i the orders of a basis of the group.

The file also records the global form of Nakayama's lemma: a finitely generated submodule N with N = m • N for every maximal ideal m is zero (Submodule.eq_bot_of_forall_isMaximal_le_smul). Over ℤ this passes from statements modulo every prime to integral statements: a finitely generated subgroup N of an abelian group with N = p • N for every prime p is zero (Submodule.eq_bot_of_forall_prime_le_smul).

For a finite module M, Nakayama's lemma also characterises I M = M as the comaximality of I with the annihilator of M (Ideal.smul_top_eq_top_iff_sup_annihilator_eq_top).

Finally, Nakayama's lemma at a field-valued point R → F: if the fibre F ⊗[R] M of a finite module has dimension d, then M is generated by d elements after inverting an element of R that does not vanish at that point (Module.exists_finset_card_le_finrank_and_smul_mem_span). The point need not be a residue field of R: it factors through the residue field of its kernel, over which F is faithfully flat.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIII.
• D. Ferrand, La démonstration par Artin–Tate du théorème de l'idéal principal (2011), §2.

theorem Submodule.exists_sub_prod_mem_and_smul_eq_zero {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] (I : Ideal R) {b : ι → M} (hb : span R (Set.range b) = ⊤) (e : ι → R) (he : ∀ (i : ι), e i • b i ∈ I • ⊤) : ∃ (r : R), r - ∏ i : ι, e i ∈ I ∧ ∀ (m : M), r • m = 0

Nakayama's lemma with weighted generators. If b spans M and e i • b i ∈ I • M for every i, then some r ≡ ∏ᵢ e i (mod I) kills M.

theorem Submodule.eq_bot_of_forall_isMaximal_le_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Submodule R M} (hN : N.FG) (h : ∀ (m : Ideal R), m.IsMaximal → N ≤ m • N) : N = ⊥

Nakayama's lemma, globally. A finitely generated submodule N with N ≤ m • N for every maximal ideal m is zero.

theorem Submodule.eq_bot_of_forall_prime_le_smul {M : Type u_4} [AddCommGroup M] {N : Submodule ℤ M} (hN : N.FG) (h : ∀ (p : ℕ), Nat.Prime p → N ≤ Ideal.span {↑p} • N) : N = ⊥

Nakayama's lemma over ℤ. A finitely generated subgroup N of an abelian group with N ≤ p • N for every prime p is zero.

theorem Ideal.smul_top_eq_top_iff_sup_annihilator_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) : I • ⊤ = ⊤ ↔ I ⊔ Module.annihilator R M = ⊤

For a finite module M, I M = M exactly when I and the annihilator of M are comaximal.

theorem Module.exists_algebraMap_ne_zero_and_smul_eq_zero {R : Type u_1} {M : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Field F] [Algebra R F] (h : Subsingleton (TensorProduct R F M)) : ∃ (r : R), (algebraMap R F) r ≠ 0 ∧ ∀ (x : M), r • x = 0

A finite module whose fibre F ⊗[R] M at a field-valued point R → F vanishes is killed by an element of R that does not vanish at that point.

theorem Module.exists_finset_card_le_finrank_and_smul_mem_span {R : Type u_1} {M : Type u_2} {F : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Field F] [Algebra R F] : ∃ (s : Finset M), s.card ≤ finrank F (TensorProduct R F M) ∧ ∃ (r : R), (algebraMap R F) r ≠ 0 ∧ ∀ (x : M), r • x ∈ Submodule.span R ↑s

Nakayama's lemma at a field-valued point. If the fibre F ⊗[R] M of a finite module at a field-valued point R → F has dimension d, then M is generated by d elements after inverting some element of R that does not vanish at that point.