PolynomialRegularityIntegral.lean

1 module
2 public import PolynomialAnalyticImplicit
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialRegularityIntegral
9 
10 open MvPolynomial Matrix
11 open Komorebi.PolynomialJointSystem
12 open Komorebi.PolynomialWeightedInverse
13 open Komorebi.PolynomialParameterSystem
14 open Komorebi.PolynomialAnalyticEvaluation
15 
16 variable {e k : ℕ}
17 
18 /-- Include the actual integral coefficients in the p-adic field. -/
19 def rationalSystem (p : ℕ) [Fact (Nat.Prime p)]
20     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p]) :
21     Fin e → MvPolynomial (Fin (e + k)) ℚ_[p] :=
22   fun i => (F i).map (algebraMap ℤ_[p] ℚ_[p])
23 
24 /-- Include every coordinate of an integral point in the p-adic field. -/
25 def rationalPoint (p : ℕ) [Fact (Nat.Prime p)] {d : ℕ}
26     (a : Fin d → ℤ_[p]) : Fin d → ℚ_[p] := fun i => (a i : ℚ_[p])
27 
28 /-- Evaluation commutes with the actual coefficient and coordinate inclusions. -/
29 @[simp] theorem eval_rationalSystem (p : ℕ) [Fact (Nat.Prime p)]
30     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
31     (a : Fin (e + k) → ℤ_[p]) (i : Fin e) :
32     eval (rationalPoint p a) (rationalSystem p F i) = (eval a (F i) : ℚ_[p]) := by
33   exact (MvPolynomial.map_eval (algebraMap ℤ_[p] ℚ_[p]) a (F i)).symm
34 
35 /-- Partial differentiation followed by evaluation commutes with coefficient inclusion. -/
36 @[simp] theorem eval_pderiv_rationalSystem (p : ℕ) [Fact (Nat.Prime p)]
37     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
38     (a : Fin (e + k) → ℤ_[p]) (i : Fin e) (j : Fin (e + k)) :
39     eval (rationalPoint p a) (pderiv j (rationalSystem p F i)) =
40       (eval a (pderiv j (F i)) : ℚ_[p]) := by
41   rw [rationalSystem, pderiv_map]
42   exact (MvPolynomial.map_eval (algebraMap ℤ_[p] ℚ_[p]) a (pderiv j (F i))).symm
43 
44 /-- The rational solved Jacobian is the inclusion of the actual integral solved Jacobian. -/
45 @[simp] theorem solvedJacobian_rationalSystem (p : ℕ) [Fact (Nat.Prime p)]
46     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
47     (a : Fin (e + k) → ℤ_[p]) :
48     Komorebi.PolynomialJointSystem.solvedJacobian (rationalSystem p F) (rationalPoint p a) =
49       rationalMatrix p (Komorebi.PolynomialJointSystem.solvedJacobian F a) := by
50   ext i j
51   exact eval_pderiv_rationalSystem p F a i (Fin.castAdd k j)
52 
53 /-- The rectangular parameter Jacobian is also the entrywise inclusion of the actual one. -/
54 @[simp] theorem parameterJacobian_rationalSystem (p : ℕ) [Fact (Nat.Prime p)]
55     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
56     (a : Fin (e + k) → ℤ_[p]) :
57     parameterJacobian (rationalSystem p F) (rationalPoint p a) =
58       fun i j => algebraMap ℤ_[p] ℚ_[p] (parameterJacobian F a i j) := by
59   ext i j
60   exact eval_pderiv_rationalSystem p F a i (Fin.natAdd e j)
61 
62 /-- Every integral exact root remains an exact root after inclusion in the field. -/
63 theorem rationalSystem_root (p : ℕ) [Fact (Nat.Prime p)]
64     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
65     (a : Fin (e + k) → ℤ_[p]) (hF : ∀ i, eval a (F i) = 0) :
66     ∀ i, eval (rationalPoint p a) (rationalSystem p F i) = 0 := by
67   intro i
68   simp [hF]
69 
70 @[simp] theorem rationalPoint_join (p : ℕ) [Fact (Nat.Prime p)]
71     (y : Fin e → ℤ_[p]) (t : Fin k → ℤ_[p]) :
72     rationalPoint p (join y t) = join (rationalPoint p y) (rationalPoint p t) := by
73   ext i
74   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;> simp [rationalPoint]
75 
76 @[simp] theorem rationalPoint_solvedPart (p : ℕ) [Fact (Nat.Prime p)]
77     (a : Fin (e + k) → ℤ_[p]) :
78     solvedPart (rationalPoint p a) = rationalPoint p (solvedPart a) := rfl
79 
80 @[simp] theorem rationalPoint_freePart (p : ℕ) [Fact (Nat.Prime p)]
81     (a : Fin (e + k) → ℤ_[p]) :
82     freePart (rationalPoint p a) = rationalPoint p (freePart a) := rfl
83 
84 /-- Integral coefficients and centers have an analytic implicit solution in the ambient
85 p-adic field. The only nonsingularity hypothesis is on their actual solved Jacobian.
86 The root graph is stated by evaluating the original integral polynomials in the field. -/
87 theorem exists_analytic_integral_implicit (p : ℕ) [Fact (Nat.Prime p)]
88     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
89     (a : Fin (e + k) → ℤ_[p]) (hF : ∀ i, eval a (F i) = 0)
90     (hJ : IsUnit (rationalMatrix p (Komorebi.PolynomialJointSystem.solvedJacobian F a))) :
91     ∃ (ψ : (Fin k → ℚ_[p]) → (Fin e → ℚ_[p])) (U : Set (Fin k → ℚ_[p]))
92       (V : Set (Fin e → ℚ_[p])),
93       IsOpen U ∧ IsOpen V ∧ rationalPoint p (freePart a) ∈ U ∧
94       rationalPoint p (solvedPart a) ∈ V ∧
95       ψ (rationalPoint p (freePart a)) = rationalPoint p (solvedPart a) ∧
96       AnalyticOnNhd ℚ_[p] ψ U ∧ (∀ t ∈ U, ψ t ∈ V) ∧
97       (∀ t ∈ U, ∀ y ∈ V,
98         (∀ i, eval₂ (algebraMap ℤ_[p] ℚ_[p]) (join y t) (F i) = 0) ↔ y = ψ t) ∧
99       HasStrictFDerivAt ψ
100         (matrixCLM (-((rationalMatrix p
101           (Komorebi.PolynomialJointSystem.solvedJacobian F a))⁻¹ *
102           Matrix.of (fun i j => algebraMap ℤ_[p] ℚ_[p] (parameterJacobian F a i j)))))
103         (rationalPoint p (freePart a)) := by
104   have hroot : evalSystem (rationalSystem p F) (rationalPoint p a) = 0 := by
105     ext i
106     exact rationalSystem_root p F a hF i
107   have hunit : IsUnit (Komorebi.PolynomialJointSystem.solvedJacobian
108       (rationalSystem p F) (rationalPoint p a)) := by
109     simpa only [solvedJacobian_rationalSystem] using hJ
110   obtain ⟨ψ, U, V, hU, hV, ht, hy, hψa, hψan, hψV, hgraph, hder⟩ :=
111     Komorebi.PolynomialAnalyticImplicit.exists_analytic_implicit
112       (rationalSystem p F) (rationalPoint p a) hroot hunit
113   refine ⟨ψ, U, V, hU, hV, ht, hy, hψa, hψan, hψV, ?_, ?_⟩
114   · intro t ht' y hy'
115     have h := hgraph t ht' y hy'
116     simpa only [evalSystem, rationalSystem, MvPolynomial.eval_map,
117       funext_iff, Pi.zero_apply] using h
118   · have hK : parameterJacobian (rationalSystem p F) (rationalPoint p a) =
119         Matrix.of (fun i j => algebraMap ℤ_[p] ℚ_[p] (parameterJacobian F a i j)) := by
120       ext i j
121       exact eval_pderiv_rationalSystem p F a i (Fin.natAdd e j)
122     rw [solvedJacobian_rationalSystem, hK, rationalPoint_freePart] at hder
123     exact hder
124 
125 end Komorebi.PolynomialRegularityIntegral

Back to source controls