Structure of finitely generated modules over a PID #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main statements #

module.equiv_direct_sum_of_is_torsion : 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_direct_sum : 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.
N is a R-module lying over a higher type universe than R. This assumption is needed on the final statement for technical reasons.
p is an irreducible element of R or a tuple of these.

Implementation details #

We first prove (submodule.is_internal_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.is_internal_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 linear_algebra/free_module/pid.lean.)

Tags #

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

source

theorem submodule.is_internal_prime_power_torsion_of_pid {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type v} [add_comm_group M] [module R M] [module.finite R M] (hM : module.is_torsion R M) :

direct_sum.is_internal (λ (p : ↥((unique_factorization_monoid.factors ⊤.annihilator).to_finset)), submodule.torsion_by R M (submodule.is_principal.generator ↑p ^ multiset.count ↑p (unique_factorization_monoid.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.

source

theorem submodule.exists_is_internal_prime_power_torsion_of_pid {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type v} [add_comm_group M] [module R M] [module.finite R M] (hM : module.is_torsion R M) :

∃ (ι : Type u) [_inst_9 : fintype ι] [_inst_10 : decidable_eq ι] (p : ι → R) (h : ∀ (i : ι), irreducible (p i)) (e : ι → ℕ), direct_sum.is_internal (λ (i : ι), submodule.torsion_by 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.

source

theorem ideal.torsion_of_eq_span_pow_p_order {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type v} [add_comm_group M] [module R M] {p : R} (hp : irreducible p) (hM : module.is_torsion' M ↥(submonoid.powers p)) [dec : Π (x : M), decidable (x = 0)] (x : M) :

ideal.torsion_of R M x = ideal.span {p ^ submodule.p_order hM x}

source

theorem module.p_pow_smul_lift {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type v} [add_comm_group M] [module R M] {p : R} (hp : irreducible p) (hM : module.is_torsion' M ↥(submonoid.powers p)) [dec : Π (x : M), decidable (x = 0)] {x y : M} {k : ℕ} (hM' : module.is_torsion_by R M (p ^ submodule.p_order hM y)) (h : p ^ k • x ∈ submodule.span R {y}) :

∃ (a : R), p ^ k • x = p ^ k • a • y

source

theorem module.exists_smul_eq_zero_and_mk_eq {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type v} [add_comm_group M] [module R M] {p : R} (hp : irreducible p) (hM : module.is_torsion' M ↥(submonoid.powers p)) [dec : Π (x : M), decidable (x = 0)] {z : M} (hz : module.is_torsion_by R M (p ^ submodule.p_order 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

source

theorem module.torsion_by_prime_power_decomposition {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {N : Type (max u v)} [add_comm_group N] [module R N] {p : R} (hp : irreducible p) (hN : module.is_torsion' N ↥(submonoid.powers p)) [h' : module.finite R N] :

∃ (d : ℕ) (k : fin d → ℕ), nonempty (N ≃ₗ[R] direct_sum (fin d) (λ (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.

source

theorem module.equiv_direct_sum_of_is_torsion {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {N : Type (max u v)} [add_comm_group N] [module R N] [h' : module.finite R N] (hN : module.is_torsion R N) :

∃ (ι : Type u) [_inst_8 : fintype ι] (p : ι → R) (h : ∀ (i : ι), irreducible (p i)) (e : ι → ℕ), nonempty (N ≃ₗ[R] direct_sum ι (λ (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.

source

theorem module.equiv_free_prod_direct_sum {R : Type u} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {N : Type (max u v)} [add_comm_group N] [module R N] [h' : module.finite R N] :

∃ (n : ℕ) (ι : Type u) [_inst_8 : fintype ι] (p : ι → R) (h : ∀ (i : ι), irreducible (p i)) (e : ι → ℕ), nonempty (N ≃ₗ[R] (fin n →₀ R) × direct_sum ι (λ (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.