mathlib3 documentation

group_theory.specific_groups.quaternion

Quaternion Groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ℤ)ˣ.

source
@[protected, instance]
def quaternion_group.decidable_eq (n : ℕ) :
decidable_eq (quaternion_group n)
source
inductive quaternion_group (n : ℕ) :
Type

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
source
@[protected, instance]
def quaternion_group.inhabited {n : ℕ} :
inhabited (quaternion_group n)
Equations
source
@[protected, instance]
def quaternion_group.group {n : ℕ} :
group (quaternion_group 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 := _}
source
@[simp]
theorem quaternion_group.a_mul_a {n : ℕ} (i j : zmod (2 * n)) :
quaternion_group.a i * quaternion_group.a j = quaternion_group.a (i + j)
source
@[simp]
theorem quaternion_group.a_mul_xa {n : ℕ} (i j : zmod (2 * n)) :
quaternion_group.a i * quaternion_group.xa j = quaternion_group.xa (j - i)
source
@[simp]
theorem quaternion_group.xa_mul_a {n : ℕ} (i j : zmod (2 * n)) :
quaternion_group.xa i * quaternion_group.a j = quaternion_group.xa (i + j)
source
@[simp]
theorem quaternion_group.xa_mul_xa {n : ℕ} (i j : zmod (2 * n)) :
quaternion_group.xa i * quaternion_group.xa j = quaternion_group.a (↑n + j - i)
source
theorem quaternion_group.one_def {n : ℕ} :
1 = quaternion_group.a 0
source
def quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero  :
quaternion_group 0 ≃* dihedral_group 0

The special case that more or less by definition quaternion_group 0 is isomorphic to the infinite dihedral group.

Equations
source
@[protected, instance]
def quaternion_group.fintype {n : ℕ} [ne_zero n] :
fintype (quaternion_group n)

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

Equations
source
@[protected, instance]
def quaternion_group.nontrivial {n : ℕ} :
nontrivial (quaternion_group n)
source
theorem quaternion_group.card {n : ℕ} [ne_zero n] :
fintype.card (quaternion_group n) = 4 * n

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

source
@[simp]
theorem quaternion_group.a_one_pow {n : ℕ} (k : ℕ) :
quaternion_group.a 1 ^ k = quaternion_group.a ↑k
source
@[simp]
theorem quaternion_group.a_one_pow_n {n : ℕ} :
quaternion_group.a 1 ^ (2 * n) = 1
source
@[simp]
theorem quaternion_group.xa_sq {n : ℕ} (i : zmod (2 * n)) :
quaternion_group.xa i ^ 2 = quaternion_group.a ↑n
source
@[simp]
theorem quaternion_group.xa_pow_four {n : ℕ} (i : zmod (2 * n)) :
quaternion_group.xa i ^ 4 = 1
source
@[simp]
theorem quaternion_group.order_of_xa {n : ℕ} [ne_zero n] (i : zmod (2 * n)) :
order_of (quaternion_group.xa i) = 4

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

source
theorem quaternion_group.quaternion_group_one_is_cyclic  :
is_cyclic (quaternion_group 1)

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

source
@[simp]
theorem quaternion_group.order_of_a_one {n : ℕ} :
order_of (quaternion_group.a 1) = 2 * n

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

source
theorem quaternion_group.order_of_a {n : ℕ} [ne_zero n] (i : zmod (2 * n)) :
order_of (quaternion_group.a i) = 2 * n / (2 * n).gcd i.val

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

source
theorem quaternion_group.exponent {n : ℕ} :
monoid.exponent (quaternion_group n) = 2 * gcd_monoid.lcm n 2