PolynomialParameterSystem.lean

1 module
2 public import PolynomialPadicLift
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialParameterSystem
9 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
10 open Komorebi.PolynomialPadicLift
11 variable {d e q : ℕ}
12 
13 /-- The coordinates to be solved. -/
14 def solvedPart {R : Type*} (z : Fin (e + q) → R) : Fin e → R :=
15   fun i => z (Fin.castAdd q i)
16 /-- The free coordinates. -/
17 def freePart {R : Type*} (z : Fin (e + q) → R) : Fin q → R :=
18   fun j => z (Fin.natAdd e j)
19 /-- Join solved and free coordinates in their original order. -/
20 def join {R : Type*} (y : Fin e → R) (t : Fin q → R) : Fin (e + q) → R :=
21   Fin.append y t
22 
23 @[simp] theorem join_solved {R : Type*} (y : Fin e → R) (t : Fin q → R) (i : Fin e) :
24     join y t (Fin.castAdd q i) = y i := by simp [join]
25 @[simp] theorem join_free {R : Type*} (y : Fin e → R) (t : Fin q → R) (j : Fin q) :
26     join y t (Fin.natAdd e j) = t j := by simp [join]
27 @[simp] theorem solvedPart_join {R : Type*} (y : Fin e → R) (t : Fin q → R) :
28     solvedPart (join y t) = y := by ext i; simp [solvedPart]
29 @[simp] theorem freePart_join {R : Type*} (y : Fin e → R) (t : Fin q → R) :
30     freePart (join y t) = t := by ext i; simp [freePart]
31 @[simp] theorem join_parts {R : Type*} (z : Fin (e + q) → R) :
32     join (solvedPart z) (freePart z) = z := by
33   ext i
34   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;> simp [solvedPart, freePart]
35 
36 theorem continuous_solvedPart {R : Type*} [TopologicalSpace R] :
37     Continuous (solvedPart (e := e) (q := q) (R := R)) := by
38   exact continuous_pi fun i => continuous_apply _
39 theorem continuous_freePart {R : Type*} [TopologicalSpace R] :
40     Continuous (freePart (e := e) (q := q) (R := R)) := by
41   exact continuous_pi fun i => continuous_apply _
42 theorem continuous_join {R : Type*} [TopologicalSpace R] :
43     Continuous (fun yt : (Fin e → R) × (Fin q → R) => join yt.1 yt.2) := by
44   apply continuous_pi
45   intro i
46   refine Fin.addCases (fun j => ?_) (fun j => ?_) i
47   · simpa only [join_solved, Function.comp_def] using (continuous_apply j).comp continuous_fst
48   · simpa only [join_free, Function.comp_def] using (continuous_apply j).comp continuous_snd
49 
50 /-- Append the free coordinate functions to the polynomial equations. -/
51 def augmented (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) :
52     Fin (e + q) → MvPolynomial (Fin (e + q)) ℤ :=
53   join F (fun j => MvPolynomial.X (Fin.natAdd e j))
54 @[simp] theorem augmented_solved (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (i : Fin e) :
55     augmented F (Fin.castAdd q i) = F i := by simp [augmented]
56 @[simp] theorem augmented_free (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (j : Fin q) :
57     augmented F (Fin.natAdd e j) = MvPolynomial.X (Fin.natAdd e j) := by simp [augmented]
58 
59 theorem evalSystem_augmented (F : Fin e → MvPolynomial (Fin (e + q)) ℤ)
60     (z : Fin (e + q) → ℤ) :
61     evalSystem (augmented F) z = join (evalSystem F z) (freePart z) := by
62   ext i
63   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;>
64     simp [evalSystem, freePart]
65 
66 theorem padicEval_augmented (p : ℕ) [Fact (Nat.Prime p)]
67     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (z : Fin (e + q) → ℤ_[p]) :
68     padicEval p (augmented F) z = join (padicEval p F z) (freePart z) := by
69   ext i
70   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;>
71     simp [padicEval, freePart]
72 
73 theorem padicEval_augmented_iff (p : ℕ) [Fact (Nat.Prime p)]
74     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ)
75     (z : Fin (e + q) → ℤ_[p]) (t : Fin q → ℤ_[p]) :
76     padicEval p (augmented F) z = join 0 t ↔ padicEval p F z = 0 ∧ freePart z = t := by
77   rw [padicEval_augmented]
78   constructor
79   · intro h
80     exact ⟨by simpa using congrArg solvedPart h, by simpa using congrArg freePart h⟩
81   · rintro ⟨hF, ht⟩
82     rw [hF, ht]
83 
84 /-- The actual Jacobian restricted to the solved coordinates. -/
85 def solvedJacobian (p : ℕ) (F : Fin e → MvPolynomial (Fin (e + q)) ℤ)
86     (x : Fin (e + q) → ℤ) : (Fin e → ZMod p) →ₗ[ZMod p] (Fin e → ZMod p) where
87   toFun u i := ∑ k, (MvPolynomial.eval x (MvPolynomial.pderiv (Fin.castAdd q k) (F i)) : ZMod p) * u k
88   map_add' u v := by ext i; simp [mul_add, Finset.sum_add_distrib]
89   map_smul' a u := by
90     ext i
91     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
92     rw [Finset.mul_sum]
93     apply Finset.sum_congr rfl
94     intro k _
95     ring
96 
97 theorem digitJacobian_join_zero (p : ℕ) (F : Fin e → MvPolynomial (Fin (e + q)) ℤ)
98     (x : Fin (e + q) → ℤ) (u : Fin e → ZMod p) :
99     digitJacobian p F x (join u 0) = solvedJacobian p F x u := by
100   ext i
101   simp [digitJacobian, solvedJacobian, Fin.sum_univ_add]
102 
103 theorem digitJacobian_augmented (p : ℕ) (F : Fin e → MvPolynomial (Fin (e + q)) ℤ)
104     (x : Fin (e + q) → ℤ) (u : Fin (e + q) → ZMod p) :
105     digitJacobian p (augmented F) x u = join (digitJacobian p F x u) (freePart u) := by
106   ext i
107   refine Fin.addCases (fun j => ?_) (fun j => ?_) i
108   · simp [digitJacobian]
109   · simp [digitJacobian, freePart, MvPolynomial.pderiv_X, Pi.single_apply, apply_ite]
110 
111 theorem augmented_jacobian_surjective (p : ℕ)
112     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
113     (hJ : Function.Surjective (solvedJacobian p F x)) :
114     Function.Surjective (digitJacobian p (augmented F) x) := by
115   intro b
116   obtain ⟨u, hu⟩ := hJ (solvedPart b - digitJacobian p F x (join 0 (freePart b)))
117   refine ⟨join u (freePart b), ?_⟩
118   rw [digitJacobian_augmented, freePart_join]
119   have hsplit : join u (freePart b) = join u 0 + join 0 (freePart b) := by
120     ext i
121     refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;> simp
122   rw [hsplit, map_add, digitJacobian_join_zero, hu, sub_add_cancel, join_parts]
123 
124 end Komorebi.PolynomialParameterSystem

Back to source controls