Submodule.isInternal_prime_power_torsion_of_pid
theorem Submodule.isInternal_prime_power_torsion_of_pid :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] {M : Type v}
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module.Finite R M],
Module.IsTorsion R M →
DirectSum.IsInternal fun p =>
Submodule.torsionBy R M
(Submodule.IsPrincipal.generator ↑p ^
Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))
This theorem states that for a finitely generated torsion module over a Principal Ideal Domain (PID), the module can be written as an internal direct sum of its torsion submodules. The torsion submodules are each scaled by a prime number raised to a certain power. In other words, each element of the module is annihilated by a power of some prime number, and these prime powers uniquely distinguish the direct summands. The prime numbers and their powers are determined by the prime factorization of the annihilator of the module.
More concisely: A finitely generated torsion module over a Principal Ideal Domain (PID) is isomorphic to the internal direct sum of its torsion submodules, each scaled by a power of a prime number that divides the annihilator of the module.
|
Module.equiv_free_prod_directSum
theorem Module.equiv_free_prod_directSum :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] {N : Type (max u v)}
[inst_3 : AddCommGroup N] [inst_4 : Module R N] [h' : Module.Finite R N],
∃ n ι x p,
∃ (_ : ∀ (i : ι), Irreducible (p i)),
∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun i => R ⧸ Submodule.span R {p i ^ e i})
This theorem is the Structure Theorem for Finitely Generated Modules over a Principal Ideal Domain (PID). It says that every finitely generated module over a PID is isomorphic to the product of a free module and a direct sum of quotient rings, specifically, `R ⧸ R ∙ (p i ^ e i)`, where `p i ^ e i` are powers of irreducible elements. The theorem not only states the existence of such an isomorphism, but also provides a formal construction of the isomorphism using a given set of generators.
More concisely: Every finitely generated module over a principal ideal domain is isomorphic to a free module followed by a direct sum of quotient rings of the domain by powers of its irreducible elements.
|
Module.equiv_directSum_of_isTorsion
theorem Module.equiv_directSum_of_isTorsion :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] {N : Type (max u v)}
[inst_3 : AddCommGroup N] [inst_4 : Module R N] [h' : Module.Finite R N],
Module.IsTorsion R N →
∃ ι x p,
∃ (_ : ∀ (i : ι), Irreducible (p i)),
∃ e, Nonempty (N ≃ₗ[R] DirectSum ι fun i => R ⧸ Submodule.span R {p i ^ e i})
The theorem `Module.equiv_directSum_of_isTorsion` states that for a given finitely generated torsion module over a Principal Ideal Domain (PID), there exists an isomorphism to a direct sum of quotient modules of the form `R ⧸ R ∙ (p i ^ e i)`, where `p i ^ e i` are prime powers. In this isomorphism, `R` is our PID, `N` is our torsion module, and `ι` is the index set for our direct sum. The map `p` assigns to each index `i` an irreducible element of `R`, and `e` is a function that assigns to each index `i` a nonnegative integer. This result presents the structure of finitely generated torsion modules over a PID in terms of simpler components.
More concisely: A finitely generated torsion module over a Principal Ideal Domain (PID) is isomorphic to a direct sum of quotient modules of the form `R ⧸ R ∙ (p i ^ e i)`, where `p i` are irreducible elements and `e i` are nonnegative integers.
|
Module.torsion_by_prime_power_decomposition
theorem Module.torsion_by_prime_power_decomposition :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] {N : Type (max u v)}
[inst_3 : AddCommGroup N] [inst_4 : Module R N] {p : R},
Irreducible p →
Module.IsTorsion' N ↥(Submonoid.powers p) →
∀ [h' : Module.Finite R N],
∃ d k, Nonempty (N ≃ₗ[R] DirectSum (Fin d) fun i => R ⧸ Submodule.span R {p ^ k i})
This theorem states that for any commutative ring `R` which is also a domain and a principal ideal ring, and `N` which is an additive commutative group and a `R`-module, given `p` which is an irreducible element of `R`, if `N` is a `p ^ ∞`-torsion module, and `N` is finitely generated over `R`, then there exist integers `d` and `k` such that `N` is isomorphic (as an `R`-module) to the direct sum of `R` quotiented by the submodule generated by `p ^ (k i)` for each `i` in the finite set `{0, 1, ..., d-1}`.
In more layman's terms, it says that a finitely generated module, where every element is killed by some power of a given irreducible element, can be decomposed into a direct sum of simpler objects, namely quotients of the ring by powers of the irreducible element.
More concisely: For any commutative domain and principal ideal ring `R`, finitely generated `R`-module `N` that is `p^∞`-torsion for some irreducible element `p` in `R`, there exists integers `d` and `k` such that `N` is isomorphic to the direct sum of `d` copies of `R/p^(ki)`.
|
Submodule.exists_isInternal_prime_power_torsion_of_pid
theorem Submodule.exists_isInternal_prime_power_torsion_of_pid :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] {M : Type v}
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module.Finite R M],
Module.IsTorsion R M →
∃ ι x x p,
∃ (_ : ∀ (i : ι), Irreducible (p i)),
∃ e, DirectSum.IsInternal fun i => Submodule.torsionBy R M (p i ^ e i)
The theorem states that for a given finitely generated torsion module over a principal ideal domain (PID), it is possible to express it as an internal direct sum of its torsion submodules. More specifically, these torsion submodules are scaled by the power of a corresponding prime number (`p i ^ e i`). The `p i` represents a set of irreducible elements (primes) in the PID, and `e i` are some numbers. In other words, given the conditions, the structure of a finitely generated torsion module can be decomposed into a direct sum of certain torsion submodules, each associated with a specific prime number raised to a certain power.
More concisely: Given a finitely generated torsion module over a principal ideal domain, it can be expressed as an internal direct sum of its torsion submodules, each scaled by the power of a corresponding irreducible element in the domain.
|