Documentation

Mathlib.GroupTheory.SpecificGroups.Quaternion

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 $⟨ a, x | a^{2 n} = 1, x^{2} = a^{n}, x^{- 1} a x = a^{- 1} ⟩$ . 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 ℤ)ˣ.

inductive QuaternionGroup (n : ℕ) :

The (generalised) quaternion group QuaternionGroup n of order 4n. It can be defined by the presentation $⟨ a, x | a^{2 n} = 1, x^{2} = a^{n}, x^{- 1} a x = a^{- 1} ⟩$ . 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

instance instDecidableEqQuaternionGroup {n✝ : ℕ} :

DecidableEq (QuaternionGroup n✝)

Equations

instDecidableEqQuaternionGroup = decEqQuaternionGroup✝

instance QuaternionGroup.instInhabited {n : ℕ} :

Inhabited (QuaternionGroup n)

Equations

QuaternionGroup.instInhabited = { default := QuaternionGroup.one✝ }

instance QuaternionGroup.instGroup {n : ℕ} :

Group (QuaternionGroup n)

The group structure on QuaternionGroup n.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionGroup.a_mul_a {n : ℕ} (i j : ZMod (2 * n)) :

a i * a j = a (i + j)

@[simp]

theorem QuaternionGroup.a_mul_xa {n : ℕ} (i j : ZMod (2 * n)) :

a i * xa j = xa (j - i)

@[simp]

theorem QuaternionGroup.xa_mul_a {n : ℕ} (i j : ZMod (2 * n)) :

xa i * a j = xa (i + j)

@[simp]

theorem QuaternionGroup.xa_mul_xa {n : ℕ} (i j : ZMod (2 * n)) :

xa i * xa j = a (↑n + j - i)

@[simp]

theorem QuaternionGroup.a_zero {n : ℕ} :

a 0 = 1

theorem QuaternionGroup.one_def {n : ℕ} :

1 = a 0

def QuaternionGroup.quaternionGroupZeroEquivDihedralGroupZero :

QuaternionGroup 0 ≃* DihedralGroup 0

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.

instance QuaternionGroup.instFintypeOfNeZeroNat {n : ℕ} [NeZero n] :

Fintype (QuaternionGroup n)

If 0 < n, then QuaternionGroup n is a finite group.

Equations

QuaternionGroup.instFintypeOfNeZeroNat = Fintype.ofEquiv (ZMod (2 * n) ⊕ ZMod (2 * n)) QuaternionGroup.fintypeHelper✝

instance QuaternionGroup.instNontrivial {n : ℕ} :

Nontrivial (QuaternionGroup n)

theorem QuaternionGroup.card {n : ℕ} [NeZero n] :

Fintype.card (QuaternionGroup n) = 4 * n

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

@[simp]

theorem QuaternionGroup.a_one_pow {n : ℕ} (k : ℕ) :

a 1 ^ k = a ↑k

theorem QuaternionGroup.a_one_pow_n {n : ℕ} :

a 1 ^ (2 * n) = 1

@[simp]

theorem QuaternionGroup.xa_sq {n : ℕ} (i : ZMod (2 * n)) :

xa i ^ 2 = a ↑n

@[simp]

theorem QuaternionGroup.xa_pow_four {n : ℕ} (i : ZMod (2 * n)) :

xa i ^ 4 = 1

@[simp]

theorem QuaternionGroup.orderOf_xa {n : ℕ} [NeZero n] (i : ZMod (2 * n)) :

orderOf (xa i) = 4

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

theorem QuaternionGroup.quaternionGroup_one_isCyclic :

IsCyclic (QuaternionGroup 1)

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

@[simp]

theorem QuaternionGroup.orderOf_a_one {n : ℕ} :

orderOf (a 1) = 2 * n

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

theorem QuaternionGroup.orderOf_a {n : ℕ} [NeZero n] (i : ZMod (2 * n)) :

orderOf (a i) = 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 : ℕ} :

Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2