Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 98f2779

Browse files
MichaelStollBayreuthMichaelStollBayreuth
committed
refactor(number_theory/legendre_symbol/*): move section general from quadratic_char.lean into new file auxiliary.lean (#14027)
This is a purely administrative step (in preparation of adding more files that may need some of the auxiliary results). We move the collection of auxiliary results that constitute `section general` of `quadratic_char.lean` to a new file `auxiliary.lean` (and change the `import`s of `quadratic_char.lean` accordingly). This new file is meant as a temporary place for these auxiliary results; when the refactor of `quadratic_reciprocity` is finished, they will be moved to appropriate files in mathlib.
1 parent 31af0e8 commit 98f2779

File tree

2 files changed

+168
-160
lines changed

2 files changed

+168
-160
lines changed

‎src/number_theory/legendre_symbol/auxiliary.lean‎

Lines changed: 167 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
/-
2+
Copyright (c) 2022 Michael Stoll. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Michael Stoll
5+
-/
6+
import tactic.basic
7+
import field_theory.finite.basic
8+
9+
/-!
10+
# Some auxiliary results
11+
12+
We collect some results here that are not specific to quadratic characters
13+
or Legendre symbols, but are needed in some places there.
14+
They will be moved to appropriate places eventually.
15+
-/
16+
17+
section general
18+
19+
/-- A natural number is odd iff it has residue `1` or `3` mod `4`-/
20+
lemma nat.odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 :=
21+
begin
22+
split,
23+
{ have help : ∀ (m : ℕ), 0 ≤ m → m < 4 → m % 2 = 1 → m = 1 ∨ m = 3 := dec_trivial,
24+
intro hn,
25+
rw [← nat.mod_mod_of_dvd n (by norm_num : 2 ∣ 4)] at hn,
26+
exact help (n % 4) zero_le' (nat.mod_lt n (by norm_num)) hn, },
27+
{ intro h,
28+
cases h with h h,
29+
{ exact nat.odd_of_mod_four_eq_one h, },
30+
{ exact nat.odd_of_mod_four_eq_three h }, },
31+
end
32+
33+
/-- If `ring_char R = 2`, where `R` is a finite reduced commutative ring,
34+
then every `a : R` is a square. -/
35+
lemma is_square_of_char_two' {R : Type*} [fintype R] [comm_ring R] [is_reduced R] [char_p R 2]
36+
(a : R) : is_square a :=
37+
exists_imp_exists (λ b h, pow_two b ▸ eq.symm h) $
38+
((fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a
39+
40+
namespace finite_field
41+
42+
variables {F : Type*} [field F] [fintype F]
43+
44+
/-- In a finite field of characteristic `2`, all elements are squares. -/
45+
lemma is_square_of_char_two (hF : ring_char F = 2) (a : F) : is_square a :=
46+
begin
47+
haveI hF' : char_p F 2 := ring_char.of_eq hF,
48+
exact is_square_of_char_two' a,
49+
end
50+
51+
/-- The finite field `F` has even cardinality iff it has characteristic `2`. -/
52+
lemma even_card_iff_char_two : ring_char F = 2 ↔ fintype.card F % 2 = 0 :=
53+
begin
54+
rcases finite_field.card F (ring_char F) with ⟨n, hp, h⟩,
55+
rw [h, nat.pow_mod],
56+
split,
57+
{ intro hF,
58+
rw hF,
59+
simp only [nat.bit0_mod_two, zero_pow', ne.def, pnat.ne_zero, not_false_iff, nat.zero_mod], },
60+
{ rw [← nat.even_iff, nat.even_pow],
61+
rintros ⟨hev, hnz⟩,
62+
rw [nat.even_iff, nat.mod_mod] at hev,
63+
cases (nat.prime.eq_two_or_odd hp) with h₁ h₁,
64+
{ exact h₁, },
65+
{ exact false.rec (ring_char F = 2) (one_ne_zero ((eq.symm h₁).trans hev)), }, },
66+
end
67+
68+
lemma even_card_of_char_two (hF : ring_char F = 2) : fintype.card F % 2 = 0 :=
69+
even_card_iff_char_two.mp hF
70+
71+
lemma odd_card_of_char_ne_two (hF : ring_char F ≠ 2) : fintype.card F % 2 = 1 :=
72+
nat.mod_two_ne_zero.mp (mt even_card_iff_char_two.mpr hF)
73+
74+
/-- Characteristic `≠ 2` implies that `-1 ≠ 1`. -/
75+
lemma neg_one_ne_one_of_char_ne_two (hF : ring_char F ≠ 2) : (-1 : F) ≠ 1 :=
76+
begin
77+
have hc := char_p.char_is_prime F (ring_char F),
78+
haveI hF' : fact (2 < ring_char F) := ⟨ lt_of_le_of_ne (nat.prime.two_le hc) (ne.symm hF) ⟩,
79+
exact char_p.neg_one_ne_one _ (ring_char F),
80+
end
81+
82+
/-- Characteristic `≠ 2` implies that `-a ≠ a` when `a ≠ 0`. -/
83+
lemma neg_ne_self_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) : a ≠ -a :=
84+
begin
85+
intro hf,
86+
apply (neg_one_ne_one_of_char_ne_two hF).symm,
87+
rw [eq_neg_iff_add_eq_zero, ←two_mul, mul_one],
88+
rw [eq_neg_iff_add_eq_zero, ←two_mul, mul_eq_zero] at hf,
89+
exact hf.resolve_right ha,
90+
end
91+
92+
/-- If `F` has odd characteristic, then for nonzero `a : F`, we have that `a ^ (#F / 2) = ±1`. -/
93+
lemma pow_dichotomy (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
94+
a^(fintype.card F / 2) = 1 ∨ a^(fintype.card F / 2) = -1 :=
95+
begin
96+
have h₁ := finite_field.pow_card_sub_one_eq_one a ha,
97+
set q := fintype.card F with hq,
98+
have hq : q % 2 = 1 := finite_field.odd_card_of_char_ne_two hF,
99+
have h₂ := nat.two_mul_odd_div_two hq,
100+
rw [← h₂, mul_comm, pow_mul, pow_two] at h₁,
101+
exact mul_self_eq_one_iff.mp h₁,
102+
end
103+
104+
/-- A unit `a` of a finite field `F` of odd characteristic is a square
105+
if and only if `a ^ (#F / 2) = 1`. -/
106+
lemma unit_is_square_iff (hF : ring_char F ≠ 2) (a : Fˣ) :
107+
is_square a ↔ a ^ (fintype.card F / 2) = 1 :=
108+
begin
109+
classical,
110+
obtain ⟨g, hg⟩ := is_cyclic.exists_generator Fˣ,
111+
obtain ⟨n, hn⟩ : a ∈ submonoid.powers g, { rw mem_powers_iff_mem_zpowers, apply hg },
112+
have hodd := nat.two_mul_odd_div_two (finite_field.odd_card_of_char_ne_two hF),
113+
split,
114+
{ rintro ⟨y, rfl⟩,
115+
rw [← pow_two, ← pow_mul, hodd],
116+
apply_fun (@coe Fˣ F _),
117+
{ push_cast,
118+
exact finite_field.pow_card_sub_one_eq_one (y : F) (units.ne_zero y), },
119+
{ exact units.ext, }, },
120+
{ subst a, assume h,
121+
have key : 2 * (fintype.card F / 2) ∣ n * (fintype.card F / 2),
122+
{ rw [← pow_mul] at h,
123+
rw [hodd, ← fintype.card_units, ← order_of_eq_card_of_forall_mem_zpowers hg],
124+
apply order_of_dvd_of_pow_eq_one h },
125+
have : 0 < fintype.card F / 2 := nat.div_pos fintype.one_lt_card (by norm_num),
126+
obtain ⟨m, rfl⟩ := nat.dvd_of_mul_dvd_mul_right this key,
127+
refine ⟨g ^ m, _⟩,
128+
rw [mul_comm, pow_mul, pow_two], },
129+
end
130+
131+
/-- A non-zero `a : F` is a square if and only if `a ^ (#F / 2) = 1`. -/
132+
lemma is_square_iff (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
133+
is_square a ↔ a ^ (fintype.card F / 2) = 1 :=
134+
begin
135+
apply (iff_congr _ (by simp [units.ext_iff])).mp
136+
(finite_field.unit_is_square_iff hF (units.mk0 a ha)),
137+
simp only [is_square, units.ext_iff, units.coe_mk0, units.coe_mul],
138+
split, { rintro ⟨y, hy⟩, exact ⟨y, hy⟩ },
139+
{ rintro ⟨y, rfl⟩,
140+
have hy : y ≠ 0, { rintro rfl, simpa [zero_pow] using ha, },
141+
refine ⟨units.mk0 y hy, _⟩, simp, }
142+
end
143+
144+
/-- In a finite field of odd characteristic, not every element is a square. -/
145+
lemma exists_nonsquare (hF : ring_char F ≠ 2) : ∃ (a : F), ¬ is_square a :=
146+
begin
147+
-- idea: the squaring map on `F` is not injetive, hence not surjective
148+
let sq : F → F := λ x, x^2,
149+
have h : ¬ function.injective sq,
150+
{ simp only [function.injective, not_forall, exists_prop],
151+
use [-1, 1],
152+
split,
153+
{ simp only [sq, one_pow, neg_one_sq], },
154+
{ exact finite_field.neg_one_ne_one_of_char_ne_two hF, }, },
155+
have h₁ := mt (fintype.injective_iff_surjective.mpr) h, -- sq not surjective
156+
push_neg at h₁,
157+
cases h₁ with a h₁,
158+
use a,
159+
simp only [is_square, sq, not_exists, ne.def] at h₁ ⊢,
160+
intros b hb,
161+
rw ← pow_two at hb,
162+
exact (h₁ b hb.symm),
163+
end
164+
165+
end finite_field
166+
167+
end general

‎src/number_theory/legendre_symbol/quadratic_char.lean‎

Lines changed: 1 addition & 160 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Michael Stoll
55
-/
66
import tactic.basic
7-
import field_theory.finite.basic
7+
import number_theory.legendre_symbol.auxiliary
88
import data.int.range
99

1010
/-!
@@ -18,165 +18,6 @@ some basic statements about it.
1818
quadratic character
1919
-/
2020

21-
/-!
22-
### Some general results, mostly on finite fields
23-
24-
We collect some results here that are not specific to quadratic characters
25-
but are needed below. They will be moved to appropriate places eventually.
26-
-/
27-
28-
section general
29-
30-
/-- A natural number is odd iff it has residue `1` or `3` mod `4`-/
31-
lemma nat.odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 :=
32-
begin
33-
split,
34-
{ have help : ∀ (m : ℕ), 0 ≤ m → m < 4 → m % 2 = 1 → m = 1 ∨ m = 3 := dec_trivial,
35-
intro hn,
36-
rw [← nat.mod_mod_of_dvd n (by norm_num : 2 ∣ 4)] at hn,
37-
exact help (n % 4) zero_le' (nat.mod_lt n (by norm_num)) hn, },
38-
{ intro h,
39-
cases h with h h,
40-
{ exact nat.odd_of_mod_four_eq_one h, },
41-
{ exact nat.odd_of_mod_four_eq_three h }, },
42-
end
43-
44-
/-- If `ring_char R = 2`, where `R` is a finite reduced commutative ring,
45-
then every `a : R` is a square. -/
46-
lemma is_square_of_char_two' {R : Type*} [fintype R] [comm_ring R] [is_reduced R] [char_p R 2]
47-
(a : R) : is_square a :=
48-
exists_imp_exists (λ b h, pow_two b ▸ eq.symm h) $
49-
((fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a
50-
51-
namespace finite_field
52-
53-
variables {F : Type*} [field F] [fintype F]
54-
55-
/-- In a finite field of characteristic `2`, all elements are squares. -/
56-
lemma is_square_of_char_two (hF : ring_char F = 2) (a : F) : is_square a :=
57-
begin
58-
haveI hF' : char_p F 2 := ring_char.of_eq hF,
59-
exact is_square_of_char_two' a,
60-
end
61-
62-
/-- The finite field `F` has even cardinality iff it has characteristic `2`. -/
63-
lemma even_card_iff_char_two : ring_char F = 2 ↔ fintype.card F % 2 = 0 :=
64-
begin
65-
rcases finite_field.card F (ring_char F) with ⟨n, hp, h⟩,
66-
rw [h, nat.pow_mod],
67-
split,
68-
{ intro hF,
69-
rw hF,
70-
simp only [nat.bit0_mod_two, zero_pow', ne.def, pnat.ne_zero, not_false_iff, nat.zero_mod], },
71-
{ rw [← nat.even_iff, nat.even_pow],
72-
rintros ⟨hev, hnz⟩,
73-
rw [nat.even_iff, nat.mod_mod] at hev,
74-
cases (nat.prime.eq_two_or_odd hp) with h₁ h₁,
75-
{ exact h₁, },
76-
{ exact false.rec (ring_char F = 2) (one_ne_zero ((eq.symm h₁).trans hev)), }, },
77-
end
78-
79-
lemma even_card_of_char_two (hF : ring_char F = 2) : fintype.card F % 2 = 0 :=
80-
even_card_iff_char_two.mp hF
81-
82-
lemma odd_card_of_char_ne_two (hF : ring_char F ≠ 2) : fintype.card F % 2 = 1 :=
83-
nat.mod_two_ne_zero.mp (mt even_card_iff_char_two.mpr hF)
84-
85-
/-- Characteristic `≠ 2` implies that `-1 ≠ 1`. -/
86-
lemma neg_one_ne_one_of_char_ne_two (hF : ring_char F ≠ 2) : (-1 : F) ≠ 1 :=
87-
begin
88-
have hc := char_p.char_is_prime F (ring_char F),
89-
haveI hF' : fact (2 < ring_char F) := ⟨ lt_of_le_of_ne (nat.prime.two_le hc) (ne.symm hF) ⟩,
90-
exact char_p.neg_one_ne_one _ (ring_char F),
91-
end
92-
93-
/-- Characteristic `≠ 2` implies that `-a ≠ a` when `a ≠ 0`. -/
94-
lemma neg_ne_self_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) : a ≠ -a :=
95-
begin
96-
intro hf,
97-
apply (neg_one_ne_one_of_char_ne_two hF).symm,
98-
rw [eq_neg_iff_add_eq_zero, ←two_mul, mul_one],
99-
rw [eq_neg_iff_add_eq_zero, ←two_mul, mul_eq_zero] at hf,
100-
exact hf.resolve_right ha,
101-
end
102-
103-
/-- If `F` has odd characteristic, then for nonzero `a : F`, we have that `a ^ (#F / 2) = ±1`. -/
104-
lemma pow_dichotomy (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
105-
a^(fintype.card F / 2) = 1 ∨ a^(fintype.card F / 2) = -1 :=
106-
begin
107-
have h₁ := finite_field.pow_card_sub_one_eq_one a ha,
108-
set q := fintype.card F with hq,
109-
have hq : q % 2 = 1 := finite_field.odd_card_of_char_ne_two hF,
110-
have h₂ := nat.two_mul_odd_div_two hq,
111-
rw [← h₂, mul_comm, pow_mul, pow_two] at h₁,
112-
exact mul_self_eq_one_iff.mp h₁,
113-
end
114-
115-
/-- A unit `a` of a finite field `F` of odd characteristic is a square
116-
if and only if `a ^ (#F / 2) = 1`. -/
117-
lemma unit_is_square_iff (hF : ring_char F ≠ 2) (a : Fˣ) :
118-
is_square a ↔ a ^ (fintype.card F / 2) = 1 :=
119-
begin
120-
classical,
121-
obtain ⟨g, hg⟩ := is_cyclic.exists_generator Fˣ,
122-
obtain ⟨n, hn⟩ : a ∈ submonoid.powers g, { rw mem_powers_iff_mem_zpowers, apply hg },
123-
have hodd := nat.two_mul_odd_div_two (finite_field.odd_card_of_char_ne_two hF),
124-
split,
125-
{ rintro ⟨y, rfl⟩,
126-
rw [← pow_two, ← pow_mul, hodd],
127-
apply_fun (@coe Fˣ F _),
128-
{ push_cast,
129-
exact finite_field.pow_card_sub_one_eq_one (y : F) (units.ne_zero y), },
130-
{ exact units.ext, }, },
131-
{ subst a, assume h,
132-
have key : 2 * (fintype.card F / 2) ∣ n * (fintype.card F / 2),
133-
{ rw [← pow_mul] at h,
134-
rw [hodd, ← fintype.card_units, ← order_of_eq_card_of_forall_mem_zpowers hg],
135-
apply order_of_dvd_of_pow_eq_one h },
136-
have : 0 < fintype.card F / 2 := nat.div_pos fintype.one_lt_card (by norm_num),
137-
obtain ⟨m, rfl⟩ := nat.dvd_of_mul_dvd_mul_right this key,
138-
refine ⟨g ^ m, _⟩,
139-
rw [mul_comm, pow_mul, pow_two], },
140-
end
141-
142-
/-- A non-zero `a : F` is a square if and only if `a ^ (#F / 2) = 1`. -/
143-
lemma is_square_iff (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
144-
is_square a ↔ a ^ (fintype.card F / 2) = 1 :=
145-
begin
146-
apply (iff_congr _ (by simp [units.ext_iff])).mp
147-
(finite_field.unit_is_square_iff hF (units.mk0 a ha)),
148-
simp only [is_square, units.ext_iff, units.coe_mk0, units.coe_mul],
149-
split, { rintro ⟨y, hy⟩, exact ⟨y, hy⟩ },
150-
{ rintro ⟨y, rfl⟩,
151-
have hy : y ≠ 0, { rintro rfl, simpa [zero_pow] using ha, },
152-
refine ⟨units.mk0 y hy, _⟩, simp, }
153-
end
154-
155-
/-- In a finite field of odd characteristic, not every element is a square. -/
156-
lemma exists_nonsquare (hF : ring_char F ≠ 2) : ∃ (a : F), ¬ is_square a :=
157-
begin
158-
-- idea: the squaring map on `F` is not injetive, hence not surjective
159-
let sq : F → F := λ x, x^2,
160-
have h : ¬ function.injective sq,
161-
{ simp only [function.injective, not_forall, exists_prop],
162-
use [-1, 1],
163-
split,
164-
{ simp only [sq, one_pow, neg_one_sq], },
165-
{ exact finite_field.neg_one_ne_one_of_char_ne_two hF, }, },
166-
have h₁ := mt (fintype.injective_iff_surjective.mpr) h, -- sq not surjective
167-
push_neg at h₁,
168-
cases h₁ with a h₁,
169-
use a,
170-
simp only [is_square, sq, not_exists, ne.def] at h₁ ⊢,
171-
intros b hb,
172-
rw ← pow_two at hb,
173-
exact (h₁ b hb.symm),
174-
end
175-
176-
end finite_field
177-
178-
end general
179-
18021
namespace char
18122

18223
/-!

0 commit comments

Comments
 (0)