mathlib3 documentation

algebra.module.pid

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 #

Notation #

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

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_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.

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) :
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
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
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.

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.

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.