-
Notifications
You must be signed in to change notification settings - Fork 5
/
Quaternion.lean
333 lines (288 loc) · 10.2 KB
/
Quaternion.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
/-
Copyright (c) 2021 Julian Kuelshammer. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Julian Kuelshammer
-/
import Data.ZMod.Basic
import Algebra.Group.Nat
import Tactic.IntervalCases
import GroupTheory.SpecificGroups.Dihedral
import GroupTheory.SpecificGroups.Cyclic
#align_import group_theory.specific_groups.quaternion from "leanprover-community/mathlib"@"c20927220ef87bb4962ba08bf6da2ce3cf50a6dd"
/-!
# 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
* https://en.wikipedia.org/wiki/Dicyclic_group
* https://en.wikipedia.org/wiki/Quaternion_group
## TODO
Show that `quaternion_group 2 ≃* (quaternion ℤ)ˣ`.
-/
#print QuaternionGroup /-
/-- 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$.
-/
inductive QuaternionGroup (n : ℕ) : Type
| a : ZMod (2 * n) → QuaternionGroup
| xa : ZMod (2 * n) → QuaternionGroup
deriving DecidableEq
#align quaternion_group QuaternionGroup
-/
namespace QuaternionGroup
variable {n : ℕ}
/-- Multiplication of the dihedral group.
-/
private def mul : QuaternionGroup n → QuaternionGroup n → QuaternionGroup n
| a i, a j => a (i + j)
| a i, xa j => xa (j - i)
| xa i, a j => xa (i + j)
| xa i, xa j => a (n + j - i)
/-- The identity `1` is given by `aⁱ`.
-/
private def one : QuaternionGroup n :=
a 0
instance : Inhabited (QuaternionGroup n) :=
⟨one⟩
/-- The inverse of an element of the quaternion group.
-/
private def inv : QuaternionGroup n → QuaternionGroup n
| a i => a (-i)
| xa i => xa (n + i)
/-- The group structure on `quaternion_group n`.
-/
instance : Group (QuaternionGroup n) where
mul := mul
mul_assoc := by
rintro (i | i) (j | j) (k | k) <;> simp only [mul] <;> abel
simp only [neg_mul, one_mul, Int.cast_one, zsmul_eq_mul, Int.cast_neg, add_right_inj]
calc
-(n : ZMod (2 * n)) = 0 - n := by rw [zero_sub]
_ = 2 * n - n := by norm_cast; simp
_ = n := by ring
one := one
one_mul := by
rintro (i | i)
· exact congr_arg a (zero_add i)
· exact congr_arg xa (sub_zero i)
mul_one := by
rintro (i | i)
· exact congr_arg a (add_zero i)
· exact congr_arg xa (add_zero i)
inv := inv
hMul_left_inv := by
rintro (i | i)
· exact congr_arg a (neg_add_self i)
· exact congr_arg a (sub_self (n + i))
variable {n}
#print QuaternionGroup.a_mul_a /-
@[simp]
theorem a_mul_a (i j : ZMod (2 * n)) : a i * a j = a (i + j) :=
rfl
#align quaternion_group.a_mul_a QuaternionGroup.a_mul_a
-/
#print QuaternionGroup.a_mul_xa /-
@[simp]
theorem a_mul_xa (i j : ZMod (2 * n)) : a i * xa j = xa (j - i) :=
rfl
#align quaternion_group.a_mul_xa QuaternionGroup.a_mul_xa
-/
#print QuaternionGroup.xa_mul_a /-
@[simp]
theorem xa_mul_a (i j : ZMod (2 * n)) : xa i * a j = xa (i + j) :=
rfl
#align quaternion_group.xa_mul_a QuaternionGroup.xa_mul_a
-/
#print QuaternionGroup.xa_mul_xa /-
@[simp]
theorem xa_mul_xa (i j : ZMod (2 * n)) : xa i * xa j = a (n + j - i) :=
rfl
#align quaternion_group.xa_mul_xa QuaternionGroup.xa_mul_xa
-/
#print QuaternionGroup.one_def /-
theorem one_def : (1 : QuaternionGroup n) = a 0 :=
rfl
#align quaternion_group.one_def QuaternionGroup.one_def
-/
private def fintype_helper : Sum (ZMod (2 * n)) (ZMod (2 * n)) ≃ QuaternionGroup n
where
invFun i :=
match i with
| a j => Sum.inl j
| xa j => Sum.inr j
toFun i :=
match i with
| Sum.inl j => a j
| Sum.inr j => xa j
left_inv := by rintro (x | x) <;> rfl
right_inv := by rintro (x | x) <;> rfl
#print QuaternionGroup.quaternionGroupZeroEquivDihedralGroupZero /-
/-- The special case that more or less by definition `quaternion_group 0` is isomorphic to the
infinite dihedral group. -/
def quaternionGroupZeroEquivDihedralGroupZero : QuaternionGroup 0 ≃* DihedralGroup 0
where
toFun i := QuaternionGroup.recOn i DihedralGroup.r DihedralGroup.sr
invFun i :=
match i with
| DihedralGroup.r j => a j
| DihedralGroup.sr j => xa j
left_inv := by rintro (k | k) <;> rfl
right_inv := by rintro (k | k) <;> rfl
map_mul' := by rintro (k | k) (l | l) <;> · dsimp; simp
#align quaternion_group.quaternion_group_zero_equiv_dihedral_group_zero QuaternionGroup.quaternionGroupZeroEquivDihedralGroupZero
-/
/-- If `0 < n`, then `quaternion_group n` is a finite group.
-/
instance [NeZero n] : Fintype (QuaternionGroup n) :=
Fintype.ofEquiv _ fintypeHelper
instance : Nontrivial (QuaternionGroup n) :=
⟨⟨a 0, xa 0, by decide⟩⟩
#print QuaternionGroup.card /-
/-- If `0 < n`, then `quaternion_group n` has `4n` elements.
-/
theorem card [NeZero n] : Fintype.card (QuaternionGroup n) = 4 * n :=
by
rw [← fintype.card_eq.mpr ⟨fintype_helper⟩, Fintype.card_sum, ZMod.card, two_mul]
ring
#align quaternion_group.card QuaternionGroup.card
-/
#print QuaternionGroup.a_one_pow /-
@[simp]
theorem a_one_pow (k : ℕ) : (a 1 : QuaternionGroup n) ^ k = a k :=
by
induction' k with k IH
· rw [Nat.cast_zero]; rfl
· rw [pow_succ', IH, a_mul_a]
congr 1
norm_cast
rw [Nat.one_add]
#align quaternion_group.a_one_pow QuaternionGroup.a_one_pow
-/
#print QuaternionGroup.a_one_pow_n /-
@[simp]
theorem a_one_pow_n : (a 1 : QuaternionGroup n) ^ (2 * n) = 1 :=
by
rw [a_one_pow, one_def]
congr 1
exact ZMod.natCast_self _
#align quaternion_group.a_one_pow_n QuaternionGroup.a_one_pow_n
-/
#print QuaternionGroup.xa_sq /-
@[simp]
theorem xa_sq (i : ZMod (2 * n)) : xa i ^ 2 = a n := by simp [sq]
#align quaternion_group.xa_sq QuaternionGroup.xa_sq
-/
#print QuaternionGroup.xa_pow_four /-
@[simp]
theorem xa_pow_four (i : ZMod (2 * n)) : xa i ^ 4 = 1 :=
by
simp only [pow_succ', sq, xa_mul_xa, xa_mul_a, add_sub_cancel_right, add_sub_assoc,
add_sub_cancel_left, sub_self, add_zero]
norm_cast
rw [← two_mul]
simp [one_def]
#align quaternion_group.xa_pow_four QuaternionGroup.xa_pow_four
-/
#print QuaternionGroup.orderOf_xa /-
/-- If `0 < n`, then `xa i` has order 4.
-/
@[simp]
theorem orderOf_xa [NeZero n] (i : ZMod (2 * n)) : orderOf (xa i) = 4 :=
by
change _ = 2 ^ 2
haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
apply orderOf_eq_prime_pow
· intro h
simp only [pow_one, xa_sq] at h
injection h with h'
apply_fun ZMod.val at h'
apply_fun (· / n) at h'
simp only [ZMod.val_natCast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self,
Nat.div_self (NeZero.pos n)] at h'
norm_num at h'
· norm_num
#align quaternion_group.order_of_xa QuaternionGroup.orderOf_xa
-/
#print QuaternionGroup.quaternionGroup_one_isCyclic /-
/-- In the special case `n = 1`, `quaternion 1` is a cyclic group (of order `4`). -/
theorem quaternionGroup_one_isCyclic : IsCyclic (QuaternionGroup 1) :=
by
apply isCyclic_of_orderOf_eq_card
rw [card, mul_one]
exact order_of_xa 0
#align quaternion_group.quaternion_group_one_is_cyclic QuaternionGroup.quaternionGroup_one_isCyclic
-/
#print QuaternionGroup.orderOf_a_one /-
/-- If `0 < n`, then `a 1` has order `2 * n`.
-/
@[simp]
theorem orderOf_a_one : orderOf (a 1 : QuaternionGroup n) = 2 * n :=
by
cases' eq_zero_or_neZero n with hn hn
· subst hn
simp_rw [MulZeroClass.mul_zero, orderOf_eq_zero_iff']
intro n h
rw [one_def, a_one_pow]
apply mt a.inj
haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero
simpa using h.ne'
apply
(Nat.le_of_dvd (NeZero.pos _)
(orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left
intro h
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _
rw [a_one_pow] at h1
injection h1 with h2
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2
exact absurd h2.symm (orderOf_pos _).Ne
#align quaternion_group.order_of_a_one QuaternionGroup.orderOf_a_one
-/
#print QuaternionGroup.orderOf_a /-
/-- If `0 < n`, then `a i` has order `(2 * n) / gcd (2 * n) i`.
-/
theorem orderOf_a [NeZero n] (i : ZMod (2 * n)) : orderOf (a i) = 2 * n / Nat.gcd (2 * n) i.val :=
by
conv_lhs => rw [← ZMod.natCast_zmod_val i]
rw [← a_one_pow, orderOf_pow, order_of_a_one]
#align quaternion_group.order_of_a QuaternionGroup.orderOf_a
-/
#print QuaternionGroup.exponent /-
theorem exponent : Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2 :=
by
rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]
norm_num
cases' eq_zero_or_neZero n with hn hn
· subst hn
simp only [lcm_zero_left, MulZeroClass.mul_zero]
exact Monoid.exponent_eq_zero_of_order_zero order_of_a_one
apply Nat.dvd_antisymm
· apply Monoid.exponent_dvd_of_forall_pow_eq_one
rintro (m | m)
· rw [← orderOf_dvd_iff_pow_eq_one, order_of_a]
refine' Nat.dvd_trans ⟨gcd (2 * n) m.val, _⟩ (dvd_lcm_left (2 * n) 4)
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm
· rw [← orderOf_dvd_iff_pow_eq_one, order_of_xa]
exact dvd_lcm_right (2 * n) 4
· apply lcm_dvd
· convert Monoid.order_dvd_exponent (a 1)
exact order_of_a_one.symm
· convert Monoid.order_dvd_exponent (xa 0)
exact (order_of_xa 0).symm
#align quaternion_group.exponent QuaternionGroup.exponent
-/
end QuaternionGroup