PolynomialHomeomorphContract.lean

1 module
2 public import PolynomialLocalInverse
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialHomeomorphContract
8 open MvPolynomial
9 variable {d : ℕ}
10 
11 /-- The homeomorphism is the actual polynomial map, and its inverse solves every output. -/
12 theorem square_homeomorphism (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
13     (F : Fin d → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
14     (hJ : Function.Surjective (fun u : Fin d → ZMod p => fun i =>
15       ∑ j, (eval x (pderiv j (F i)) : ZMod p) * u j)) :
16     ∃ h : {a : Fin d → ℤ_[p] // ∀ j, (p : ℤ_[p])^L ∣ a j - (x j : ℤ_[p])} ≃ₜ
17       {t : Fin d → ℤ_[p] // ∀ i, (p : ℤ_[p])^L ∣ t i - (eval x (F i) : ℤ_[p])},
18       (∀ a i, (h a).val i = eval₂ (Int.castRingHom ℤ_[p]) a.val (F i)) ∧
19       (∀ t i, eval₂ (Int.castRingHom ℤ_[p]) (h.symm t).val (F i) = t.val i) ∧
20       (∀ N t u, (∀ i, (p : ℤ_[p])^N ∣ t.val i - u.val i) →
21         ∀ j, (p : ℤ_[p])^N ∣ (h.symm t).val j - (h.symm u).val j) := by
22   refine ⟨PolynomialLocalInverse.localHomeomorph p L hL F x hJ, ?_, ?_, ?_⟩
23   · intro a i
24     rfl
25   · intro t i
26     exact congrFun (PolynomialLocalInverse.localHomeomorph_symm_eval p L hL F x hJ t) i
27   · intro N t u htu
28     exact PolynomialLocalInverse.localHomeomorph_symm_congruent p L N hL F x hJ t u htu
29 
30 end Komorebi.PolynomialHomeomorphContract

Back to source controls