Uniqueness of elementary divisors with a fixed base #
An additive equivalence between finite products of ZMod (b ^ e i), with b > 1 and positive
exponents, determines the exponents up to reindexing. For a prime b = p the exponents are the
elementary divisors of a finite abelian p-group, so this is the uniqueness clause of the
classification of finite abelian p-groups; it also identifies the finite factor of a topologically
finitely generated abelian pro-p group up to reindexing of its cyclic summands.
The exponents are required to be positive because a factor ZMod (b ^ 0) is trivial and leaves
the product unchanged.
Main results #
ZMod.exists_equiv_exponents_of_pi_pow_addEquiv: two such products have the same exponents after a bijection of their finite index types.
theorem
ZMod.exists_equiv_exponents_of_pi_pow_addEquiv
{b : ℕ}
(hb : 1 < b)
{ι : Type u_1}
{κ : Type u_2}
[Finite ι]
[Finite κ]
(e : ι → ℕ)
(e' : κ → ℕ)
(he : ∀ (i : ι), 0 < e i)
(he' : ∀ (j : κ), 0 < e' j)
(f : ((i : ι) → ZMod (b ^ e i)) ≃+ ((j : κ) → ZMod (b ^ e' j)))
:
Finite products of nontrivial cyclic groups with orders powers of the same base b > 1
have uniquely determined exponents up to reindexing. Primality of the base is not needed.