English
If a ∈ R is irreducible in a PID and M is a finitely generated R-module torsion with respect to a, then the a-torsion submodule torsionBy R M a is semisimple.
Русский
Если a ∈ R ирредуцируем в ПИД и M — конечнопорожденный R-модуль, тождественный к a-тorsion, то torsionBy R M a является полусемисимпл.
LaTeX
$$$\\mathrm{IsSemisimpleModule}\\ R\\left(\\mathrm{torsionBy}\\ R\\ M\\ a\\right)$$$
Lean4
/-- 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 isInternal_prime_power_torsion_of_pid [DecidableEq (Ideal R)] [Module.Finite R M] (hM : Module.IsTorsion R M) :
DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
torsionBy R M (IsPrincipal.generator (p : Ideal R) ^ (factors (⊤ : Submodule R M).annihilator).count ↑p) :=
by
convert isInternal_prime_power_torsion hM
rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
Ideal.span_singleton_generator]
