Rank-two finite abelian groups of prime-power exponent #
A finite abelian group killed by p ^ k, of order p ^ (2 * k), and with exactly p ^ 2
elements killed by p is the product of two cyclic groups of order p ^ k. This is the
rank-two prime-power case of the structure theorem for finite abelian groups.
The criterion is useful when the total order and the first torsion layer are easier to count than explicit generators. It determines both the number of cyclic factors and their exponents.
Main result #
TauCeti.AddCommGroup.nonempty_addEquiv_prod_zmod_primePow: the rank-two characterisation.
theorem
TauCeti.AddCommGroup.nonempty_addEquiv_prod_zmod_primePow
{G : Type u_1}
[AddCommGroup G]
{p k : ℕ}
(hp : Nat.Prime p)
(hpow : ∀ (x : G), p ^ k • x = 0)
(hcard : Nat.card G = p ^ (2 * k))
(hcardp : Nat.card ↥(AddSubgroup.torsionBy G ↑p) = p ^ 2)
:
Rank-two prime-power characterisation. An abelian group killed by p ^ k, with
order p ^ (2 * k) and p ^ 2 elements killed by p, is additively equivalent to
ZMod (p ^ k) × ZMod (p ^ k).