Dual groups of finite abelian groups
TheoremA finite abelian group is isomorphic to its dual group#✓fully proved
Every finite abelian group \(A\) is isomorphic to its dual group, the group of characters of \(A\) under pointwise multiplication, where a character of \(A\) is a map \(\chi : A \to \mathbb{C}\) with \(\chi(0) = 1\) and \(\chi(a + a') = \chi(a)\chi(a')\) for all \(a, a' \in A\).
Proof: Use the structure theorem to write \(A\) as a direct sum of finite cyclic groups, identify each cyclic group \(\mathbb{Z}/n\mathbb{Z}\) with its dual group, and transport characters along the decomposition. This is the proof of Conrad's Theorem 3.13: the cyclic case, then products of cyclic groups.
public theorem finite_abelian_dual_iso (α : Type*) [AddCommGroup α]
[Finite α] : Nonempty (α ≃+ AddChar α ℂ)Sources
- K. Conrad, Characters of finite abelian groups, https://kconrad.math.uconn.edu/blurbs/grouptheory/charthy.pdf, Theorem 3.13.
TheoremCharacters of a product of abelian groups#✓fully proved
For all abelian groups \(A\) and \(B\), the group of characters of \(A \times B\) is isomorphic to the product of the character groups of \(A\) and \(B\). Here a character of \(A\) is a map \(\chi : A \to \mathbb{C}\) with \(\chi(0) = 1\) and \(\chi(a + a') = \chi(a)\chi(a')\) for all \(a, a' \in A\), and the characters of \(A\) form a group under pointwise multiplication.
Proof: Restrict a character along the two coordinate inclusions, with inverse \((\chi_1, \chi_2) \mapsto ((x, y) \mapsto \chi_1(x)\chi_2(y))\). Conrad's Lemma 3.12 uses the same restriction map for finite groups and concludes by counting; the explicit inverse removes the finiteness assumption.
public theorem dual_prod (α β : Type*) [AddCommGroup α] [AddCommGroup β] :
Nonempty (AddChar (α × β) ℂ ≃+ (AddChar α ℂ × AddChar β ℂ))Sources
- K. Conrad, Characters of finite abelian groups, https://kconrad.math.uconn.edu/blurbs/grouptheory/charthy.pdf, Lemma 3.12.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.