PolynomialParameterChart.lean

1 module
2 public import PolynomialLocalInverse
3 public import PolynomialParameterSystem
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialParameterChart
10 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
11 open Komorebi.PolynomialPadicLift Komorebi.PolynomialPadicUnique
12 open Komorebi.PolynomialLocalSurjective Komorebi.PolynomialLocalInverse
13 open Komorebi.PolynomialParameterSystem
14 variable {e q : ℕ}
15 
16 /-- The target with zero polynomial residual and the prescribed free coordinates. -/
17 def chartTarget (p L : ℕ) [Fact (Nat.Prime p)]
18     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
19     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
20     (t : residueBall p L (freePart x)) :
21     residueBall p L (evalSystem (augmented F) x) :=
22   ⟨join 0 t.val, by
23     intro i
24     refine Fin.addCases (fun j => ?_) (fun j => ?_) i
25     · simpa only [join_solved, Pi.zero_apply, evalSystem_augmented, zero_sub] using
26         dvd_neg.mpr ((int_pow_dvd_iff p L _).mp (hx j))
27     · simpa only [evalSystem_augmented, join_free] using t.property j⟩
28 
29 theorem continuous_chartTarget (p L : ℕ) [Fact (Nat.Prime p)]
30     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
31     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i) :
32     Continuous (chartTarget p L F x hx) := by
33   apply Continuous.subtype_mk
34   exact continuous_join.comp (continuous_const.prodMk continuous_subtype_val)
35 
36 def chartPoint (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
37     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
38     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
39     (hJ : Function.Surjective (solvedJacobian p F x))
40     (t : residueBall p L (freePart x)) : residueBall p L x :=
41   (localHomeomorph p L hL (augmented F) x
42     (augmented_jacobian_surjective p F x hJ)).symm (chartTarget p L F x hx t)
43 
44 theorem chartPoint_spec (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
45     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
46     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
47     (hJ : Function.Surjective (solvedJacobian p F x))
48     (t : residueBall p L (freePart x)) :
49     padicEval p F (chartPoint p L hL F x hx hJ t).val = 0 ∧
50       freePart (chartPoint p L hL F x hx hJ t).val = t.val := by
51   apply (padicEval_augmented_iff p F _ t.val).mp
52   exact localHomeomorph_symm_eval p L hL (augmented F) x
53     (augmented_jacobian_surjective p F x hJ) (chartTarget p L F x hx t)
54 
55 theorem chartPoint_root (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
56     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
57     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
58     (hJ : Function.Surjective (solvedJacobian p F x))
59     (t : residueBall p L (freePart x)) :
60     padicEval p F (chartPoint p L hL F x hx hJ t).val = 0 :=
61   (chartPoint_spec p L hL F x hx hJ t).1
62 
63 theorem chartPoint_free (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
64     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
65     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
66     (hJ : Function.Surjective (solvedJacobian p F x))
67     (t : residueBall p L (freePart x)) :
68     freePart (chartPoint p L hL F x hx hJ t).val = t.val :=
69   (chartPoint_spec p L hL F x hx hJ t).2
70 
71 theorem chartPoint_unique (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
72     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
73     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
74     (hJ : Function.Surjective (solvedJacobian p F x))
75     (t : residueBall p L (freePart x)) (z : residueBall p L x)
76     (hz : padicEval p F z.val = 0) (ht : freePart z.val = t.val) :
77     z = chartPoint p L hL F x hx hJ t := by
78   apply (localHomeomorph p L hL (augmented F) x
79     (augmented_jacobian_surjective p F x hJ)).injective
80   apply Subtype.ext
81   change padicEval p (augmented F) z.val =
82     padicEval p (augmented F) (chartPoint p L hL F x hx hJ t).val
83   rw [padicEval_augmented, padicEval_augmented, hz, ht,
84     chartPoint_root, chartPoint_free]
85 
86 theorem continuous_chartPoint (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
87     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
88     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
89     (hJ : Function.Surjective (solvedJacobian p F x)) :
90     Continuous (chartPoint p L hL F x hx hJ) :=
91   (localHomeomorph p L hL (augmented F) x
92     (augmented_jacobian_surjective p F x hJ)).symm.continuous.comp
93       (continuous_chartTarget p L F x hx)
94 
95 theorem chartPoint_congruent (p L N : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
96     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
97     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
98     (hJ : Function.Surjective (solvedJacobian p F x))
99     (t u : residueBall p L (freePart x))
100     (htu : ∀ j, (p : ℤ_[p])^N ∣ t.val j - u.val j) :
101     ∀ i, (p : ℤ_[p])^N ∣ (chartPoint p L hL F x hx hJ t).val i -
102       (chartPoint p L hL F x hx hJ u).val i := by
103   apply localHomeomorph_symm_congruent p L N hL (augmented F) x
104     (augmented_jacobian_surjective p F x hJ)
105   intro i
106   change (p : ℤ_[p])^N ∣ join (0 : Fin e → ℤ_[p]) t.val i - join 0 u.val i
107   refine Fin.addCases (fun j => ?_) (fun j => ?_) i
108   · simp only [join_solved, sub_self, dvd_zero]
109   · simpa only [join_free] using htu j
110 
111 def chartPhi (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
112     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
113     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
114     (hJ : Function.Surjective (solvedJacobian p F x))
115     (t : residueBall p L (freePart x)) : Fin e → ℤ_[p] :=
116   solvedPart (chartPoint p L hL F x hx hJ t).val
117 
118 theorem continuous_chartPhi (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
119     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
120     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
121     (hJ : Function.Surjective (solvedJacobian p F x)) :
122     Continuous (chartPhi p L hL F x hx hJ) :=
123   continuous_solvedPart.comp (continuous_subtype_val.comp
124     (continuous_chartPoint p L hL F x hx hJ))
125 
126 theorem chartPoint_graph (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
127     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
128     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
129     (hJ : Function.Surjective (solvedJacobian p F x))
130     (t : residueBall p L (freePart x)) :
131     join (chartPhi p L hL F x hx hJ t) t.val =
132       (chartPoint p L hL F x hx hJ t).val := by
133   rw [← chartPoint_free p L hL F x hx hJ t]
134   exact join_parts _
135 
136 theorem chartGraph_iff (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
137     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
138     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
139     (hJ : Function.Surjective (solvedJacobian p F x))
140     (t : residueBall p L (freePart x)) (z : residueBall p L x) :
141     (padicEval p F z.val = 0 ∧ freePart z.val = t.val) ↔
142       z.val = join (chartPhi p L hL F x hx hJ t) t.val := by
143   rw [chartPoint_graph]
144   constructor
145   · rintro ⟨hz, ht⟩
146     exact congrArg Subtype.val (chartPoint_unique p L hL F x hx hJ t z hz ht)
147   · intro h
148     rw [h]
149     exact chartPoint_spec p L hL F x hx hJ t
150 
151 theorem chartPoint_congruent_iff (p L N : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
152     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
153     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
154     (hJ : Function.Surjective (solvedJacobian p F x))
155     (t u : residueBall p L (freePart x)) :
156     (∀ j, (p : ℤ_[p])^N ∣ t.val j - u.val j) ↔
157       (∀ i, (p : ℤ_[p])^N ∣ (chartPoint p L hL F x hx hJ t).val i -
158         (chartPoint p L hL F x hx hJ u).val i) := by
159   constructor
160   · exact chartPoint_congruent p L N hL F x hx hJ t u
161   · intro h j
162     have ht := congrFun (chartPoint_free p L hL F x hx hJ t) j
163     have hu := congrFun (chartPoint_free p L hL F x hx hJ u) j
164     simpa only [freePart] using (ht ▸ hu ▸ h (Fin.natAdd e j))
165 
166 /-- The whole root locus is continuously and uniquely parameterized by its free coordinates. -/
167 def parameterHomeomorph (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
168     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
169     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
170     (hJ : Function.Surjective (solvedJacobian p F x)) :
171     residueBall p L (freePart x) ≃ₜ {z : residueBall p L x // padicEval p F z.val = 0} where
172   toFun t := ⟨chartPoint p L hL F x hx hJ t, chartPoint_root p L hL F x hx hJ t⟩
173   invFun z := ⟨freePart z.val.val, fun j => z.val.property (Fin.natAdd e j)⟩
174   left_inv t := Subtype.ext (chartPoint_free p L hL F x hx hJ t)
175   right_inv z := by
176     apply Subtype.ext
177     exact (chartPoint_unique p L hL F x hx hJ _ z.val z.property rfl).symm
178   continuous_toFun := by
179     apply Continuous.subtype_mk
180     exact continuous_chartPoint p L hL F x hx hJ
181   continuous_invFun := by
182     apply Continuous.subtype_mk
183     exact continuous_freePart.comp (continuous_subtype_val.comp continuous_subtype_val)
184 
185 #print axioms chartTarget
186 #print axioms continuous_chartTarget
187 #print axioms chartPoint
188 #print axioms chartPoint_spec
189 #print axioms chartPoint_root
190 #print axioms chartPoint_free
191 #print axioms chartPoint_unique
192 #print axioms continuous_chartPoint
193 #print axioms chartPoint_congruent
194 #print axioms chartPhi
195 #print axioms continuous_chartPhi
196 #print axioms chartPoint_graph
197 #print axioms chartGraph_iff
198 #print axioms chartPoint_congruent_iff
199 #print axioms parameterHomeomorph
200 
201 end Komorebi.PolynomialParameterChart

Back to source controls