Submodule.exists_isInternal_prime_power_torsion
theorem Submodule.exists_isInternal_prime_power_torsion :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {M : Type v} [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : IsDedekindDomain R] [inst_5 : Module.Finite R M],
Module.IsTorsion R M →
∃ P x, ∃ (_ : ∀ p ∈ P, Prime p), ∃ e, DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ e p)
The theorem `Submodule.exists_isInternal_prime_power_torsion` states that for any finitely generated torsion module over a Dedekind domain, it can be expressed as an internal direct sum of its `-torsion` submodules, each determined by a prime ideal elevated to a certain power. More specifically, if `R` is a Dedekind domain and `M` is a finitely generated `R`-module such that every element of `M` is `a`-torsion for some non-zero-divisor `a`, then there exist a set `P` of prime ideals in `R`, a function `e` from `P` to natural numbers, such that `M` is the internal direct sum of the submodules of `M` consisting of `p^e(p)`-torsion elements, for each prime ideal `p` in `P`.
More concisely: Given a Dedekind domain `R` and a finitely generated `R`-module `M` such that every element of `M` is `a`-torsion for some non-zero-divisor `a`, there exist prime ideals `P` and natural numbers `e` such that `M` is the internal direct sum of its submodules of `p^e(p)`-torsion elements for each prime ideal `p` in `P`.
|
Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal
theorem Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {M : Type v} [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : IsDedekindDomain R] {I : Ideal R},
I ≠ ⊥ →
Module.IsTorsionBySet R M ↑I →
DirectSum.IsInternal fun p =>
Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors I))
This theorem states that over a Dedekind domain, a module that is `I`-torsion (i.e., every element of the module becomes null when multiplied by any element of the ideal `I`) can be expressed as an internal direct sum of its `p i ^ e i`-torsion submodules, where `I = ∏ i, p i ^ e i` is the unique decomposition of the ideal `I` in prime ideals.
In other words, if `R` is a Dedekind domain, `M` is a module over `R`, and `I` is a non-zero ideal of `R` such that every element of `M` becomes null when multiplied by any element of `I`, then `M` can be decomposed as the direct sum of submodules which are `p^e`-torsion, where `p` runs through the prime ideals appearing in the factorization of `I`, and `e` is the multiplicity of `p` in this factorization.
More concisely: A module over a Dedekind domain that is torsion with respect to an ideal is the internal direct sum of its submodules that are torsion with respect to each prime ideal in the factorization of the ideal.
|
Submodule.isInternal_prime_power_torsion
theorem Submodule.isInternal_prime_power_torsion :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {M : Type v} [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : IsDedekindDomain R] [inst_5 : Module.Finite R M],
Module.IsTorsion R M →
DirectSum.IsInternal fun p =>
Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
This theorem states that for a finitely generated torsion module over a Dedekind domain, the module can be expressed as an internal direct sum of its `p^e`-torsion submodules. Here, `p` are prime factors of the annihilator of the whole module `(⊤ : Submodule R M)`, and `e` are the multiplicities of these prime factors. A torsion module is a module in which every element becomes zero when multiplied by some non-zero element of the ring. A `p^e`-torsion submodule is the set of all module elements that become zero when multiplied by `p^e`. An internal direct sum is a way to decompose a module into a sum of submodules in a way that is "internal" to the module itself.
More concisely: A finitely generated torsion module over a Dedekind domain can be expressed as an internal direct sum of its submodules consisting of elements annihilated by distinct prime powers that generate the annihilator ideal.
|