Quaternion Groups #
We define the (generalised) quaternion groups quaternion_group n
of order 4n
, also known as
dicyclic groups, with elements a i
and xa i
for i : zmod n
. The (generalised) quaternion
groups can be defined by the presentation
$\langle a, x | a^{2n} = 1, x^2 = a^n, x^{-1}ax=a^{-1}\rangle$. We write a i
for
$a^i$ and xa i
for $x * a^i$. For n=2
the quaternion group quaternion_group 2
is isomorphic to
the unit integral quaternions (quaternion ℤ)ˣ
.
Main definition #
quaternion_group n
: The (generalised) quaternion group of order 4n
.
Implementation notes #
This file is heavily based on dihedral_group
by Shing Tak Lam.
In mathematics, the name "quaternion group" is reserved for the cases n ≥ 2
. Since it would be
inconvenient to carry around this condition we define quaternion_group
also for n = 0
and
n = 1
. quaternion_group 0
is isomorphic to the infinite dihedral group, while
quaternion_group 1
is isomorphic to a cyclic group of order 4
.
References #
TODO #
Show that quaternion_group 2 ≃* (quaternion ℤ)ˣ
.
- a : Π {n : ℕ}, zmod (2 * n) → quaternion_group n
- xa : Π {n : ℕ}, zmod (2 * n) → quaternion_group n
The (generalised) quaternion group quaternion_group n
of order 4n
. It can be defined by the
presentation $\langle a, x | a^{2n} = 1, x^2 = a^n, x^{-1}ax=a^{-1}\rangle$. We write a i
for
$a^i$ and xa i
for $x * a^i$.
Instances for quaternion_group
- quaternion_group.has_sizeof_inst
- quaternion_group.inhabited
- quaternion_group.group
- quaternion_group.fintype
- quaternion_group.nontrivial
Equations
- quaternion_group.inhabited = {default := one n}
The group structure on quaternion_group n
.
Equations
- quaternion_group.group = {mul := mul n, mul_assoc := _, one := one n, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default one mul quaternion_group.group._proof_4 quaternion_group.group._proof_5, npow_zero' := _, npow_succ' := _, inv := inv n, div := div_inv_monoid.div._default mul quaternion_group.group._proof_8 one quaternion_group.group._proof_9 quaternion_group.group._proof_10 (div_inv_monoid.npow._default one mul quaternion_group.group._proof_4 quaternion_group.group._proof_5) quaternion_group.group._proof_11 quaternion_group.group._proof_12 inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default mul quaternion_group.group._proof_14 one quaternion_group.group._proof_15 quaternion_group.group._proof_16 (div_inv_monoid.npow._default one mul quaternion_group.group._proof_4 quaternion_group.group._proof_5) quaternion_group.group._proof_17 quaternion_group.group._proof_18 inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
The special case that more or less by definition quaternion_group 0
is isomorphic to the
infinite dihedral group.
Equations
- quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero = {to_fun := λ (i : quaternion_group 0), i.rec_on dihedral_group.r dihedral_group.sr, inv_fun := λ (i : dihedral_group 0), quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero._match_1 i, left_inv := quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero._proof_1, right_inv := quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero._proof_2, map_mul' := quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero._proof_3}
- quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero._match_1 (dihedral_group.sr j) = quaternion_group.xa j
- quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero._match_1 (dihedral_group.r j) = quaternion_group.a j
If 0 < n
, then quaternion_group n
is a finite group.
Equations
- quaternion_group.fintype = fintype.of_equiv (zmod (2 * n) ⊕ zmod (2 * n)) fintype_helper
If 0 < n
, then quaternion_group n
has 4n
elements.
If 0 < n
, then xa i
has order 4.
In the special case n = 1
, quaternion 1
is a cyclic group (of order 4
).
If 0 < n
, then a 1
has order 2 * n
.