PolynomialGeneralChart.lean

1 module
2 public import PolynomialParameterChart
3 public import PolynomialCoordinateReorder
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialGeneralChart
10 open Komorebi.PolynomialObstruction Komorebi.PolynomialDigitBridge
11 open Komorebi.PolynomialPadicLift Komorebi.PolynomialLocalSurjective
12 open Komorebi.PolynomialParameterSystem Komorebi.PolynomialParameterChart
13 open Komorebi.PolynomialCoordinateReorder
14 variable {d e q : ℕ}
15 
16 /-- Coordinate renaming identifies the entire original and reordered root loci. -/
17 def reorderRootHomeomorph (p L : ℕ) [Fact (Nat.Prime p)]
18     (σ : Equiv.Perm (Fin d)) (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
19     {a : residueBall p L x // padicEval p F a.val = 0} ≃ₜ
20       {a : residueBall p L (reorderPoint σ x) // padicEval p (reorderSystem σ F) a.val = 0} where
21   toFun a := ⟨⟨reorderPoint σ a.val.val, fun i => a.val.property (σ i)⟩, by
22     rw [padicEval_reorder_at]
23     exact a.property⟩
24   invFun a := ⟨⟨reorderPoint σ.symm a.val.val, by
25     intro i
26     simpa only [reorderPoint, Equiv.apply_symm_apply] using a.val.property (σ.symm i)⟩, by
27     rw [← padicEval_reorder]
28     exact a.property⟩
29   left_inv a := by
30     apply Subtype.ext
31     apply Subtype.ext
32     exact reorderPoint_inverse σ a.val.val
33   right_inv a := by
34     apply Subtype.ext
35     apply Subtype.ext
36     exact reorderPoint_inverse' σ a.val.val
37   continuous_toFun := by
38     apply Continuous.subtype_mk
39     apply Continuous.subtype_mk
40     exact (continuous_reorderPoint σ).comp
41       (continuous_subtype_val.comp continuous_subtype_val)
42   continuous_invFun := by
43     apply Continuous.subtype_mk
44     apply Continuous.subtype_mk
45     exact (continuous_reorderPoint σ.symm).comp
46       (continuous_subtype_val.comp continuous_subtype_val)
47 
48 /-- A full surjective rectangular Jacobian supplies its own solved coordinates.
49 The original root locus is homeomorphic to the remaining-coordinate ball,
50 with its actual coordinate projection as inverse and exact congruence reflection. -/
51 theorem exists_parameter_homeomorph (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
52     (F : Fin e → MvPolynomial (Fin (e + q)) ℤ) (x : Fin (e + q) → ℤ)
53     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
54     (hJ : Function.Surjective (digitJacobian p F x)) :
55     ∃ σ : Equiv.Perm (Fin (e + q)),
56     ∃ h : residueBall p L (freePart (reorderPoint σ x)) ≃ₜ
57         {z : residueBall p L x // padicEval p F z.val = 0},
58       (∀ z, (h.symm z).val = freePart (reorderPoint σ z.val.val)) ∧
59       (∀ N t u,
60         (∀ j, (p : ℤ_[p])^N ∣ t.val j - u.val j) ↔
61         (∀ i, (p : ℤ_[p])^N ∣ (h t).val.val i - (h u).val.val i)) := by
62   obtain ⟨σ, hσ⟩ := exists_reorder_solvedJacobian_surjective p F x hJ
63   have hxσ : ∀ i, (p : ℤ)^L ∣ evalSystem (reorderSystem σ F) (reorderPoint σ x) i := by
64     simpa only [evalSystem_reorder_at] using hx
65   let h₁ := parameterHomeomorph p L hL (reorderSystem σ F) (reorderPoint σ x) hxσ hσ
66   let h₂ := reorderRootHomeomorph p L σ F x
67   let h := h₁.trans h₂.symm
68   refine ⟨σ, h, ?_, ?_⟩
69   · intro z
70     rfl
71   · intro N t u
72     constructor
73     · intro htu i
74       exact chartPoint_congruent p L N hL (reorderSystem σ F) (reorderPoint σ x)
75         hxσ hσ t u htu (σ.symm i)
76     · intro htu j
77       have hh := htu (σ (Fin.natAdd e j))
78       change (p : ℤ_[p])^N ∣
79         (chartPoint p L hL (reorderSystem σ F) (reorderPoint σ x) hxσ hσ t).val
80           (σ.symm (σ (Fin.natAdd e j))) -
81         (chartPoint p L hL (reorderSystem σ F) (reorderPoint σ x) hxσ hσ u).val
82           (σ.symm (σ (Fin.natAdd e j))) at hh
83       simp only [Equiv.symm_apply_apply] at hh
84       have ht := congrFun (chartPoint_free p L hL (reorderSystem σ F)
85         (reorderPoint σ x) hxσ hσ t) j
86       have hu := congrFun (chartPoint_free p L hL (reorderSystem σ F)
87         (reorderPoint σ x) hxσ hσ u) j
88       change (chartPoint p L hL (reorderSystem σ F) (reorderPoint σ x) hxσ hσ t).val
89         (Fin.natAdd e j) = t.val j at ht
90       change (chartPoint p L hL (reorderSystem σ F) (reorderPoint σ x) hxσ hσ u).val
91         (Fin.natAdd e j) = u.val j at hu
92       rwa [ht, hu] at hh
93 
94 #print axioms reorderRootHomeomorph
95 #print axioms exists_parameter_homeomorph
96 
97 end Komorebi.PolynomialGeneralChart

Back to source controls