Theorems · Theorem · commutative algebra

Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal

∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {M : Type v} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {I : Ideal R},
  I ≠ ⊥ →
    Module.IsTorsionBySet R M ↑I →
      DirectSum.IsInternal fun p =>
        Submodule.torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (UniqueFactorizationMonoid.factors I))

Over a Dedekind domain, an 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.

Defined in

Mathlib.Algebra.Module.DedekindDomain

Cited by

1 results in Mathlib

Foundations

Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomainAddCommGroupModule