PolynomialCoordinateReorder.lean

1 module
2 public import PolynomialParameterSystem
3 public import PolynomialMinorSelection
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialCoordinateReorder
10 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
11 open Komorebi.PolynomialPadicLift Komorebi.PolynomialParameterSystem
12 open Komorebi.PolynomialMinorSelection
13 variable {d e q : ℕ}
14 
15 /-- Reorder coordinates by a permutation. -/
16 def reorderPoint {R : Type*} (σ : Equiv.Perm (Fin d)) (x : Fin d → R) : Fin d → R :=
17   fun i => x (σ i)
18 /-- Rename actual polynomial variables consistently with reordered coordinates. -/
19 def reorderSystem (σ : Equiv.Perm (Fin d)) (F : Fin e → MvPolynomial (Fin d) ℤ) :
20     Fin e → MvPolynomial (Fin d) ℤ := fun i => MvPolynomial.rename σ.symm (F i)
21 
22 @[simp] theorem reorderPoint_inverse {R : Type*} (σ : Equiv.Perm (Fin d)) (x : Fin d → R) :
23     reorderPoint σ.symm (reorderPoint σ x) = x := by ext i; simp [reorderPoint]
24 @[simp] theorem reorderPoint_inverse' {R : Type*} (σ : Equiv.Perm (Fin d)) (x : Fin d → R) :
25     reorderPoint σ (reorderPoint σ.symm x) = x := by ext i; simp [reorderPoint]
26 
27 theorem continuous_reorderPoint {R : Type*} [TopologicalSpace R] (σ : Equiv.Perm (Fin d)) :
28     Continuous (reorderPoint (R := R) σ) := by exact continuous_pi fun i => continuous_apply _
29 
30 theorem evalSystem_reorder (σ : Equiv.Perm (Fin d))
31     (F : Fin e → MvPolynomial (Fin d) ℤ) (z : Fin d → ℤ) :
32     evalSystem (reorderSystem σ F) z = evalSystem F (reorderPoint σ.symm z) := by
33   ext i
34   simp only [evalSystem, reorderSystem, MvPolynomial.eval_rename]
35   rfl
36 
37 theorem evalSystem_reorder_at (σ : Equiv.Perm (Fin d))
38     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
39     evalSystem (reorderSystem σ F) (reorderPoint σ x) = evalSystem F x := by
40   rw [evalSystem_reorder, reorderPoint_inverse]
41 
42 theorem padicEval_reorder (p : ℕ) [Fact (Nat.Prime p)] (σ : Equiv.Perm (Fin d))
43     (F : Fin e → MvPolynomial (Fin d) ℤ) (z : Fin d → ℤ_[p]) :
44     padicEval p (reorderSystem σ F) z = padicEval p F (reorderPoint σ.symm z) := by
45   ext i
46   simp only [padicEval, reorderSystem, MvPolynomial.eval₂_rename]
47   rfl
48 
49 theorem padicEval_reorder_at (p : ℕ) [Fact (Nat.Prime p)] (σ : Equiv.Perm (Fin d))
50     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ_[p]) :
51     padicEval p (reorderSystem σ F) (reorderPoint σ x) = padicEval p F x := by
52   rw [padicEval_reorder, reorderPoint_inverse]
53 
54 theorem pderiv_reorder (σ : Equiv.Perm (Fin d))
55     (F : Fin e → MvPolynomial (Fin d) ℤ) (i : Fin e) (k : Fin d) :
56     MvPolynomial.pderiv k (reorderSystem σ F i) =
57       MvPolynomial.rename σ.symm (MvPolynomial.pderiv (σ k) (F i)) := by
58   simpa only [Equiv.symm_apply_apply, reorderSystem] using
59     MvPolynomial.pderiv_rename σ.symm.injective (σ k) (F i)
60 
61 theorem pderiv_eval_reorder (σ : Equiv.Perm (Fin d))
62     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) (i : Fin e) (k : Fin d) :
63     MvPolynomial.eval (reorderPoint σ x) (MvPolynomial.pderiv k (reorderSystem σ F i)) =
64       MvPolynomial.eval x (MvPolynomial.pderiv (σ k) (F i)) := by
65   rw [pderiv_reorder, MvPolynomial.eval_rename]
66   have hx : reorderPoint σ x ∘ σ.symm = x := by
67     ext j
68     simp [reorderPoint]
69   rw [hx]
70 
71 theorem digitJacobian_single (p : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ)
72     (x : Fin d → ℤ) (k : Fin d) (i : Fin e) :
73     digitJacobian p F x (Pi.single k 1) i =
74       (MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) : ZMod p) := by
75   classical
76   simp [digitJacobian, Pi.single_apply, apply_ite]
77 
78 theorem solvedJacobian_reorder_apply (p : ℕ) (σ : Equiv.Perm (Fin (e + q)))
79     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
80     (u : Fin e → ZMod p) :
81     solvedJacobian p (reorderSystem σ F) (reorderPoint σ x) u =
82       ∑ k, u k • digitJacobian p F x (Pi.single (σ (Fin.castAdd q k)) 1) := by
83   ext i
84   simp only [solvedJacobian, LinearMap.coe_mk, AddHom.coe_mk, pderiv_eval_reorder,
85     Finset.sum_apply, Pi.smul_apply, smul_eq_mul, digitJacobian_single]
86   apply Finset.sum_congr rfl
87   intro k _
88   ring
89 
90 theorem exists_reorder_solvedJacobian_surjective (p : ℕ) [Fact (Nat.Prime p)]
91     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
92     (hJ : Function.Surjective (digitJacobian p F x)) :
93     ∃ σ : Equiv.Perm (Fin (e + q)),
94       Function.Surjective (solvedJacobian p (reorderSystem σ F) (reorderPoint σ x)) := by
95   obtain ⟨σ, hσ⟩ := exists_prime_permuted_columns p (digitJacobian p F x) hJ
96   refine ⟨σ, ?_⟩
97   intro b
98   obtain ⟨u, hu⟩ := hσ b
99   exact ⟨u, by rw [solvedJacobian_reorder_apply]; exact hu⟩
100 
101 end Komorebi.PolynomialCoordinateReorder

Back to source controls