Ideal.Filtration.submodule_fg_iff_stable
theorem Ideal.Filtration.submodule_fg_iff_stable :
∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
(F : I.Filtration M), (∀ (i : ℕ), (F.N i).FG) → (F.submodule.FG ↔ F.Stable)
The theorem states that for any commutative ring `R`, an additive commutative group `M`, and a module `M` over `R`, if the components of a filtration `F` of an ideal `I` in `R` are finitely generated, then the filtration `F` is stable if and only if its associated submodule is finitely generated. Here, stability of a filtration is a property involving the limiting behavior of the filtration sequence as the index tends to infinity.
More concisely: For a commutative ring `R`, an additive commutative group `M`, and an ideal `I` of `R` with finitely generated filtration components, the filtration is stable if and only if the associated submodule of `M` generated by the filtration elements is finitely generated.
|
Ideal.iInf_pow_eq_bot_of_localRing
theorem Ideal.iInf_pow_eq_bot_of_localRing :
∀ {R : Type u} [inst : CommRing R] (I : Ideal R) [inst_1 : IsNoetherianRing R] [inst_2 : LocalRing R],
I ≠ ⊤ → ⨅ i, I ^ i = ⊥
**Krull's Intersection Theorem** for Noetherian local rings states that for any given type `R` which is a commutative ring, any given ideal `I` of `R`, provided `R` is a Noetherian ring and a local ring, and `I` is not the unit ideal, the intersection of all powers of `I` (i.e., `I` to the power of `i` for all `i`) is the zero ideal. In other words, if we keep multiplying the ideal `I` by itself indefinitely, the only element that we can guarantee will be present in every generated ideal is the zero element. This theorem holds an important position in the field of commutative algebra.
More concisely: In a commutative Noetherian local ring, any non-unit ideal intersects all its powers to form the zero ideal.
|
Ideal.exists_pow_inf_eq_pow_smul
theorem Ideal.exists_pow_inf_eq_pow_smul :
∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
[inst_3 : IsNoetherianRing R] [inst_4 : Module.Finite R M] (N : Submodule R M),
∃ k, ∀ n ≥ k, I ^ n • ⊤ ⊓ N = I ^ (n - k) • (I ^ k • ⊤ ⊓ N)
The "Artin-Rees lemma" theorem states that for any commutative ring `R`, additive commutative group `M`, module structure over `R` on `M`, ideal `I` in `R`, and `R` is a Noetherian ring and `M` is a finitely generated `R`-module, and a submodule `N` of `M`, there exists a natural number `k` such that for all `n` greater than or equal to `k`, the `nth` power of the ideal `I` generated in the top module `M` intersected with the submodule `N` is equal to the (`n-k`)'th power of the ideal `I` generated in the submodule of `M` which is intersection of `k`-th power of `I`-generated `M` and `N`. This is a formal statement of the "Artin-Rees lemma" in the language of commutative algebra.
More concisely: For any Noetherian ring `R`, finitely generated `R`-module `M`, ideal `I` in `R`, and submodule `N` of `M`, there exists a natural number `k` such that for all `n >= k`, $(I^n \cap N) = I^{n-k} (I^k \cap N)$.
|
Ideal.iInf_pow_eq_bot_of_isDomain
theorem Ideal.iInf_pow_eq_bot_of_isDomain :
∀ {R : Type u} [inst : CommRing R] (I : Ideal R) [inst_1 : IsNoetherianRing R] [inst_2 : IsDomain R],
I ≠ ⊤ → ⨅ i, I ^ i = ⊥
**Krull's Intersection Theorem** for Noetherian domains can be described as follows: Given a commutative ring `R` which is a Noetherian ring as well as a domain, and an ideal `I` in `R` that is not the whole ring, the theorem states that the intersection of all powers of `I` equals the zero ideal. In other words, for every natural number `i`, if you take the `i`-th power of `I` and then form the intersection of all these ideals, you get the zero ideal. In Noetherian rings, the power set of an ideal eventually stabilizes, and in a domain, this leads to the intersection of all powers of an ideal being the zero ideal, reflecting the core idea of Krull's Intersection Theorem.
More concisely: In a commutative Noetherian domain `R` with ideal `I` not equal to `R`, the intersection of all powers of `I` equals the zero ideal.
|
Ideal.isIdempotentElem_iff_eq_bot_or_top_of_localRing
theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_localRing :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : LocalRing R] (I : Ideal R),
IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
This theorem states that for any commutative ring 'R' which is both a Noetherian and a Local ring, an ideal 'I' in 'R' is idempotent (that is, when you square it, you get the ideal back) if and only if the ideal 'I' is either bot (the zero ideal) or top (the unit ideal). This is a special case of a more general principle observable in integral domains.
More concisely: In a commutative Noetherian and local ring, an ideal is idempotent if and only if it is the zero or unit ideal.
|