PolynomialPrescribedTowerUnique.lean

1 module
2 public import PolynomialParameterChart
3 public import PolynomialPrescribedSystem
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialPrescribedTowerUnique
10 
11 open Komorebi.PolynomialObstruction Komorebi.PolynomialPadicLift
12 open Komorebi.PolynomialParameterSystem Komorebi.PolynomialParameterChart
13 open Komorebi.PolynomialLocalSurjective
14 
15 variable {e k : ℕ}
16 
17 /-- In the square solved case the rectangular interface is the existing chart block. -/
18 theorem solvedJacobian_square (p : ℕ)
19     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ) (x : Fin (e + k) → ℤ) :
20     PolynomialPrescribedSystem.solvedJacobian p F x =
21       PolynomialParameterSystem.solvedJacobian p F x := rfl
22 
23 /-- Every exact root with the prescribed parameters is the checked chart point.
24 The solved block is square; its actual reduction at the initial integer point is surjective. -/
25 theorem prescribed_root_eq_chartPoint (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
26     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ) (x : Fin (e + k) → ℤ)
27     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
28     (hJ : Function.Surjective (PolynomialPrescribedSystem.solvedJacobian p F x))
29     (t : residueBall p L (freePart x)) (b : Fin (e + k) → ℤ_[p])
30     (hb : ∀ i, padicEval p F b i = 0)
31     (hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p]))
32     (ht : freePart b = t.val) :
33     b = (chartPoint p L hL F x hx (by simpa only [solvedJacobian_square] using hJ) t).val := by
34   exact congrArg Subtype.val (chartPoint_unique p L hL F x hx
35     (by simpa only [solvedJacobian_square] using hJ) t ⟨b, hbx⟩ (funext hb) ht)
36 
37 /-- Two roots in the initial ball with the same parameters coincide when the solved block is square. -/
38 theorem prescribed_root_unique (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
39     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ) (x : Fin (e + k) → ℤ)
40     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
41     (hJ : Function.Surjective (PolynomialPrescribedSystem.solvedJacobian p F x))
42     (b c : Fin (e + k) → ℤ_[p])
43     (hb : ∀ i, padicEval p F b i = 0) (hc : ∀ i, padicEval p F c i = 0)
44     (hbx : ∀ i, (p : ℤ_[p])^L ∣ b i - (x i : ℤ_[p]))
45     (hcx : ∀ i, (p : ℤ_[p])^L ∣ c i - (x i : ℤ_[p]))
46     (hparams : freePart b = freePart c) : b = c := by
47   let t : residueBall p L (freePart x) :=
48     ⟨freePart b, fun j => hbx (Fin.natAdd e j)⟩
49   exact (prescribed_root_eq_chartPoint p L hL F x hx hJ t b hb hbx rfl).trans
50     (prescribed_root_eq_chartPoint p L hL F x hx hJ t c hc hcx hparams.symm).symm
51 
52 /-- Tower and parameter-approximation choices do not affect the square-case endpoint.
53 Only the initial retained precision is needed to place both exact endpoints in the uniqueness ball. -/
54 theorem prescribed_tower_endpoints_unique (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
55     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ) (x : Fin (e + k) → ℤ)
56     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
57     (hJ : Function.Surjective (PolynomialPrescribedSystem.solvedJacobian p F x))
58     (z w : ℕ → Fin (e + k) → ℤ) (hz0 : z 0 = x) (hw0 : w 0 = x)
59     (b c : Fin (e + k) → ℤ_[p]) (τ : Fin k → ℤ_[p])
60     (hb : ∀ i, padicEval p F b i = 0) (hc : ∀ i, padicEval p F c i = 0)
61     (hbz : ∀ n i, (p : ℤ_[p])^(L+n) ∣ b i - (z n i : ℤ_[p]))
62     (hcw : ∀ n i, (p : ℤ_[p])^(L+n) ∣ c i - (w n i : ℤ_[p]))
63     (hbτ : freePart b = τ) (hcτ : freePart c = τ) : b = c := by
64   apply prescribed_root_unique p L hL F x hx hJ b c hb hc
65   · simpa only [Nat.add_zero, hz0] using hbz 0
66   · simpa only [Nat.add_zero, hw0] using hcw 0
67   · exact hbτ.trans hcτ.symm
68 
69 end Komorebi.PolynomialPrescribedTowerUnique

Back to source controls