PolynomialWeightedLift.lean

1 module
2 public import PolynomialTaylorRing
3 public import PolynomialPadicContraction
4 public import PolynomialWeightedInverse
5 public import PolynomialWeightedNormalization
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PolynomialWeightedLift
12 open MvPolynomial PolynomialWeightedInverse PolynomialPadicContraction
13 variable {d : ℕ}
14 
15 /-- The integral coordinates on the full weighted uniqueness ball. -/
16 def shiftedPoint (p s : ℕ) [Fact p.Prime] (a u : Fin d → ℤ_[p]) : Fin d → ℤ_[p] :=
17   fun i => a i + (p : ℤ_[p]) ^ (s + 1) * u i
18 
19 /-- Polynomial normalization yields a root, its retained precision, and uniqueness
20 throughout the full ball. The actual Taylor normalization is supplied below. -/
21 theorem exists_root_of_normalization (p s r : ℕ) [Fact p.Prime]
22     (hr : 2 * s < r) (F : Fin d → MvPolynomial (Fin d) ℤ_[p])
23     (a : Fin d → ℤ_[p]) (A : Matrix (Fin d) (Fin d) ℤ_[p])
24     (hJA : jacobian F a * A = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
25     (C : Fin d → ℤ_[p]) (Q : Fin d → MvPolynomial (Fin d) ℤ_[p])
26     (hC : ∀ i, (p : ℤ_[p]) ^ (r - (2 * s + 1)) ∣ C i)
27     (hQ : ∀ i, eval (0 : Fin d → ℤ_[p]) (Q i) = 0)
28     (hnorm : ∀ u i, eval (shiftedPoint p s a u) (precondition A F i) =
29       (p : ℤ_[p]) ^ (2 * s + 1) * (C i + u i + (p : ℤ_[p]) * eval u (Q i))) :
30     ∃ b : Fin d → ℤ_[p],
31       (∀ i, eval b (F i) = 0) ∧
32       (∀ i, (p : ℤ_[p]) ^ (r - s) ∣ b i - a i) ∧
33       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
34       (∀ z : Fin d → ℤ_[p], (∀ i, eval z (F i) = 0) →
35         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) := by
36   let H : Fin d → MvPolynomial (Fin d) ℤ_[p] := fun i => -Q i
37   let c : Fin d → ℤ_[p] := fun i => -C i
38   have hH : evalSystem p H 0 = 0 := by
39     funext i
40     change eval (0 : Fin d → ℤ_[p]) (-Q i) = 0
41     rw [map_neg, hQ i, neg_zero]
42   have hc : ∀ i, (p : ℤ_[p]) ^ (r - (2 * s + 1)) ∣ c i :=
43     fun i => dvd_neg.mpr (hC i)
44   obtain ⟨u, hu, huniq⟩ := exists_unique_fixedPoint p H c
45   have hprec := fixedPoint_divisible p (r - (2 * s + 1)) H c u hH hu hc
46   have hp : (p : ℤ_[p]) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero
47   have hroot_iff (w : Fin d → ℤ_[p]) :
48       (∀ i, eval (shiftedPoint p s a w) (F i) = 0) ↔ contractionMap p H c w = w := by
49     have hpre := precondition_root_iff p s A (jacobian F a) hJA F (shiftedPoint p s a w)
50     constructor
51     · intro hw
52       have hg : (fun i => eval (shiftedPoint p s a w) (precondition A F i)) = 0 :=
53         hpre.mpr (funext hw)
54       funext i
55       have hi := congrFun hg i
56       rw [hnorm] at hi
57       have hz : C i + w i + (p : ℤ_[p]) * eval w (Q i) = 0 :=
58         (mul_eq_zero.mp hi).resolve_left (pow_ne_zero _ hp)
59       change -C i + (p : ℤ_[p]) * eval w (-Q i) = w i
60       rw [map_neg]
61       linear_combination -hz
62     · intro hw
63       apply funext_iff.mp (hpre.mp ?_)
64       funext i
65       rw [hnorm]
66       have hi := congrFun hw i
67       change -C i + (p : ℤ_[p]) * eval w (-Q i) = w i at hi
68       rw [map_neg] at hi
69       have hz : C i + w i + (p : ℤ_[p]) * eval w (Q i) = 0 := by
70         linear_combination -hi
71       simp only [hz, mul_zero, Pi.zero_apply]
72   refine ⟨shiftedPoint p s a u, (hroot_iff u).mpr hu, ?_, ?_, ?_⟩
73   · intro i
74     obtain ⟨v, hv⟩ := hprec i
75     refine ⟨v, ?_⟩
76     have he : s + 1 + (r - (2 * s + 1)) = r - s := by omega
77     simp only [shiftedPoint, add_sub_cancel_left]
78     rw [hv, ← mul_assoc, ← pow_add, he]
79   · intro i
80     exact ⟨u i, by simp [shiftedPoint]⟩
81   · intro z hz hball
82     choose w hw using hball
83     have hzw : z = shiftedPoint p s a w := by
84       funext i
85       have hi := hw i
86       change z i = a i + (p : ℤ_[p]) ^ (s + 1) * w i
87       linear_combination hi
88     rw [hzw] at hz ⊢
89     exact congrArg (shiftedPoint p s a) (huniq w ((hroot_iff w).mp hz))
90 
91 /-- Weighted nonlinear lifting for the actual Jacobian, with an effective integral
92 inverse certificate. Uniqueness holds on the entire ball of depth s+1. -/
93 theorem exists_weighted_root_certificate (p s r : ℕ) [Fact p.Prime]
94     (hr : 2 * s < r) (F : Fin d → MvPolynomial (Fin d) ℤ_[p])
95     (a : Fin d → ℤ_[p]) (A : Matrix (Fin d) (Fin d) ℤ_[p])
96     (hAJ : A * jacobian F a = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
97     (hJA : jacobian F a * A = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
98     (hF : ∀ i, (p : ℤ_[p]) ^ r ∣ eval a (F i)) :
99     ∃ b : Fin d → ℤ_[p],
100       (∀ i, eval b (F i) = 0) ∧
101       (∀ i, (p : ℤ_[p]) ^ (r - s) ∣ b i - a i) ∧
102       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
103       (∀ z : Fin d → ℤ_[p], (∀ i, eval z (F i) = 0) →
104         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) := by
105   obtain ⟨C, Q, hC, hQ, hnorm⟩ :=
106     PolynomialWeightedNormalization.exists_normalization p s r hr F a A hAJ hF
107   exact exists_root_of_normalization p s r hr F a A hJA C Q hC hQ hnorm
108 
109 /-- The full weighted lifting theorem under the stated fraction-field inverse bound.
110 Coefficients and the center are arbitrary p-adic integers, and the same exponent s
111 is retained without replacing it by a determinant valuation. -/
112 theorem exists_weighted_root (p s r : ℕ) [Fact p.Prime]
113     (hr : 2 * s < r) (F : Fin d → MvPolynomial (Fin d) ℤ_[p])
114     (a : Fin d → ℤ_[p]) (hJ : IsUnit (rationalMatrix p (jacobian F a)))
115     (hbound : ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
116       rationalMatrix p A = (p : ℚ_[p]) ^ s • (rationalMatrix p (jacobian F a))⁻¹)
117     (hF : ∀ i, (p : ℤ_[p]) ^ r ∣ eval a (F i)) :
118     ∃ b : Fin d → ℤ_[p],
119       (∀ i, eval b (F i) = 0) ∧
120       (∀ i, (p : ℤ_[p]) ^ (r - s) ∣ b i - a i) ∧
121       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) ∧
122       (∀ z : Fin d → ℤ_[p], (∀ i, eval z (F i) = 0) →
123         (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ z i - a i) → z = b) := by
124   obtain ⟨A, hAJ, hJA⟩ := (bounded_inverse_iff_certificate p s (jacobian F a)).mp ⟨hJ, hbound⟩
125   exact exists_weighted_root_certificate p s r hr F a A hAJ hJA hF
126 
127 /-- Unique-existence presentation, with uniqueness in the full ball as predicate. -/
128 theorem exists_unique_weighted_root (p s r : ℕ) [Fact p.Prime]
129     (hr : 2 * s < r) (F : Fin d → MvPolynomial (Fin d) ℤ_[p])
130     (a : Fin d → ℤ_[p]) (hJ : IsUnit (rationalMatrix p (jacobian F a)))
131     (hbound : ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
132       rationalMatrix p A = (p : ℚ_[p]) ^ s • (rationalMatrix p (jacobian F a))⁻¹)
133     (hF : ∀ i, (p : ℤ_[p]) ^ r ∣ eval a (F i)) :
134     (∃! b : Fin d → ℤ_[p], (∀ i, eval b (F i) = 0) ∧
135       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i)) ∧
136     (∀ b : Fin d → ℤ_[p], (∀ i, eval b (F i) = 0) →
137       (∀ i, (p : ℤ_[p]) ^ (s + 1) ∣ b i - a i) →
138       ∀ i, (p : ℤ_[p]) ^ (r - s) ∣ b i - a i) := by
139   obtain ⟨b, hb, hprec, hball, huniq⟩ := exists_weighted_root p s r hr F a hJ hbound hF
140   constructor
141   · exact ⟨b, ⟨hb, hball⟩, fun z hz => huniq z hz.1 hz.2⟩
142   · intro z hz hzb
143     rw [huniq z hz hzb]
144     exact hprec
145 
146 end Komorebi.PolynomialWeightedLift

Back to source controls