PolynomialObstruction.lean

1 module
2 public import AffineObstructionCore
3 public import Mathlib.Algebra.MvPolynomial.PDeriv
4 public import PolynomialTaylor
5 
6 /-!
7 # Finite polynomial obstruction at a fixed presentation
8 
9 The Jacobian below is computed from the actual multivariable polynomials.
10 The one-step criterion uses their Taylor remainder, not a linearization premise.
11 -/
12 
13 @[expose] public section
14 
15 noncomputable section
16 set_option autoImplicit false
17 
18 namespace Komorebi.PolynomialObstruction
19 
20 open Komorebi.NativeAffine
21 
22 variable {d e : ℕ}
23 
24 /-- Evaluation of the given finite list of integer polynomials. -/
25 def evalSystem (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) : Fin e → ℤ :=
26   fun i => MvPolynomial.eval x (F i)
27 
28 /-- The actual Jacobian, acting on an integer correction vector. -/
29 def jacobian (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
30     (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ) where
31   toFun t i := ∑ k, MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) * t k
32   map_add' t u := by
33     ext i
34     simp [mul_add, Finset.sum_add_distrib]
35   map_smul' a t := by
36     ext i
37     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
38     rw [Finset.mul_sum]
39     apply Finset.sum_congr rfl
40     intro k _
41     ring
42 
43 theorem evalSystem_apply (F : Fin e → MvPolynomial (Fin d) ℤ)
44     (x : Fin d → ℤ) (i : Fin e) :
45     evalSystem F x i = MvPolynomial.eval x (F i) := rfl
46 
47 theorem jacobian_apply (F : Fin e → MvPolynomial (Fin d) ℤ)
48     (x t : Fin d → ℤ) (i : Fin e) :
49     jacobian F x t i = ∑ k, MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) * t k := rfl
50 
51 /-- A lower-level solution has an exact integer residual. -/
52 theorem residual_exists (q L : ℕ)
53     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
54     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i) :
55     ∃ r : Fin e → ℤ, evalSystem F x = (q : ℤ)^L • r := by
56   choose r hr using hx
57   exact ⟨r, funext hr⟩
58 
59 theorem residual_unique (q L : ℕ) (hq : 0 < q)
60     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
61     (r s : Fin e → ℤ)
62     (hr : evalSystem F x = (q : ℤ)^L • r)
63     (hs : evalSystem F x = (q : ℤ)^L • s) : r = s := by
64   have hqL : (q : ℤ)^L ≠ 0 := pow_ne_zero _ (Int.natCast_ne_zero.mpr (Nat.ne_of_gt hq))
65   ext i
66   exact mul_left_cancel₀ hqL (congrFun (hr.symm.trans hs) i)
67 
68 /-- Subtracting a multiple of the modulus preserves divisibility. -/
69 theorem dvd_iff_of_dvd_sub (m a b : ℤ) (h : m ∣ a - b) :
70     m ∣ a ↔ m ∣ b := by
71   constructor
72   · intro ha
73     simpa using dvd_sub ha h
74   · intro hb
75     simpa using dvd_add h hb
76 
77 /-- Taylor expansion transports the exact residual up to the next modulus. -/
78 theorem taylor_residual_dvd (q L : ℕ) (hL : 1 ≤ L)
79     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
80     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
81     (t : Fin d → ℤ) (i : Fin e) :
82     (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • t) i -
83       (q : ℤ)^L * (r + jacobian F x t) i := by
84   have hx : MvPolynomial.eval x (F i) = (q : ℤ)^L * r i := congrFun hr i
85   have ht := Komorebi.PolynomialTaylor.taylor_step_dvd (F i) x t q L hL
86   have hshift : x + (q : ℤ)^L • t = fun k => x k + (q : ℤ)^L * t k := by
87     ext k
88     simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul]
89   rw [hshift]
90   convert ht using 1
91   dsimp [evalSystem, jacobian, Komorebi.PolynomialTaylor.directional]
92   rw [hx]
93   ring
94 
95 /-- Each integer correction lifts exactly when its actual Jacobian digit cancels
96 the residual. This is uniform in the polynomial list and the correction. -/
97 theorem next_level_iff_digit (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
98     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
99     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
100     (t : Fin d → ℤ) :
101     (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • t) i) ↔
102       reduction q e (r + jacobian F x t) = 0 := by
103   rw [reduction_zero_iff]
104   apply forall_congr'
105   intro i
106   rw [dvd_iff_of_dvd_sub _ _ _ (taylor_residual_dvd q L hL F x r hr t i)]
107   have hqL : (q : ℤ)^L ≠ 0 := pow_ne_zero _ (Int.natCast_ne_zero.mpr (Nat.ne_of_gt hq))
108   rw [pow_succ, mul_dvd_mul_iff_left hqL]
109 
110 /-- The finite cokernel decides the existence of a next-level digit correction. -/
111 theorem polynomial_lift_iff_obstruction_zero (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
112     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
113     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r) :
114     (∃ t : Fin d → ℤ, ∀ i,
115       (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • t) i) ↔
116       obstruction q (jacobian F x) r = 0 := by
117   rw [obstruction_zero_iff_correction]
118   exact exists_congr fun t => next_level_iff_digit q L hq hL F x r hr t
119 
120 /-- The same criterion stated directly for all representatives of the lower
121 residue vector, rather than a chosen correction parametrization. -/
122 theorem polynomial_same_residue_lift_iff (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
123     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
124     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r) :
125     (∃ y : Fin d → ℤ,
126       (∀ i, (q : ℤ)^L ∣ (y - x) i) ∧
127       (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F y i)) ↔
128       obstruction q (jacobian F x) r = 0 := by
129   rw [← polynomial_lift_iff_obstruction_zero q L hq hL F x r hr]
130   constructor
131   · rintro ⟨y, hy, hFy⟩
132     obtain ⟨t, rfl⟩ := (same_residue_iff ((q : ℤ)^L) x y).mp hy
133     exact ⟨t, hFy⟩
134   · rintro ⟨t, ht⟩
135     exact ⟨x + (q : ℤ)^L • t,
136       (same_residue_iff ((q : ℤ)^L) x _).mpr ⟨t, rfl⟩, ht⟩
137 
138 /-- Every solution of a fixed finite polynomial presentation has an explicit
139 finite obstruction, with vanishing equivalent to an actual one-step lift.
140 The modulus may be composite and may equal one. -/
141 theorem finite_polynomial_obstruction (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
142     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
143     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i) :
144     ∃ r : Fin e → ℤ,
145       evalSystem F x = (q : ℤ)^L • r ∧
146       Finite (Obstruction q (jacobian F x)) ∧
147       ((∃ y : Fin d → ℤ,
148         (∀ i, (q : ℤ)^L ∣ (y - x) i) ∧
149         (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F y i)) ↔
150           obstruction q (jacobian F x) r = 0) := by
151   obtain ⟨r, hr⟩ := residual_exists q L F x hx
152   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
153   exact ⟨r, hr, obstruction_finite q (jacobian F x),
154     polynomial_same_residue_lift_iff q L hq hL F x r hr⟩
155 
156 #print axioms evalSystem
157 #print axioms jacobian
158 #print axioms evalSystem_apply
159 #print axioms jacobian_apply
160 #print axioms residual_exists
161 #print axioms residual_unique
162 #print axioms dvd_iff_of_dvd_sub
163 #print axioms taylor_residual_dvd
164 #print axioms next_level_iff_digit
165 #print axioms polynomial_lift_iff_obstruction_zero
166 #print axioms polynomial_same_residue_lift_iff
167 #print axioms finite_polynomial_obstruction
168 
169 end Komorebi.PolynomialObstruction

Back to source controls