Nakayama's lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.smul_sup_eq_smul_sup_of_le_smul_of_le_jacobson - A version of (4) in Stacks: Nakayama's Lemma., generalising to the Jacobson of any ideal.
submodule.smul_sup_eq_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 ring_theory/noetherian 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

source

theorem submodule.eq_smul_of_le_smul_of_le_jacobson {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group 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 = ⊥.

source

theorem submodule.eq_bot_of_le_smul_of_le_jacobson_bot {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group 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

source

theorem submodule.smul_sup_eq_smul_sup_of_le_smul_of_le_jacobson {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {I J : ideal R} {N N' : submodule R M} (hN' : N'.fg) (hIJ : I ≤ J.jacobson) (hNN : N ⊔ 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_sup_eq_of_le_smul_of_le_jacobson_bot for the special case when J = ⊥.

source

theorem submodule.smul_sup_le_of_le_smul_of_le_jacobson_bot {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {I : ideal R} {N N' : submodule R M} (hN' : N'.fg) (hIJ : I ≤ ⊥.jacobson) (hNN : N ⊔ N' ≤ N ⊔ I • N') :

I • N' ≤ N

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