Primary decomposition of finite abelian groups

This file packages the canonical decomposition of a finite abelian group as the product of its prime-primary components. The equivalence sends a tuple of primary elements to their sum in the ambient group. It also defines the part of an additive subgroup lying in one primary component.

The proof follows the cardinality argument used by Mathlib's Sylow.directProductOfNormal: primary components for distinct primes have coprime cardinalities, and the product of those cardinalities is the cardinality of the group. We pass through the multiplicative avatar of the group only to reuse Sylow.card_eq_multiplicity; the resulting equivalence is entirely additive and uses Mathlib's canonical AddCommGroup.primaryComponent subgroups.

Main results

• AddSubgroup.primaryPart: the part of a subgroup in one primary component.
• TauCeti.AddCommGroup.primaryDecomposition: a finite abelian group is additively equivalent to the product of its prime-primary components.
• TauCeti.AddCommGroup.primaryDecomposition_apply: the equivalence is the sum of the component inclusions.

References

• D. Gorenstein, Finite Groups, Chapter 1.

This is the group-theoretic input to the primary-decomposition part of Layer 3 of TauCetiRoadmap/IntegralLattices/README.md.

def AddSubgroup.primaryPart {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) (p : ℕ) : AddSubgroup ↥(AddCommGroup.primaryComponent G p)

The p-primary part of H, regarded as a subgroup of the ambient p-primary component.

Equations

• H.primaryPart p = AddSubgroup.comap (AddCommGroup.primaryComponent G p).subtype H

@[simp]

theorem AddSubgroup.mem_primaryPart_iff {G : Type u_1} [AddCommGroup G] (H : AddSubgroup G) (p : ℕ) (x : ↥(AddCommGroup.primaryComponent G p)) : x ∈ H.primaryPart p ↔ ↑x ∈ H

noncomputable def TauCeti.AddCommGroup.primaryDecomposition (A : Type u) [AddCommGroup A] [Finite A] : ((p : ↥(Nat.card A).primeFactors) → ↥(AddCommGroup.primaryComponent A ↑p)) ≃+ A

A finite abelian group is canonically the direct product of its prime-primary components.

Equations

• TauCeti.AddCommGroup.primaryDecomposition A = AddEquiv.ofBijective (TauCeti.AddCommGroup.primaryDecompositionHom✝ A) ⋯

@[simp]

theorem TauCeti.AddCommGroup.primaryDecomposition_apply (A : Type u) [AddCommGroup A] [Finite A] (x : (p : ↥(Nat.card A).primeFactors) → ↥(AddCommGroup.primaryComponent A ↑p)) : (primaryDecomposition A) x = ∑ p : ↥(Nat.card A).primeFactors, ↑(x p)

The canonical primary decomposition maps a tuple to the sum of its components.