-
Notifications
You must be signed in to change notification settings - Fork 259
/
ZModChar.lean
219 lines (180 loc) · 8.42 KB
/
ZModChar.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
/-
Copyright (c) 2022 Michael Stoll. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Michael Stoll
-/
import Mathlib.Data.Int.Range
import Mathlib.Data.ZMod.Basic
import Mathlib.NumberTheory.MulChar.Basic
#align_import number_theory.legendre_symbol.zmod_char from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
/-!
# Quadratic characters on ℤ/nℤ
This file defines some quadratic characters on the rings ℤ/4ℤ and ℤ/8ℤ.
We set them up to be of type `MulChar (ZMod n) ℤ`, where `n` is `4` or `8`.
## Tags
quadratic character, zmod
-/
/-!
### Quadratic characters mod 4 and 8
We define the primitive quadratic characters `χ₄`on `ZMod 4`
and `χ₈`, `χ₈'` on `ZMod 8`.
-/
namespace ZMod
section QuadCharModP
/-- Define the nontrivial quadratic character on `ZMod 4`, `χ₄`.
It corresponds to the extension `ℚ(√-1)/ℚ`. -/
@[simps]
def χ₄ : MulChar (ZMod 4) ℤ where
toFun a :=
match a with
| 0 | 2 => 0
| 1 => 1
| 3 => -1
map_one' := rfl
map_mul' := by decide
map_nonunit' := by decide
#align zmod.χ₄ ZMod.χ₄
/-- `χ₄` takes values in `{0, 1, -1}` -/
theorem isQuadratic_χ₄ : χ₄.IsQuadratic := by
unfold MulChar.IsQuadratic
decide
#align zmod.is_quadratic_χ₄ ZMod.isQuadratic_χ₄
/-- The value of `χ₄ n`, for `n : ℕ`, depends only on `n % 4`. -/
theorem χ₄_nat_mod_four (n : ℕ) : χ₄ n = χ₄ (n % 4 : ℕ) := by
rw [← ZMod.natCast_mod n 4]
#align zmod.χ₄_nat_mod_four ZMod.χ₄_nat_mod_four
/-- The value of `χ₄ n`, for `n : ℤ`, depends only on `n % 4`. -/
theorem χ₄_int_mod_four (n : ℤ) : χ₄ n = χ₄ (n % 4 : ℤ) := by
rw [← ZMod.intCast_mod n 4, Nat.cast_ofNat]
#align zmod.χ₄_int_mod_four ZMod.χ₄_int_mod_four
/-- An explicit description of `χ₄` on integers / naturals -/
theorem χ₄_int_eq_if_mod_four (n : ℤ) :
χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 := by
have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by
decide
rw [← Int.emod_emod_of_dvd n (by omega : (2 : ℤ) ∣ 4), ← ZMod.intCast_mod n 4]
exact help (n % 4) (Int.emod_nonneg n (by omega)) (Int.emod_lt n (by omega))
#align zmod.χ₄_int_eq_if_mod_four ZMod.χ₄_int_eq_if_mod_four
theorem χ₄_nat_eq_if_mod_four (n : ℕ) :
χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 :=
mod_cast χ₄_int_eq_if_mod_four n
#align zmod.χ₄_nat_eq_if_mod_four ZMod.χ₄_nat_eq_if_mod_four
/-- Alternative description of `χ₄ n` for odd `n : ℕ` in terms of powers of `-1` -/
theorem χ₄_eq_neg_one_pow {n : ℕ} (hn : n % 2 = 1) : χ₄ n = (-1) ^ (n / 2) := by
rw [χ₄_nat_eq_if_mod_four]
simp only [hn, Nat.one_ne_zero, if_false]
nth_rewrite 3 [← Nat.div_add_mod n 4]
nth_rewrite 3 [show 4 = 2 * 2 by omega]
rw [mul_assoc, add_comm, Nat.add_mul_div_left _ _ zero_lt_two, pow_add, pow_mul,
neg_one_sq, one_pow, mul_one]
have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide
exact help _ (Nat.mod_lt n (by omega)) <| (Nat.mod_mod_of_dvd n (by omega : 2 ∣ 4)).trans hn
#align zmod.χ₄_eq_neg_one_pow ZMod.χ₄_eq_neg_one_pow
/-- If `n % 4 = 1`, then `χ₄ n = 1`. -/
theorem χ₄_nat_one_mod_four {n : ℕ} (hn : n % 4 = 1) : χ₄ n = 1 := by
rw [χ₄_nat_mod_four, hn]
rfl
#align zmod.χ₄_nat_one_mod_four ZMod.χ₄_nat_one_mod_four
/-- If `n % 4 = 3`, then `χ₄ n = -1`. -/
theorem χ₄_nat_three_mod_four {n : ℕ} (hn : n % 4 = 3) : χ₄ n = -1 := by
rw [χ₄_nat_mod_four, hn]
rfl
#align zmod.χ₄_nat_three_mod_four ZMod.χ₄_nat_three_mod_four
/-- If `n % 4 = 1`, then `χ₄ n = 1`. -/
theorem χ₄_int_one_mod_four {n : ℤ} (hn : n % 4 = 1) : χ₄ n = 1 := by
rw [χ₄_int_mod_four, hn]
rfl
#align zmod.χ₄_int_one_mod_four ZMod.χ₄_int_one_mod_four
/-- If `n % 4 = 3`, then `χ₄ n = -1`. -/
theorem χ₄_int_three_mod_four {n : ℤ} (hn : n % 4 = 3) : χ₄ n = -1 := by
rw [χ₄_int_mod_four, hn]
rfl
#align zmod.χ₄_int_three_mod_four ZMod.χ₄_int_three_mod_four
/-- If `n % 4 = 1`, then `(-1)^(n/2) = 1`. -/
theorem neg_one_pow_div_two_of_one_mod_four {n : ℕ} (hn : n % 4 = 1) : (-1 : ℤ) ^ (n / 2) = 1 :=
χ₄_eq_neg_one_pow (Nat.odd_of_mod_four_eq_one hn) ▸ χ₄_nat_one_mod_four hn
#align zmod.neg_one_pow_div_two_of_one_mod_four ZMod.neg_one_pow_div_two_of_one_mod_four
/-- If `n % 4 = 3`, then `(-1)^(n/2) = -1`. -/
theorem neg_one_pow_div_two_of_three_mod_four {n : ℕ} (hn : n % 4 = 3) : (-1 : ℤ) ^ (n / 2) = -1 :=
χ₄_eq_neg_one_pow (Nat.odd_of_mod_four_eq_three hn) ▸ χ₄_nat_three_mod_four hn
#align zmod.neg_one_pow_div_two_of_three_mod_four ZMod.neg_one_pow_div_two_of_three_mod_four
/-- Define the first primitive quadratic character on `ZMod 8`, `χ₈`.
It corresponds to the extension `ℚ(√2)/ℚ`. -/
@[simps]
def χ₈ : MulChar (ZMod 8) ℤ where
toFun a :=
match a with
| 0 | 2 | 4 | 6 => 0
| 1 | 7 => 1
| 3 | 5 => -1
map_one' := rfl
map_mul' := by decide
map_nonunit' := by decide
#align zmod.χ₈ ZMod.χ₈
/-- `χ₈` takes values in `{0, 1, -1}` -/
theorem isQuadratic_χ₈ : χ₈.IsQuadratic := by
unfold MulChar.IsQuadratic
decide
#align zmod.is_quadratic_χ₈ ZMod.isQuadratic_χ₈
/-- The value of `χ₈ n`, for `n : ℕ`, depends only on `n % 8`. -/
theorem χ₈_nat_mod_eight (n : ℕ) : χ₈ n = χ₈ (n % 8 : ℕ) := by
rw [← ZMod.natCast_mod n 8]
#align zmod.χ₈_nat_mod_eight ZMod.χ₈_nat_mod_eight
/-- The value of `χ₈ n`, for `n : ℤ`, depends only on `n % 8`. -/
theorem χ₈_int_mod_eight (n : ℤ) : χ₈ n = χ₈ (n % 8 : ℤ) := by
rw [← ZMod.intCast_mod n 8, Nat.cast_ofNat]
#align zmod.χ₈_int_mod_eight ZMod.χ₈_int_mod_eight
/-- An explicit description of `χ₈` on integers / naturals -/
theorem χ₈_int_eq_if_mod_eight (n : ℤ) :
χ₈ n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 := by
have help :
∀ m : ℤ, 0 ≤ m → m < 8 → χ₈ m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 := by
decide
rw [← Int.emod_emod_of_dvd n (by omega : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]
exact help (n % 8) (Int.emod_nonneg n (by omega)) (Int.emod_lt n (by omega))
#align zmod.χ₈_int_eq_if_mod_eight ZMod.χ₈_int_eq_if_mod_eight
theorem χ₈_nat_eq_if_mod_eight (n : ℕ) :
χ₈ n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 :=
mod_cast χ₈_int_eq_if_mod_eight n
#align zmod.χ₈_nat_eq_if_mod_eight ZMod.χ₈_nat_eq_if_mod_eight
/-- Define the second primitive quadratic character on `ZMod 8`, `χ₈'`.
It corresponds to the extension `ℚ(√-2)/ℚ`. -/
@[simps]
def χ₈' : MulChar (ZMod 8) ℤ where
toFun a :=
match a with
| 0 | 2 | 4 | 6 => 0
| 1 | 3 => 1
| 5 | 7 => -1
map_one' := rfl
map_mul' := by decide
map_nonunit' := by decide
#align zmod.χ₈' ZMod.χ₈'
/-- `χ₈'` takes values in `{0, 1, -1}` -/
theorem isQuadratic_χ₈' : χ₈'.IsQuadratic := by
unfold MulChar.IsQuadratic
decide
#align zmod.is_quadratic_χ₈' ZMod.isQuadratic_χ₈'
/-- An explicit description of `χ₈'` on integers / naturals -/
theorem χ₈'_int_eq_if_mod_eight (n : ℤ) :
χ₈' n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 := by
have help :
∀ m : ℤ, 0 ≤ m → m < 8 → χ₈' m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 := by
decide
rw [← Int.emod_emod_of_dvd n (by omega : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]
exact help (n % 8) (Int.emod_nonneg n (by omega)) (Int.emod_lt n (by omega))
#align zmod.χ₈'_int_eq_if_mod_eight ZMod.χ₈'_int_eq_if_mod_eight
theorem χ₈'_nat_eq_if_mod_eight (n : ℕ) :
χ₈' n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 :=
mod_cast χ₈'_int_eq_if_mod_eight n
#align zmod.χ₈'_nat_eq_if_mod_eight ZMod.χ₈'_nat_eq_if_mod_eight
/-- The relation between `χ₄`, `χ₈` and `χ₈'` -/
theorem χ₈'_eq_χ₄_mul_χ₈ : ∀ a : ZMod 8, χ₈' a = χ₄ (cast a) * χ₈ a := by
decide
#align zmod.χ₈'_eq_χ₄_mul_χ₈ ZMod.χ₈'_eq_χ₄_mul_χ₈
theorem χ₈'_int_eq_χ₄_mul_χ₈ (a : ℤ) : χ₈' a = χ₄ a * χ₈ a := by
rw [← @cast_intCast 8 (ZMod 4) _ 4 _ (by omega) a]
exact χ₈'_eq_χ₄_mul_χ₈ a
#align zmod.χ₈'_int_eq_χ₄_mul_χ₈ ZMod.χ₈'_int_eq_χ₄_mul_χ₈
end QuadCharModP
end ZMod