Quaternion Groups #
We define the (generalised) quaternion groups QuaternionGroup 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 QuaternionGroup 2 is isomorphic to
the unit integral quaternions (Quaternion ℤ)ˣ.
Main definition #
QuaternionGroup n: The (generalised) quaternion group of order 4n.
Implementation notes #
This file is heavily based on DihedralGroup 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 QuaternionGroup also for n = 0 and
n = 1. QuaternionGroup 0 is isomorphic to the infinite dihedral group, while
QuaternionGroup 1 is isomorphic to a cyclic group of order 4.
References #
TODO #
Show that QuaternionGroup 2 ≃* (Quaternion ℤ)ˣ.
The (generalised) quaternion group QuaternionGroup 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$.
- a: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
- xa: {n : ℕ} → ZMod (2 * n) → QuaternionGroup n
Instances For
Equations
- instDecidableEqQuaternionGroup = decEqQuaternionGroup✝
Equations
- QuaternionGroup.instInhabited = { default := QuaternionGroup.one }
The group structure on QuaternionGroup n.
The special case that more or less by definition QuaternionGroup 0 is isomorphic to the
infinite dihedral group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If 0 < n, then QuaternionGroup n is a finite group.
If 0 < n, then QuaternionGroup 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.