Structure of finitely generated modules over a PID

Main statements

• Module.equiv_directSum_of_isTorsion : A finitely generated torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p i ^ e i) where the p i ^ e i are prime powers.
• Module.equiv_free_prod_directSum : A finitely generated module over a PID is isomorphic to the product of a free module (its torsion free part) and a direct sum of the form above (its torsion submodule).

Notation

• R is a PID and M is a (finitely generated for main statements) R-module, with additional torsion hypotheses in the intermediate lemmas.
• p is an irreducible element of R or a tuple of these.

Implementation details

We first prove (Submodule.isInternal_prime_power_torsion_of_pid) that a finitely generated torsion module is the internal direct sum of its p i ^ e i-torsion submodules for some (finitely many) prime powers p i ^ e i. This is proved in more generality for a Dedekind domain at Submodule.isInternal_prime_power_torsion.

Then we treat the case of a p ^ ∞-torsion module (that is, a module where all elements are cancelled by scalar multiplication by some power of p) and apply it to the p i ^ e i-torsion submodules (that are p i ^ ∞-torsion) to get the result for torsion modules.

Then we get the general result using that a torsion free module is free (which has been proved at Module.free_of_finite_type_torsion_free' at LinearAlgebra.FreeModule.PID.)

Tags

Finitely generated module, principal ideal domain, classification, structure theorem

theorem Submodule.isSemisimple_torsionBy_of_irreducible {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] {a : R} (h : Irreducible a) : IsSemisimpleModule R ↥(torsionBy R M a)

theorem Submodule.isInternal_prime_power_torsion_of_pid {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] [DecidableEq (Ideal R)] [Module.Finite R M] (hM : Module.IsTorsion R M) : DirectSum.IsInternal fun (p : { x : Ideal R // x ∈ (UniqueFactorizationMonoid.factors ⊤.annihilator).toFinset }) => torsionBy R M (IsPrincipal.generator ↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors ⊤.annihilator))

A finitely generated torsion module over a PID is an internal direct sum of its p i ^ e i-torsion submodules for some primes p i and numbers e i.

theorem Submodule.exists_isInternal_prime_power_torsion_of_pid {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] [Module.Finite R M] (hM : Module.IsTorsion R M) : ∃ (ι : Type u) (x : Fintype ι) (x : DecidableEq ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ), DirectSum.IsInternal fun (i : ι) => torsionBy R M (p i ^ e i)

A finitely generated torsion module over a PID is an internal direct sum of its p i ^ e i-torsion submodules for some primes p i and numbers e i.

theorem Ideal.torsionOf_eq_span_pow_pOrder {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] {p : R} (hp : Irreducible p) (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] (x : M) : torsionOf R M x = span {p ^ Submodule.pOrder hM x}

theorem Module.p_pow_smul_lift {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] {p : R} (hp : Irreducible p) (hM : IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] {x y : M} {k : ℕ} (hM' : IsTorsionBy R M (p ^ Submodule.pOrder hM y)) (h : p ^ k • x ∈ Submodule.span R {y}) : ∃ (a : R), p ^ k • x = p ^ k • a • y

theorem Module.exists_smul_eq_zero_and_mk_eq {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] {p : R} (hp : Irreducible p) (hM : IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] {z : M} (hz : IsTorsionBy R M (p ^ Submodule.pOrder hM z)) {k : ℕ} (f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}) : ∃ (x : M), p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1

theorem Module.torsion_by_prime_power_decomposition {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] {p : R} (hp : Irreducible p) (hM : IsTorsion' M ↥(Submonoid.powers p)) [h' : Module.Finite R M] : ∃ (d : ℕ) (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] DirectSum (Fin d) fun (i : Fin d) => R ⧸ Submodule.span R {p ^ k i})

A finitely generated p ^ ∞-torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p ^ e i) for some e i.

theorem Module.equiv_directSum_of_isTorsion {R : Type u} [CommRing R] [IsPrincipalIdealRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsDomain R] [h' : Module.Finite R M] (hM : IsTorsion R M) : ∃ (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ), Nonempty (M ≃ₗ[R] DirectSum ι fun (i : ι) => R ⧸ Submodule.span R {p i ^ e i})

A finitely generated torsion module over a PID is isomorphic to a direct sum of some R ⧸ R ∙ (p i ^ e i) where the p i ^ e i are prime powers.

theorem Module.equiv_free_prod_directSum (R : Type u) [CommRing R] [IsPrincipalIdealRing R] (M : Type v) [AddCommGroup M] [Module R M] [IsDomain R] [h' : Module.Finite R M] : ∃ (n : ℕ) (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ), Nonempty (M ≃ₗ[R] (Fin n →₀ R) × DirectSum ι fun (i : ι) => R ⧸ Submodule.span R {p i ^ e i})

Structure theorem of finitely generated modules over a PID : A finitely generated module over a PID is isomorphic to the product of a free module and a direct sum of some R ⧸ R ∙ (p i ^ e i) where the p i ^ e i are prime powers.

theorem Module.exists_ker_toSpanSingleton_eq_annihilator (R : Type u) [CommRing R] [IsPrincipalIdealRing R] (M : Type v) [AddCommGroup M] [Module R M] [IsDomain R] [Module.Finite R M] : ∃ (x : M), LinearMap.ker (LinearMap.toSpanSingleton R M x) = annihilator R M