Primary decomposition of torsion subgroups

For a nonzero natural number N, the prime-power factors p ^ N.factorization p are pairwise coprime and multiply to N. Consequently the N-torsion subgroup of an additive commutative group is the internal direct sum of its p ^ N.factorization p-torsion subgroups, one for each prime factor p of N. This reduces questions about N-torsion to prime-power torsion.

Main results

• TauCeti.AddSubgroup.torsionBy_primeFactors_isInternal: the N-torsion subgroup is the internal direct sum of its primary components.

theorem TauCeti.AddSubgroup.torsionBy_primeFactors_isInternal {A : Type u_1} [AddCommGroup A] (N : ℕ) (hN : N ≠ 0) : DirectSum.IsInternal fun (p : ↥N.primeFactors) => Submodule.torsionBy ℤ ↥(AddSubgroup.torsionBy A ↑N) ↑(↑p ^ N.factorization ↑p)

The primary torsion subgroups form an internal direct sum of the ambient N-torsion subgroup.