PolynomialLocalSurjective.lean

1 module
2 public import PolynomialPadicUnique
3 public import Mathlib.NumberTheory.Padics.ProperSpace
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 open Filter Topology
10 
11 namespace Komorebi.PolynomialLocalSurjective
12 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
13 open Komorebi.PolynomialPadicLift Komorebi.PolynomialPadicUnique
14 
15 variable {d e : ℕ}
16 
17 /-- The actual p-adic residue ball about an integer vector. -/
18 def residueBall (p L : ℕ) [Fact (Nat.Prime p)] (x : Fin d → ℤ) :
19     Set (Fin d → ℤ_[p]) :=
20   {a | ∀ i, (p : ℤ_[p])^L ∣ a i - (x i : ℤ_[p])}
21 
22 theorem isClosed_residueBall (p L : ℕ) [Fact (Nat.Prime p)] (x : Fin d → ℤ) :
23     IsClosed (residueBall p L x) := by
24   simp only [residueBall, ← Ideal.mem_span_singleton,
25     ← PadicInt.norm_le_pow_iff_mem_span_pow, Set.ofPred_forall]
26   exact isClosed_iInter (fun i =>
27     isClosed_le (((continuous_apply i).sub continuous_const).norm) continuous_const)
28 
29 theorem isCompact_residueBall (p L : ℕ) [Fact (Nat.Prime p)] (x : Fin d → ℤ) :
30     IsCompact (residueBall p L x) :=
31   (isClosed_residueBall p L x).isCompact
32 
33 /-- All canonical integer truncations converge to the original p-adic vector. -/
34 theorem truncInt_tendsto (p L : ℕ) [Fact (Nat.Prime p)] (t : Fin d → ℤ_[p]) :
35     Tendsto (fun n i => (truncInt p (L+n) t i : ℤ_[p])) atTop (𝓝 t) := by
36   apply tendsto_pi_nhds.mpr
37   intro i
38   rw [Metric.tendsto_atTop]
39   intro ε hε
40   obtain ⟨N, hN⟩ := PadicInt.exists_pow_neg_lt p hε
41   refine ⟨N, ?_⟩
42   intro n hn
43   have hd : (p : ℤ_[p])^N ∣ t i - (truncInt p (L+n) t i : ℤ_[p]) :=
44     dvd_trans (pow_dvd_pow (p : ℤ_[p]) (by omega)) (truncInt_precision p (L+n) t i)
45   have hb := (PadicInt.norm_le_pow_iff_mem_span_pow
46     (t i - (truncInt p (L+n) t i : ℤ_[p])) N).mpr
47     (Ideal.mem_span_singleton.mpr hd)
48   rw [dist_comm, dist_eq_norm]
49   exact lt_of_le_of_lt hb hN
50 
51 /-- Subtracting a constant target does not alter the actual reduced Jacobian. -/
52 theorem digitJacobian_sub_C (q : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ)
53     (x : Fin d → ℤ) (y : Fin e → ℤ) :
54     digitJacobian q (fun i => F i - MvPolynomial.C (y i)) x =
55       digitJacobian q F x := by
56   ext u i
57   simp [digitJacobian]
58 
59 /-- Every sufficiently close integer output has a p-adic preimage in the base ball. -/
60 theorem exists_integer_target_preimage (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
61     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
62     (hJ : Function.Surjective (digitJacobian p F x)) (y : Fin e → ℤ)
63     (hy : ∀ i, (p : ℤ)^L ∣ y i - evalSystem F x i) :
64     ∃ a : Fin d → ℤ_[p], padicEval p F a = (fun i => (y i : ℤ_[p])) ∧
65       a ∈ residueBall p L x := by
66   have hx : ∀ i, (p : ℤ)^L ∣
67       evalSystem (fun i => F i - MvPolynomial.C (y i)) x i := by
68     intro i
69     simpa only [evalSystem, MvPolynomial.eval_sub, MvPolynomial.eval_C, neg_sub] using
70       (dvd_neg.mpr (hy i))
71   have hJ' : Function.Surjective
72       (digitJacobian p (fun i => F i - MvPolynomial.C (y i)) x) := by
73     rw [digitJacobian_sub_C]
74     exact hJ
75   obtain ⟨a, ha, hax⟩ := exists_padic_root p L hL
76     (fun i => F i - MvPolynomial.C (y i)) x hx hJ'
77   refine ⟨a, ?_, hax⟩
78   funext i
79   have hi := ha i
80   rw [MvPolynomial.eval₂_sub, MvPolynomial.eval₂_C] at hi
81   exact sub_eq_zero.mp hi
82 
83 /-- The compact image contains every p-adic output in the corresponding residue ball.
84 Integer truncations are used only as output approximations, so no compatibility
85 of chosen preimages is assumed. -/
86 theorem exists_padic_preimage (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
87     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
88     (hJ : Function.Surjective (digitJacobian p F x)) (t : Fin e → ℤ_[p])
89     (ht : ∀ i, (p : ℤ_[p])^L ∣ t i - (evalSystem F x i : ℤ_[p])) :
90     ∃ a : Fin d → ℤ_[p], padicEval p F a = t ∧ a ∈ residueBall p L x := by
91   have hcont : Continuous (padicEval p F) := continuous_pi (continuous_padicEval p F)
92   have hclosed : IsClosed (padicEval p F '' residueBall p L x) :=
93     ((isCompact_residueBall p L x).image hcont).isClosed
94   have hmem : ∀ n, (fun i => (truncInt p (L+n) t i : ℤ_[p])) ∈
95       padicEval p F '' residueBall p L x := by
96     intro n
97     have hy : ∀ i, (p : ℤ)^L ∣ truncInt p (L+n) t i - evalSystem F x i := by
98       intro i
99       apply (int_pow_dvd_iff p L _).mpr
100       have hd := dvd_trans (pow_dvd_pow (p : ℤ_[p]) (Nat.le_add_right L n))
101         (truncInt_precision p (L+n) t i)
102       simpa only [Int.cast_sub, sub_sub_sub_cancel_left] using dvd_sub (ht i) hd
103     obtain ⟨a, ha, hax⟩ := exists_integer_target_preimage p L hL F x hJ
104       (truncInt p (L+n) t) hy
105     exact ⟨a, hax, ha⟩
106   have htarget := hclosed.mem_of_tendsto (truncInt_tendsto p L t) (Eventually.of_forall hmem)
107   obtain ⟨a, hax, ha⟩ := htarget
108   exact ⟨a, ha, hax⟩
109 
110 #print axioms residueBall
111 #print axioms isClosed_residueBall
112 #print axioms isCompact_residueBall
113 #print axioms truncInt_tendsto
114 #print axioms digitJacobian_sub_C
115 #print axioms exists_integer_target_preimage
116 #print axioms exists_padic_preimage
117 
118 end Komorebi.PolynomialLocalSurjective

Back to source controls