PolynomialGeneralChartContract.lean

1 module
2 public import PolynomialGeneralChart
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace Komorebi.PolynomialGeneralChartContract
8 open MvPolynomial
9 variable {e q : ℕ}
10 
11 /-- No chosen minor, unspecified equation, or assumed root function occurs in this contract. -/
12 theorem full_rectangular_chart (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
13     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
14     (hx : ∀ i, (p : ℤ)^L ∣ eval x (F i))
15     (hJ : Function.Surjective (fun u : Fin (e + q) → ZMod p => fun i =>
16       ∑ j, (eval x (pderiv j (F i)) : ZMod p) * u j)) :
17     ∃ σ : Equiv.Perm (Fin (e + q)),
18     ∃ h : {t : Fin q → ℤ_[p] //
19           ∀ j, (p : ℤ_[p])^L ∣ t j - (x (σ (Fin.natAdd e j)) : ℤ_[p])} ≃ₜ
20         {z : {a : Fin (e + q) → ℤ_[p] //
21           ∀ j, (p : ℤ_[p])^L ∣ a j - (x j : ℤ_[p])} //
22           (fun i => eval₂ (Int.castRingHom ℤ_[p]) z.val (F i)) = 0},
23       (∀ z j, (h.symm z).val j = z.val.val (σ (Fin.natAdd e j))) ∧
24       (∀ N t u,
25         (∀ j, (p : ℤ_[p])^N ∣ t.val j - u.val j) ↔
26         (∀ i, (p : ℤ_[p])^N ∣ (h t).val.val i - (h u).val.val i)) := by
27   obtain ⟨σ, h, hproj, hcong⟩ :=
28     PolynomialGeneralChart.exists_parameter_homeomorph p L hL F x hx hJ
29   refine ⟨σ, h, ?_, hcong⟩
30   intro z j
31   exact congrFun (hproj z) j
32 
33 end Komorebi.PolynomialGeneralChartContract

Back to source controls