PadicQuadraticSplitting.lean

1 import Mathlib.NumberTheory.Padics.Hensel
2 import Mathlib.NumberTheory.Padics.RingHoms
3 import Mathlib.NumberTheory.LegendreSymbol.Basic
4 import Mathlib.Tactic
5 
6 /-!
7 # Splitting of the quadratic polynomial X² + 1 over p-adic fields
8 
9 A square root of −1 in Q_p has norm one and hence lies in Z_p. This permits
10 finite residue obstructions at p = 3 and p = 2. At odd primes a simple residue
11 root lifts by the pinned Mathlib Hensel theorem. Together with the finite-field
12 criterion this proves the exact congruence criterion for every prime.
13 
14 The p-adic fields and reduction maps below are actual Mathlib constructions.
15 No local-type label, square-root-existence oracle, or new axiom is assumed.
16 -/
17 
18 noncomputable section
19 open Polynomial
20 namespace PaperX.PadicQuadraticSplitting
21 local instance : Fact (Nat.Prime 5) := ⟨by decide⟩
22 
23 /-- Every p-adic square root of −1 is integral. -/
24 theorem root_integral {p : ℕ} [Fact p.Prime] {x : ℚ_[p]} (hx : x ^ 2 = -1) :
25     ∃ y : ℤ_[p], (y : ℚ_[p]) = x ∧ y ^ 2 = -1 := by
26   have hn : ‖x‖ ^ 2 = 1 := by simpa only [norm_pow, norm_neg, norm_one] using congrArg norm hx
27   have hl : ‖x‖ ≤ 1 := by nlinarith [norm_nonneg x]
28   refine ⟨⟨x, hl⟩, rfl, ?_⟩
29   apply Subtype.ext
30   exact hx
31 
32 /-- Reduction modulo three obstructs a square root of −1 in Q_3. -/
33 theorem no_root_three : ¬ ∃ x : ℚ_[3], x ^ 2 = -1 := by
34   rintro ⟨x, hx⟩
35   obtain ⟨y, _, hy⟩ := root_integral hx
36   have hz := congrArg (PadicInt.toZMod : ℤ_[3] →+* ZMod 3) hy
37   have bad : ∀ z : ZMod 3, z ^ 2 ≠ -1 := by decide +kernel
38   exact bad _ (by simpa using hz)
39 
40 /-- Reduction modulo four obstructs a square root of −1 in Q_2. -/
41 theorem no_root_two : ¬ ∃ x : ℚ_[2], x ^ 2 = -1 := by
42   rintro ⟨x, hx⟩
43   obtain ⟨y, _, hy⟩ := root_integral hx
44   have hz := congrArg (PadicInt.toZModPow 2 : ℤ_[2] →+* ZMod 4) hy
45   have bad : ∀ z : ZMod 4, z ^ 2 ≠ -1 := by decide +kernel
46   exact bad _ (by simpa using hz)
47 
48 /-- Hensel lifting at the residue root 2 produces a root in Z_5. -/
49 theorem root_five_integral : ∃ x : ℤ_[5], x ^ 2 = -1 := by
50   have hf : ∀ x : ℤ_[5], (X ^ 2 + 1 : Polynomial ℤ).aeval x = x ^ 2 + 1 := by intro x; simp
51   have hd : (X ^ 2 + 1 : Polynomial ℤ).derivative.aeval (2 : ℤ_[5]) = 4 := by norm_num [Polynomial.aeval_def]
52   have hv : (X ^ 2 + 1 : Polynomial ℤ).aeval (2 : ℤ_[5]) = 5 := by norm_num
53   have hn : ‖(X ^ 2 + 1 : Polynomial ℤ).aeval (2 : ℤ_[5])‖ <
54       ‖(X ^ 2 + 1 : Polynomial ℤ).derivative.aeval (2 : ℤ_[5])‖ ^ 2 := by
55     rw [hd, hv]
56     have h4 : ‖(4 : ℤ_[5])‖ = 1 := (PadicInt.norm_natCast_eq_one_iff).2 (by decide)
57     have h5 : ‖(5 : ℤ_[5])‖ < 1 := (PadicInt.norm_natCast_lt_one_iff).2 (dvd_refl _)
58     simpa only [h4, one_pow] using h5
59   obtain ⟨x, hx, _⟩ := hensels_lemma hn
60   exact ⟨x, by have h := hf x; rw [h] at hx; exact eq_neg_of_add_eq_zero_left hx⟩
61 
62 /-- The integral root gives an actual square root of −1 in Q_5. -/
63 theorem root_five : ∃ x : ℚ_[5], x ^ 2 = -1 := by
64   obtain ⟨x, hx⟩ := root_five_integral
65   exact ⟨x, congrArg (fun y : ℤ_[5] => (y : ℚ_[5])) hx⟩
66 
67 
68 /-- A p-adic integer has norm less than one exactly when its residue vanishes. -/
69 theorem residual_norm_lt_one {p : ℕ} [Fact p.Prime] (a : ℤ_[p]) :
70     ‖a‖ < 1 ↔ PadicInt.toZMod a = 0 := by
71   rw [← PadicInt.mem_nonunits, ← IsLocalRing.mem_maximalIdeal,
72     ← PadicInt.ker_toZMod, RingHom.mem_ker]
73 
74 /-- Every residue root of X² + 1 at an odd prime supplies an integral root. -/
75 theorem lift_odd_root {p : ℕ} [Fact p.Prime] (hp : p ≠ 2)
76     (x : ZMod p) (hx : x ^ 2 = -1) : ∃ y : ℤ_[p], y ^ 2 = -1 := by
77   obtain ⟨a, ha⟩ := ZMod.ringHom_surjective (PadicInt.toZMod : ℤ_[p] →+* ZMod p) x
78   have hx0 : x ≠ 0 := by intro h; simp [h] at hx
79   have ht : (2 : ZMod p) ≠ 0 := by
80     intro h
81     have hdvd : p ∣ 2 := (ZMod.natCast_eq_zero_iff 2 p).mp h
82     have hle : p ≤ 2 := Nat.le_of_dvd (by decide) hdvd
83     have hge := (Fact.out : Nat.Prime p).two_le
84     omega
85   have hf : ∀ z : ℤ_[p], (X ^ 2 + 1 : Polynomial ℤ).aeval z = z ^ 2 + 1 := by intro z; simp
86   have hd : (X ^ 2 + 1 : Polynomial ℤ).derivative.aeval a = 2 * a := by
87     norm_num [Polynomial.aeval_def]
88   have hn : ‖a ^ 2 + 1‖ < 1 := (residual_norm_lt_one _).2 (by simp [ha, hx])
89   have hdn : ‖(2 : ℤ_[p]) * a‖ = 1 := by
90     have hnot : ¬ ‖(2 : ℤ_[p]) * a‖ < 1 := by
91       rw [residual_norm_lt_one]
92       simpa only [map_mul, map_ofNat, ha] using mul_ne_zero ht hx0
93     exact le_antisymm (PadicInt.norm_le_one _) (not_lt.mp hnot)
94   obtain ⟨y, hy, _⟩ := hensels_lemma (F := (X ^ 2 + 1 : Polynomial ℤ)) (a := a)
95     (by simpa only [hf, hd, hdn, one_pow] using hn)
96   exact ⟨y, by rw [hf] at hy; exact eq_neg_of_add_eq_zero_left hy⟩
97 
98 /-- For odd primes the p-adic criterion agrees with the finite-field criterion. -/
99 theorem root_iff_mod_four {p : ℕ} [Fact p.Prime] (hp : p ≠ 2) :
100     (∃ x : ℚ_[p], x ^ 2 = -1) ↔ p % 4 ≠ 3 := by
101   constructor
102   · rintro ⟨x, hx⟩
103     obtain ⟨y, _, hy⟩ := root_integral hx
104     apply ZMod.mod_four_ne_three_of_sq_eq_neg_one
105     simpa using congrArg (PadicInt.toZMod : ℤ_[p] →+* ZMod p) hy
106   · intro h
107     obtain ⟨x, hx⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr h
108     obtain ⟨y, hy⟩ := lift_odd_root hp x (by simpa only [pow_two] using hx.symm)
109     exact ⟨y, congrArg (fun z : ℤ_[p] => (z : ℚ_[p])) hy⟩
110 
111 
112 /-- Complete criterion, including the nonsplit prime two. -/
113 theorem root_iff_mod_four_eq_one (p : ℕ) [Fact p.Prime] :
114     (∃ x : ℚ_[p], x ^ 2 = -1) ↔ p % 4 = 1 := by
115   by_cases hp : p = 2
116   · subst p
117     simp only [no_root_two, false_iff]
118     norm_num
119   · rw [root_iff_mod_four hp]
120     have hodd := (Nat.Prime.mod_two_eq_one_iff_ne_two (Fact.out : p.Prime)).mpr hp
121     omega
122 
123 end PaperX.PadicQuadraticSplitting

Back to source controls