English
Over a Dedekind domain, a torsion module is internal direct sum of its p^e-torsion parts indexed by prime ideals of the decomposition of the annihilator; this is a refinement of the earlier isInternal principle.
Русский
В области Дедекондаtorsion-модуля представляется как внутренний прямой сумма его p^e-тorsion частей по разложению аннигиляторa на простые идеалы.
LaTeX
$$$\mathrm{DirectSum.IsInternal}\; (p \mapsto {\mathrm torsionBySet})$$$
Lean4
/-- 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. -/
theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal [DecidableEq (Ideal R)] {I : Ideal R} (hI : I ≠ ⊥)
(hM : Module.IsTorsionBySet R M I) :
DirectSum.IsInternal fun p : (factors I).toFinset => torsionBySet R M (p ^ (factors I).count ↑p : Ideal R) :=
by
let P := factors I
have prime_of_mem := fun p (hp : p ∈ P.toFinset) => prime_of_factor p (Multiset.mem_toFinset.mp hp)
apply torsionBySet_isInternal (p := fun p => p ^ P.count p) _
· convert hM
rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_prime_pow_eq_prod, ← Finset.prod_multiset_count, ← associated_iff_eq]
· exact factors_prod hI
· exact prime_of_mem
· exact fun _ _ _ _ ij => ij
· intro p hp q hq pq; dsimp
rw [irreducible_pow_sup]
· suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
rw [Multiset.count_eq_zero, normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
Multiset.mem_replicate]
exact fun H => pq <| H.2.trans <| normalize_eq q
· rw [← Ideal.zero_eq_bot]; apply pow_ne_zero; exact (prime_of_mem q hq).ne_zero
· exact (prime_of_mem p hp).irreducible
