Modules over a Dedekind domain #

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

Over a Dedekind domain, a I-torsion module is the internal direct sum of its p i ^ e i-torsion submodules, where I = ∏ i, p i ^ e i is its unique decomposition in prime ideals. Therefore, as any finitely generated torsion module is I-torsion for some I, it is an internal direct sum of its p i ^ e i-torsion submodules for some prime ideals p i and numbers e i.

source

theorem submodule.is_internal_prime_power_torsion_of_is_torsion_by_ideal {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [add_comm_group M] [module R M] [is_dedekind_domain R] {I : ideal R} (hI : I ≠ ⊥) (hM : module.is_torsion_by_set R M ↑I) :

direct_sum.is_internal (λ (p : ↥((unique_factorization_monoid.factors I).to_finset)), submodule.torsion_by_set R M ↑(↑p ^ multiset.count ↑p (unique_factorization_monoid.factors I)))

Over a Dedekind domain, a I-torsion module is the internal direct sum of its p i ^ e i- torsion submodules, where I = ∏ i, p i ^ e i is its unique decomposition in prime ideals.

source

theorem submodule.is_internal_prime_power_torsion {R : Type u} [comm_ring R] [is_domain R] {M : Type v} [add_comm_group M] [module R M] [is_dedekind_domain R] [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_set R M ↑(↑p ^ multiset.count ↑p (unique_factorization_monoid.factors ⊤.annihilator)))

A finitely generated torsion module over a Dedekind domain is an internal direct sum of its p i ^ e i-torsion submodules where p i are factors of (⊤ : submodule R M).annihilator and e i are their multiplicities.

source

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

∃ (P : finset (ideal R)) [_inst_7 : decidable_eq ↥P] [_inst_8 : ∀ (p : ideal R), p ∈ P → prime p] (e : ↥P → ℕ), direct_sum.is_internal (λ (p : ↥P), submodule.torsion_by_set R M ↑(↑p ^ e p))

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