PolynomialPadicLift.lean

1 module
2 public import PolynomialSmoothCounts
3 public import PadicTowerLimit
4 public import Mathlib.Topology.Algebra.MvPolynomial
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 open Filter Topology
11 
12 namespace Komorebi.PolynomialPadicLift
13 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
14 open Komorebi.PolynomialIntegerTower Komorebi.PolynomialSmoothCounts
15 variable {d e : ℕ}
16 
17 /-- Evaluation of the original integer polynomials in the actual p-adic integers. -/
18 def padicEval (p : ℕ) [Fact (Nat.Prime p)]
19     (F : Fin e → MvPolynomial (Fin d) ℤ) (a : Fin d → ℤ_[p]) : Fin e → ℤ_[p] :=
20   fun i => MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i)
21 
22 /-- Coefficient casting commutes with evaluation of every original polynomial. -/
23 theorem padicEval_intCast (p : ℕ) [Fact (Nat.Prime p)]
24     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) (i : Fin e) :
25     padicEval p F (fun k => (x k : ℤ_[p])) i = (evalSystem F x i : ℤ_[p]) := by
26   exact (MvPolynomial.eval₂_comp (Int.castRingHom ℤ_[p]) x (F i)).symm
27 
28 /-- The actual polynomial evaluation is continuous in the p-adic product topology. -/
29 theorem continuous_padicEval (p : ℕ) [Fact (Nat.Prime p)]
30     (F : Fin e → MvPolynomial (Fin d) ℤ) (i : Fin e) :
31     Continuous (fun a : Fin d → ℤ_[p] => padicEval p F a i) := by
32   simpa only [padicEval, MvPolynomial.eval_map] using
33     (MvPolynomial.continuous_eval ((F i).map (Int.castRingHom ℤ_[p])))
34 
35 /-- A convergent polynomial tower with diverging residual precision has an exact root as its limit. -/
36 theorem polynomial_tower_limit_root (p L : ℕ) [Fact (Nat.Prime p)]
37     (F : Fin e → MvPolynomial (Fin d) ℤ) (z : ℕ → Fin d → ℤ)
38     (a : Fin d → ℤ_[p])
39     (hroot : ∀ n i, (p : ℤ)^(L+n) ∣ evalSystem F (z n) i)
40     (hlim : Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 a)) :
41     ∀ i, padicEval p F a i = 0 := by
42   intro i
43   have heval := ((continuous_padicEval p F i).tendsto a).comp hlim
44   have hzero := PadicTowerLimit.divisible_int_tendsto_zero p L
45     (fun n => evalSystem F (z n) i) (fun n => hroot n i)
46   have hcast : (fun n => padicEval p F (fun k => (z n k : ℤ_[p])) i) =
47       (fun n => (evalSystem F (z n) i : ℤ_[p])) := by
48     funext n
49     exact padicEval_intCast p F (z n) i
50   change Tendsto (fun n => padicEval p F (fun k => (z n k : ℤ_[p])) i)
51     atTop (𝓝 (padicEval p F a i)) at heval
52   rw [hcast] at heval
53   exact tendsto_nhds_unique heval hzero
54 
55 /-- A surjective initial reduced Jacobian gives an actual convergent tower,
56 a p-adic root, all retained precisions, a constant reduced Jacobian, and exact branching. -/
57 theorem exists_padic_root_with_tower (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
58     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
59     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
60     (hJ : Function.Surjective (digitJacobian p F x)) :
61     ∃ z : ℕ → Fin d → ℤ, ∃ a : Fin d → ℤ_[p],
62       z 0 = x ∧
63       (∀ n i, (p : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
64       (∀ n i, (p : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
65       Tendsto (fun n i => (z n i : ℤ_[p])) atTop (𝓝 a) ∧
66       (∀ n i, (p : ℤ_[p])^(L+n) ∣ a i - (z n i : ℤ_[p])) ∧
67       (∀ i, padicEval p F a i = 0) ∧
68       (∀ n, digitJacobian p F (z n) = digitJacobian p F x) ∧
69       (∀ n, Nat.card (PolynomialLiftCounts.ActualLifts p (L+n) F (z n)) = p^(d-e)) := by
70   obtain ⟨z, hz0, hroot, hstep, _, hcount⟩ := exists_regular_tower p L hL F x hx hJ
71   obtain ⟨a, ha, hprecision⟩ :=
72     PadicTowerLimit.compatible_vector_tower_limit p L z hstep
73   refine ⟨z, a, hz0, hroot, hstep, ha, hprecision,
74     polynomial_tower_limit_root p L F z a hroot ha, ?_, hcount⟩
75   intro n
76   rw [← hz0]
77   exact tower_digitJacobian_eq p L hL F z hstep n
78 
79 /-- Every smooth lower polynomial root lifts to an exact p-adic root in the
80 same prescribed residue class. Only the initial Jacobian is assumed surjective. -/
81 theorem exists_padic_root (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
82     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
83     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
84     (hJ : Function.Surjective (digitJacobian p F x)) :
85     ∃ a : Fin d → ℤ_[p],
86       (∀ i, MvPolynomial.eval₂ (Int.castRingHom ℤ_[p]) a (F i) = 0) ∧
87       (∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])) := by
88   obtain ⟨z, a, hz0, _, _, _, hprecision, hroot, _, _⟩ :=
89     exists_padic_root_with_tower p L hL F x hx hJ
90   refine ⟨a, hroot, ?_⟩
91   intro i
92   simpa only [Nat.add_zero, hz0] using hprecision 0 i
93 
94 end Komorebi.PolynomialPadicLift

Back to source controls