Nakayama's lemma

This file contains some alternative statements of Nakayama's Lemma as found in Stacks: Nakayama's Lemma.

Main statements

• Submodule.eq_smul_of_le_smul_of_le_jacobson - A version of (2) in Stacks: Nakayama's Lemma., generalising to the Jacobson of any ideal.

• Submodule.eq_bot_of_le_smul_of_le_jacobson_bot - Statement (2) in Stacks: Nakayama's Lemma.

• Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson - A version of (4) in Stacks: Nakayama's Lemma., generalising to the Jacobson of any ideal.

• Submodule.smul_le_of_le_smul_of_le_jacobson_bot - Statement (4) in Stacks: Nakayama's Lemma.

Note that a version of Statement (1) in Stacks: Nakayama's Lemma can be found in RingTheory.Finiteness under the name Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul

References

• Stacks: Nakayama's Lemma

Tags

Nakayama, Jacobson

theorem Submodule.eq_smul_of_le_smul_of_le_jacobson {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I J : Ideal R} {N : Submodule R M} (hN : N.FG) (hIN : N ≤ I • N) (hIjac : I ≤ J.jacobson) : N = J • N

Nakayama's Lemma - A slightly more general version of (2) in Stacks 00DV. See also eq_bot_of_le_smul_of_le_jacobson_bot for the special case when J = ⊥.

theorem Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {N : Submodule R M} (hN : N.FG) (hIN : N = I • N) (hIjac : I ≤ N.annihilator.jacobson) : N = ⊥

theorem Submodule.eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {r : R} {N : Submodule R M} (hN : N.FG) (hrN : N = r • N) (hrJac : r ∈ N.annihilator.jacobson) : N = ⊥

theorem Submodule.eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {s : Set R} {N : Submodule R M} (hN : N.FG) (hsN : N = s • N) (hsJac : s ⊆ ↑N.annihilator.jacobson) : N = ⊥

theorem Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Finite R M] {I : Ideal R} (h : I ≤ (Module.annihilator R M).jacobson) : ⊤ ≠ I • ⊤

theorem Submodule.top_ne_set_smul_of_subset_jacobson_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Finite R M] {s : Set R} (h : s ⊆ ↑(Module.annihilator R M).jacobson) : ⊤ ≠ s • ⊤

theorem Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Finite R M] {r : R} (h : r ∈ (Module.annihilator R M).jacobson) : ⊤ ≠ r • ⊤

theorem Submodule.eq_bot_of_le_smul_of_le_jacobson_bot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R) (N : Submodule R M) (hN : N.FG) (hIN : N ≤ I • N) (hIjac : I ≤ ⊥.jacobson) : N = ⊥

Nakayama's Lemma - Statement (2) in Stacks 00DV. See also eq_smul_of_le_smul_of_le_jacobson for a generalisation to the jacobson of any ideal

theorem Submodule.sup_eq_sup_smul_of_le_smul_of_le_jacobson {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I J : Ideal R} {N N' : Submodule R M} (hN' : N'.FG) (hIJ : I ≤ J.jacobson) (hNN : N' ≤ N ⊔ I • N') : N ⊔ N' = N ⊔ J • N'

theorem Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I J : Ideal R} {N N' : Submodule R M} (hN' : N'.FG) (hIJ : I ≤ J.jacobson) (hNN : N' ≤ N ⊔ I • N') : N ⊔ I • N' = N ⊔ J • N'

Nakayama's Lemma - A slightly more general version of (4) in Stacks 00DV. See also smul_le_of_le_smul_of_le_jacobson_bot for the special case when J = ⊥.

theorem Submodule.le_of_le_smul_of_le_jacobson_bot {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {N N' : Submodule R M} (hN' : N'.FG) (hIJ : I ≤ ⊥.jacobson) (hNN : N' ≤ N ⊔ I • N') : N' ≤ N

theorem Submodule.smul_le_of_le_smul_of_le_jacobson_bot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {N N' : Submodule R M} (hN' : N'.FG) (hIJ : I ≤ ⊥.jacobson) (hNN : N' ≤ N ⊔ I • N') : I • N' ≤ N

Nakayama's Lemma - Statement (4) in Stacks 00DV. See also sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson for a generalisation to the jacobson of any ideal