# 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.

## TODO #

Show that QuaternionGroup 2 ≃* (Quaternion ℤ)ˣ.

inductive QuaternionGroup (n : ) :

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$.

Instances For
instance instDecidableEqQuaternionGroup :
{n : } →
Equations
• instDecidableEqQuaternionGroup = decEqQuaternionGroup✝
Equations
• QuaternionGroup.instInhabited = { default := QuaternionGroup.one }

The group structure on QuaternionGroup n.

Equations
• QuaternionGroup.instGroup =
@[simp]
theorem QuaternionGroup.a_mul_a {n : } (i : ZMod (2 * n)) (j : ZMod (2 * n)) :
@[simp]
theorem QuaternionGroup.a_mul_xa {n : } (i : ZMod (2 * n)) (j : ZMod (2 * n)) :
@[simp]
theorem QuaternionGroup.xa_mul_a {n : } (i : ZMod (2 * n)) (j : ZMod (2 * n)) :
@[simp]
theorem QuaternionGroup.xa_mul_xa {n : } (i : ZMod (2 * n)) (j : ZMod (2 * n)) :
= QuaternionGroup.a (n + j - i)

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.

Equations
Equations
• =
theorem QuaternionGroup.card {n : } [] :
= 4 * n

If 0 < n, then QuaternionGroup n has 4n elements.

@[simp]
theorem QuaternionGroup.a_one_pow {n : } (k : ) :
theorem QuaternionGroup.a_one_pow_n {n : } :
^ (2 * n) = 1
@[simp]
theorem QuaternionGroup.xa_sq {n : } (i : ZMod (2 * n)) :
@[simp]
theorem QuaternionGroup.xa_pow_four {n : } (i : ZMod (2 * n)) :
= 1
@[simp]
theorem QuaternionGroup.orderOf_xa {n : } [] (i : ZMod (2 * n)) :

If 0 < n, then xa i has order 4.

In the special case n = 1, Quaternion 1 is a cyclic group (of order 4).

@[simp]
theorem QuaternionGroup.orderOf_a_one {n : } :
= 2 * n

If 0 < n, then a 1 has order 2 * n.

theorem QuaternionGroup.orderOf_a {n : } [] (i : ZMod (2 * n)) :
= 2 * n / (2 * n).gcd i.val

If 0 < n, then a i has order (2 * n) / gcd (2 * n) i.

theorem QuaternionGroup.exponent {n : } :
= 2 * lcm n 2