Submodule.eq_smul_of_le_smul_of_le_jacobson
theorem Submodule.eq_smul_of_le_smul_of_le_jacobson :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I J : Ideal R}
{N : Submodule R M}, N.FG → N ≤ I • N → I ≤ J.jacobson → N = J • N
**Nakayama's Lemma** - This theorem states that for any commutative ring `R`, any additive commutative group `M` and any `R`-module `M`, given ideals `I` and `J` of `R`, and a submodule `N` of `M` that is finitely generated (`N.FG`), if `N` is contained in the product of `I` and `N` (`N ≤ I • N`) and `I` is contained in the jacobson of `J` (`I ≤ J.jacobson`), then `N` is equal to the product of `J` and `N` (`N = J • N`). It's a slightly more general version of (2) in [Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). A special case when `J = ⊥` is also discussed in `eq_bot_of_le_smul_of_le_jacobson_bot`.
More concisely: If `R` is a commutative ring, `M` is an additive commutative group and `M` is an `R`-module, `I` and `J` are ideals of `R`, and `N` is a finitely generated submodule of `M` with `N ≤ I • N` and `I ≤ J.jacobson`, then `N = J • N`.
|
Submodule.smul_le_of_le_smul_of_le_jacobson_bot
theorem Submodule.smul_le_of_le_smul_of_le_jacobson_bot :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
{N N' : Submodule R M}, N'.FG → I ≤ ⊥.jacobson → N' ≤ N ⊔ I • N' → I • N' ≤ N
This theorem is a version of Nakayama's Lemma. For any commutative ring `R`, additive commutative group `M`, and `R`-module `M`, given an ideal `I` of `R` and two submodules `N` and `N'` of `M`, if `N'` is finitely generated, `I` is contained in the Jacobson radical of the zero ideal, and `N'` is contained in the join of `N` and the submodule generated by `I` and `N'`, then the submodule generated by `I` and `N'` is contained in `N`.
In mathematical notation, for a commutative ring \(R\), an additive commutative group \(M\), and \(R\)-module \(M\), given an ideal \(I\) of \(R\) and two submodules \(N\) and \(N'\) of \(M\), if \(N'\) is finitely generated, \(I \subseteq \textrm{JacobsonRadical}(0)\), and \(N' \subseteq N+IN'\), then \(IN' \subseteq N\), where \(IN'\) represents the submodule generated by the products of elements in \(I\) with elements in \(N'\).
More concisely: If `I` is an ideal of a commutative ring `R`, `N'` is a finitely generated submodule of an `R`-module `M`, and `I` is contained in the Jacobson radical of the zero ideal, then the submodule generated by `I` and `N'` is contained in `N`, given that `N'` is contained in the join of `N` and the submodule generated by `I` and `N'`.
|
Submodule.eq_bot_of_le_smul_of_le_jacobson_bot
theorem Submodule.eq_bot_of_le_smul_of_le_jacobson_bot :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
(N : Submodule R M), N.FG → N ≤ I • N → I ≤ ⊥.jacobson → N = ⊥
This theorem is a statement of Nakayama's Lemma, specifically Statement (2) as it appears in the Stacks Project. The theorem states that for any commutative ring `R`, any additive commutative group `M`, and any module `M` over `R`, given an ideal `I` of `R` and a finitely generated submodule `N` of `M`, if `N` is contained in the submodule generated by `I` and `N`, and `I` is contained in the Jacobson radical of the zero ideal, then `N` must be the zero submodule. In other words, under these conditions, any finitely generated module over the ring that is annihilated by an ideal contained in the Jacobson radical must be zero. This is a key result in commutative algebra and has important implications in the study of modules and ideals.
More concisely: If `R` is a commutative ring, `M` is an additive commutative group, and `M` is a `R`-module with `I` an ideal of `R`, `N` a finitely generated submodule of `M`, and `I` contained in the Jacobson radical of the zero ideal, then `N` is the zero submodule of `M`.
|
Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson
theorem Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I J : Ideal R}
{N N' : Submodule R M}, N'.FG → I ≤ J.jacobson → N' ≤ N ⊔ I • N' → N ⊔ I • N' = N ⊔ J • N'
**Nakayama's Lemma** - This theorem is a more generalized version of Nakayama's Lemma compared to the one mentioned in Stacks 00DV. The theorem states that for any commutative ring `R`, additive commutative group `M`, and `R`-module `M`, given two ideals `I` and `J` in `R`, and two submodules `N` and `N'` of `M`, if `N'` is finitely generated (denoted as `N'.FG`), `I` is contained within the Jacobson radical of `J` (denoted as `I ≤ J.jacobson`), and `N'` is contained within the join of `N` and the `I`-module of `N'` (denoted as `N' ≤ N ⊔ I • N'`), then the join of `N` and the `I`-module of `N'` is equal to the join of `N` and the `J`-module of `N'` (denoted as `N ⊔ I • N' = N ⊔ J • N'`).
More concisely: If `R` is a commutative ring, `M` is an additive commutative `R`-module, `I` and `J` are ideals in `R`, `N` and `N'` are submodules of `M` with `N'.FG`, `I ≤ J.jacobson`, and `N' ≤ N ⊔ I • N'`, then `N ⊔ I • N' = N ⊔ J • N'`.
|