PolynomialPadicUnique.lean

1 module
2 public import PolynomialPadicLift
3 public import Mathlib.NumberTheory.Padics.RingHoms
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialPadicUnique
10 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
11 open Komorebi.PolynomialLiftCounts Komorebi.PolynomialSmoothCounts
12 open Komorebi.PolynomialPadicLift
13 
14 variable {d e : ℕ}
15 
16 /-- Equality in the actual residue quotient is equivalent to p-adic divisibility. -/
17 theorem toZModPow_eq_iff_dvd_sub (p n : ℕ) [Fact (Nat.Prime p)]
18     (a b : ℤ_[p]) :
19     PadicInt.toZModPow n a = PadicInt.toZModPow n b ↔
20       (p : ℤ_[p])^n ∣ a - b := by
21   rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker,
22     PadicInt.ker_toZModPow, Ideal.mem_span_singleton]
23 
24 /-- Integer divisibility is faithfully detected inside the p-adic integers. -/
25 theorem int_pow_dvd_iff (p n : ℕ) [Fact (Nat.Prime p)] (z : ℤ) :
26     (p : ℤ)^n ∣ z ↔ (p : ℤ_[p])^n ∣ (z : ℤ_[p]) := by
27   have h := toZModPow_eq_iff_dvd_sub p n (z : ℤ_[p]) 0
28   simpa only [map_intCast, map_zero, sub_zero, ZMod.intCast_zmod_eq_zero_iff_dvd,
29     Nat.cast_pow] using h
30 
31 /-- Canonical integer representatives of an arbitrary p-adic vector modulo p^n. -/
32 def truncInt (p n : ℕ) [Fact (Nat.Prime p)] (a : Fin d → ℤ_[p]) : Fin d → ℤ :=
33   fun i => ((PadicInt.toZModPow n (a i)).val : ℤ)
34 
35 /-- The canonical integer representative retains exactly the requested precision. -/
36 theorem truncInt_precision (p n : ℕ) [Fact (Nat.Prime p)]
37     (a : Fin d → ℤ_[p]) (i : Fin d) :
38     (p : ℤ_[p])^n ∣ a i - (truncInt p n a i : ℤ_[p]) := by
39   apply (toZModPow_eq_iff_dvd_sub p n _ _).mp
40   simp [truncInt]
41 
42 /-- Evaluation in every residue quotient commutes with canonical truncation. -/
43 theorem truncInt_eval_residue (p n : ℕ) [Fact (Nat.Prime p)]
44     (F : Fin e → MvPolynomial (Fin d) ℤ) (a : Fin d → ℤ_[p]) (i : Fin e) :
45     (evalSystem F (truncInt p n a) i : ZMod (p^n)) =
46       PadicInt.toZModPow n (padicEval p F a i) := by
47   have h := MvPolynomial.hom_eval₂ (F i) (Int.castRingHom ℤ_[p])
48     (PadicInt.toZModPow n) a
49   rw [padicEval, h]
50   change (Int.castRingHom (ZMod (p^n))) (MvPolynomial.eval (truncInt p n a) (F i)) = _
51   rw [MvPolynomial.eval₂_comp]
52   congr 1
53   · ext z
54     simp
55   · funext k
56     simp [truncInt]
57 
58 /-- An exact p-adic polynomial root gives genuine integer roots at every finite precision. -/
59 theorem truncInt_root (p n : ℕ) [Fact (Nat.Prime p)]
60     (F : Fin e → MvPolynomial (Fin d) ℤ) (a : Fin d → ℤ_[p])
61     (ha : ∀ i, padicEval p F a i = 0) :
62     ∀ i, (p : ℤ)^n ∣ evalSystem F (truncInt p n a) i := by
63   intro i
64   have h := truncInt_eval_residue p n F a i
65   rw [ha i, map_zero] at h
66   simpa only [ZMod.intCast_zmod_eq_zero_iff_dvd, Nat.cast_pow] using h
67 
68 /-- An exact root in an integer residue ball produces an actual next-level lift. -/
69 def rootResidueLift (p n : ℕ) [Fact (Nat.Prime p)]
70     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
71     (a : Fin d → ℤ_[p]) (ha : ∀ i, padicEval p F a i = 0)
72     (hax : ∀ i, (p : ℤ_[p])^n ∣ a i - (x i : ℤ_[p])) : ActualLifts p n F x := by
73   refine ⟨⟨fun i => PadicInt.toZModPow (n+1) (a i), ?_⟩, ?_⟩
74   · intro i
75     apply (int_pow_dvd_iff p n _).mpr
76     have hc := dvd_trans (pow_dvd_pow (p : ℤ_[p]) (Nat.le_succ n))
77       (truncInt_precision p (n+1) a i)
78     have h := dvd_sub (hax i) hc
79     simpa only [Int.cast_sub, sub_sub_sub_cancel_left, truncInt] using h
80   · exact truncInt_root p (n+1) F a ha
81 
82 /-- In the square smooth case, any two exact roots over a lower integer root
83 have the same next residue. This uses the checked count of actual lift classes. -/
84 theorem root_next_residue_eq (p n : ℕ) [Fact (Nat.Prime p)] (hn : 1 ≤ n)
85     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
86     (hx : ∀ i, (p : ℤ)^n ∣ evalSystem F x i)
87     (hJ : Function.Surjective (digitJacobian p F x))
88     (a b : Fin d → ℤ_[p])
89     (ha : ∀ i, padicEval p F a i = 0) (hb : ∀ i, padicEval p F b i = 0)
90     (hax : ∀ i, (p : ℤ_[p])^n ∣ a i - (x i : ℤ_[p]))
91     (hbx : ∀ i, (p : ℤ_[p])^n ∣ b i - (x i : ℤ_[p])) :
92     ∀ i, PadicInt.toZModPow (n+1) (a i) = PadicInt.toZModPow (n+1) (b i) := by
93   have hcard : Nat.card (ActualLifts p n F x) = 1 := by
94     simpa only [Nat.sub_self, pow_zero] using smooth_lift_card p n hn F x hx hJ
95   let : Subsingleton (ActualLifts p n F x) := (Nat.card_eq_one_iff_unique.mp hcard).1
96   have h := Subsingleton.elim (rootResidueLift p n F x a ha hax)
97     (rootResidueLift p n F x b hb hbx)
98   intro i
99   exact congrFun (congrArg (fun y : ActualLifts p n F x => y.val.val) h) i
100 
101 /-- Arbitrary exact roots in the same smooth square residue ball coincide.
102 No chosen tower, agreement with a tower limit, or root uniqueness is assumed. -/
103 theorem padic_root_unique (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
104     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
105     (hJ : Function.Surjective (digitJacobian p F x))
106     (a b : Fin d → ℤ_[p])
107     (ha : ∀ i, padicEval p F a i = 0) (hb : ∀ i, padicEval p F b i = 0)
108     (hax : ∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p]))
109     (hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p])) : a = b := by
110   have hab : ∀ n i, (p : ℤ_[p])^(L+n) ∣ a i - b i := by
111     intro n
112     induction n with
113     | zero =>
114         intro i
115         simpa only [Nat.add_zero, sub_sub_sub_cancel_right] using dvd_sub (hax i) (hbx i)
116     | succ n ih =>
117         let y := truncInt p (L+n) a
118         have hay : ∀ i, (p : ℤ_[p])^(L+n) ∣ a i - (y i : ℤ_[p]) :=
119           truncInt_precision p (L+n) a
120         have hby : ∀ i, (p : ℤ_[p])^(L+n) ∣ b i - (y i : ℤ_[p]) := by
121           intro i
122           simpa only [sub_sub_sub_cancel_left] using dvd_sub (hay i) (ih i)
123         have hyx : ∀ i, (p : ℤ) ∣ y i - x i := by
124           intro i
125           have hlow := dvd_trans (pow_dvd_pow (p : ℤ_[p]) (Nat.le_add_right L n)) (hay i)
126           have hdiff : (p : ℤ_[p])^L ∣ ((y i - x i : ℤ) : ℤ_[p]) := by
127             simpa only [Int.cast_sub, sub_sub_sub_cancel_left] using dvd_sub (hax i) hlow
128           exact dvd_trans (by simpa only [pow_one] using pow_dvd_pow (p : ℤ) hL)
129             ((int_pow_dvd_iff p L _).mpr hdiff)
130         have hyJ : Function.Surjective (digitJacobian p F y) := by
131           rw [Komorebi.PolynomialSurjectiveStep.digitJacobian_eq p F x y hyx]
132           exact hJ
133         have heq := root_next_residue_eq p (L+n) (by omega) F y
134           (truncInt_root p (L+n) F a ha) hyJ a b ha hb hay hby
135         intro i
136         simpa only [Nat.add_assoc] using
137           (toZModPow_eq_iff_dvd_sub p (L+n+1) (a i) (b i)).mp (heq i)
138   funext i
139   apply PadicInt.ext_of_toZModPow.mp
140   intro n
141   apply (toZModPow_eq_iff_dvd_sub p n _ _).mpr
142   exact dvd_trans (pow_dvd_pow (p : ℤ_[p]) (Nat.le_add_left n L)) (hab n i)
143 
144 /-- A square system with surjective actual reduced Jacobian has exactly one
145 p-adic root in the prescribed lower residue class. -/
146 theorem exists_unique_padic_root (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
147     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
148     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
149     (hJ : Function.Surjective (digitJacobian p F x)) :
150     ∃! a : Fin d → ℤ_[p],
151       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0) ∧
152       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) := by
153   obtain ⟨a, ha, hax⟩ := exists_padic_root p L hL F x hx hJ
154   refine ⟨a, ⟨ha, hax⟩, ?_⟩
155   intro b hb
156   exact padic_root_unique p L hL F x hJ b a hb.1 ha hb.2 hax
157 
158 #print axioms toZModPow_eq_iff_dvd_sub
159 #print axioms int_pow_dvd_iff
160 #print axioms truncInt
161 #print axioms truncInt_precision
162 #print axioms truncInt_eval_residue
163 #print axioms truncInt_root
164 #print axioms rootResidueLift
165 #print axioms root_next_residue_eq
166 #print axioms padic_root_unique
167 #print axioms exists_unique_padic_root
168 
169 end Komorebi.PolynomialPadicUnique

Back to source controls