PolynomialLocalInverse.lean

1 module
2 public import PolynomialInverseCongruence
3 public import PolynomialLocalSurjective
4 public import Mathlib.Topology.Homeomorph.Lemmas
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialLocalInverse
11 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
12 open Komorebi.PolynomialPadicLift Komorebi.PolynomialInverseCongruence
13 open Komorebi.PolynomialLocalSurjective
14 
15 variable {d e : ℕ}
16 
17 /-- The actual polynomial evaluation restricted to its input and output residue balls. -/
18 def ballMap (p L : ℕ) [Fact (Nat.Prime p)]
19     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
20     residueBall p L x → residueBall p L (evalSystem F x) := fun a =>
21   ⟨padicEval p F a.val, by
22     intro i
23     simpa only [padicEval_intCast] using
24       padicEval_congruent p L F a.val (fun k => (x k : ℤ_[p])) a.property i⟩
25 
26 theorem continuous_ballMap (p L : ℕ) [Fact (Nat.Prime p)]
27     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
28     Continuous (ballMap p L F x) := by
29   apply Continuous.subtype_mk
30   exact (continuous_pi (continuous_padicEval p F)).comp continuous_subtype_val
31 
32 theorem ballMap_bijective (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
33     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
34     (hJ : Function.Surjective (digitJacobian p F x)) :
35     Function.Bijective (ballMap p L F x) := by
36   constructor
37   · intro a b hab
38     apply Subtype.ext
39     apply padic_map_injective p F x hJ a.val b.val
40     · intro i
41       exact ((by simpa only [pow_one] using pow_dvd_pow (p : ℤ_[p]) hL) :
42       (p : ℤ_[p]) ∣ (p : ℤ_[p])^L).trans
43         (a.property i)
44     · intro i
45       exact ((by simpa only [pow_one] using pow_dvd_pow (p : ℤ_[p]) hL) :
46       (p : ℤ_[p]) ∣ (p : ℤ_[p])^L).trans
47         (b.property i)
48     · exact congrArg Subtype.val hab
49   · intro t
50     obtain ⟨a, ha, hax⟩ := exists_padic_preimage p L hL F x hJ t.val t.property
51     exact ⟨⟨a, hax⟩, Subtype.ext ha⟩
52 
53 /-- Smooth square polynomial evaluation is a homeomorphism of the complete residue balls. -/
54 def localHomeomorph (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
55     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
56     (hJ : Function.Surjective (digitJacobian p F x)) :
57     residueBall p L x ≃ₜ residueBall p L (evalSystem F x) := by
58   letI : CompactSpace (residueBall p L x) :=
59     isCompact_iff_compactSpace.mp (isCompact_residueBall p L x)
60   let f := Equiv.ofBijective (ballMap p L F x) (ballMap_bijective p L hL F x hJ)
61   exact Continuous.homeoOfEquivCompactToT2 (f := f) (continuous_ballMap p L F x)
62 
63 theorem localHomeomorph_apply (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
64     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
65     (hJ : Function.Surjective (digitJacobian p F x)) (a : residueBall p L x) :
66     (localHomeomorph p L hL F x hJ a).val = padicEval p F a.val := rfl
67 
68 theorem localHomeomorph_symm_eval (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
69     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
70     (hJ : Function.Surjective (digitJacobian p F x))
71     (t : residueBall p L (evalSystem F x)) :
72     padicEval p F ((localHomeomorph p L hL F x hJ).symm t).val = t.val := by
73   exact congrArg Subtype.val ((localHomeomorph p L hL F x hJ).apply_symm_apply t)
74 
75 theorem localHomeomorph_symm_congruent (p L N : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
76     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
77     (hJ : Function.Surjective (digitJacobian p F x))
78     (t u : residueBall p L (evalSystem F x))
79     (htu : ∀ i, (p : ℤ_[p])^N ∣ t.val i - u.val i) :
80     ∀ i, (p : ℤ_[p])^N ∣
81       ((localHomeomorph p L hL F x hJ).symm t).val i -
82       ((localHomeomorph p L hL F x hJ).symm u).val i := by
83   apply padic_inverse_congruence p N F x hJ
84   · intro i
85     exact ((by simpa only [pow_one] using pow_dvd_pow (p : ℤ_[p]) hL) :
86       (p : ℤ_[p]) ∣ (p : ℤ_[p])^L).trans
87       (((localHomeomorph p L hL F x hJ).symm t).property i)
88   · intro i
89     exact ((by simpa only [pow_one] using pow_dvd_pow (p : ℤ_[p]) hL) :
90       (p : ℤ_[p]) ∣ (p : ℤ_[p])^L).trans
91       (((localHomeomorph p L hL F x hJ).symm u).property i)
92   · simpa only [localHomeomorph_symm_eval] using htu
93 
94 #print axioms ballMap
95 #print axioms continuous_ballMap
96 #print axioms ballMap_bijective
97 #print axioms localHomeomorph
98 #print axioms localHomeomorph_apply
99 #print axioms localHomeomorph_symm_eval
100 #print axioms localHomeomorph_symm_congruent
101 
102 end Komorebi.PolynomialLocalInverse

Back to source controls