PolynomialShared.lean

1 module
2 public import PolynomialObstruction
3 public import AffineSharedCorrection
4 
5 /-!
6 # A finite common quotient for simultaneous polynomial lifts
7 
8 The two blocks use the same unknown vector. Their actual reduced Jacobians
9 define a finite common quotient, and equal labels are precisely the remaining
10 condition for a joint next-level lift after each block lifts individually.
11 -/
12 
13 @[expose] public section
14 noncomputable section
15 set_option autoImplicit false
16 
17 namespace Komorebi.PolynomialShared
18 
19 open Komorebi.NativeAffine Komorebi.PolynomialObstruction Komorebi.SharedCorrection
20 
21 variable {d e f : ℕ}
22 
23 /-- The common quotient of the two actual reduced Jacobians. -/
24 abbrev SharedObstruction (q : ℕ)
25     (F : Fin e → MvPolynomial (Fin d) ℤ)
26     (G : Fin f → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :=
27   Komorebi.AffinePair.SharedObstruction q (jacobian F x) (jacobian G x)
28 
29 /-- A single vector must lift both polynomial systems. -/
30 def HasJointLift (q L : ℕ)
31     (F : Fin e → MvPolynomial (Fin d) ℤ)
32     (G : Fin f → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) : Prop :=
33   ∃ y : Fin d → ℤ,
34     (∀ i, (q : ℤ)^L ∣ (y - x) i) ∧
35     (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F y i) ∧
36     (∀ i, (q : ℤ)^(L+1) ∣ evalSystem G y i)
37 
38 theorem shared_obstruction_finite (q : ℕ) (hq : 0 < q)
39     (F : Fin e → MvPolynomial (Fin d) ℤ)
40     (G : Fin f → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
41     Finite (SharedObstruction q F G x) :=
42   Komorebi.AffinePair.shared_obstruction_finite q hq (jacobian F x) (jacobian G x)
43 
44 /-- Polynomial Taylor expansion identifies the actual simultaneous-lift
45 problem with two correction equations at the same digit. -/
46 theorem joint_lift_iff_digit_correction (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
47     (F : Fin e → MvPolynomial (Fin d) ℤ)
48     (G : Fin f → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
49     (r : Fin e → ℤ) (s : Fin f → ℤ)
50     (hr : evalSystem F x = (q : ℤ)^L • r)
51     (hs : evalSystem G x = (q : ℤ)^L • s) :
52     HasJointLift q L F G x ↔
53       ∃ t : Fin d → ℤ, reduction q e (r + jacobian F x t) = 0 ∧
54         reduction q f (s + jacobian G x t) = 0 := by
55   constructor
56   · rintro ⟨y, hy, hF, hG⟩
57     obtain ⟨t, rfl⟩ := (same_residue_iff ((q : ℤ)^L) x y).mp hy
58     exact ⟨t, (next_level_iff_digit q L hq hL F x r hr t).mp hF,
59       (next_level_iff_digit q L hq hL G x s hs t).mp hG⟩
60   · rintro ⟨t, hF, hG⟩
61     exact ⟨x + (q : ℤ)^L • t,
62       (same_residue_iff ((q : ℤ)^L) x _).mpr ⟨t, rfl⟩,
63       (next_level_iff_digit q L hq hL F x r hr t).mpr hF,
64       (next_level_iff_digit q L hq hL G x s hs t).mpr hG⟩
65 
66 /-- The left label is independent of the chosen actual polynomial lift. -/
67 theorem left_class_independent (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
68     (F : Fin e → MvPolynomial (Fin d) ℤ)
69     (G : Fin f → MvPolynomial (Fin d) ℤ) (x u u' : Fin d → ℤ)
70     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
71     (hu : ∀ i, (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • u) i)
72     (hu' : ∀ i, (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • u') i) :
73     (Submodule.Quotient.mk u : SharedObstruction q F G x) =
74       Submodule.Quotient.mk u' :=
75   Komorebi.AffinePair.left_class_independent q (jacobian F x) (jacobian G x) r u u'
76     ((next_level_iff_digit q L hq hL F x r hr u).mp hu)
77     ((next_level_iff_digit q L hq hL F x r hr u').mp hu')
78 
79 /-- The right label is independent of the chosen actual polynomial lift. -/
80 theorem right_class_independent (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
81     (F : Fin e → MvPolynomial (Fin d) ℤ)
82     (G : Fin f → MvPolynomial (Fin d) ℤ) (x v v' : Fin d → ℤ)
83     (s : Fin f → ℤ) (hs : evalSystem G x = (q : ℤ)^L • s)
84     (hv : ∀ i, (q : ℤ)^(L+1) ∣ evalSystem G (x + (q : ℤ)^L • v) i)
85     (hv' : ∀ i, (q : ℤ)^(L+1) ∣ evalSystem G (x + (q : ℤ)^L • v') i) :
86     (Submodule.Quotient.mk v : SharedObstruction q F G x) =
87       Submodule.Quotient.mk v' :=
88   Komorebi.AffinePair.right_class_independent q (jacobian F x) (jacobian G x) s v v'
89     ((next_level_iff_digit q L hq hL G x s hs v).mp hv)
90     ((next_level_iff_digit q L hq hL G x s hs v').mp hv')
91 
92 /-- Given actual individual polynomial lifts, equal common-quotient labels
93 are necessary and sufficient for a simultaneous polynomial lift. -/
94 theorem joint_lift_iff_class_eq (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
95     (F : Fin e → MvPolynomial (Fin d) ℤ)
96     (G : Fin f → MvPolynomial (Fin d) ℤ) (x u v : Fin d → ℤ)
97     (r : Fin e → ℤ) (s : Fin f → ℤ)
98     (hr : evalSystem F x = (q : ℤ)^L • r)
99     (hs : evalSystem G x = (q : ℤ)^L • s)
100     (hu : ∀ i, (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • u) i)
101     (hv : ∀ i, (q : ℤ)^(L+1) ∣ evalSystem G (x + (q : ℤ)^L • v) i) :
102     HasJointLift q L F G x ↔
103       (Submodule.Quotient.mk u : SharedObstruction q F G x) =
104         Submodule.Quotient.mk v := by
105   have hu' := (next_level_iff_digit q L hq hL F x r hr u).mp hu
106   have hv' := (next_level_iff_digit q L hq hL G x s hs v).mp hv
107   rw [joint_lift_iff_digit_correction q L hq hL F G x r s hr hs,
108     quotient_mk_eq_iff_common]
109   exact exists_congr fun t => and_congr
110     (Komorebi.AffinePair.digit_correction_iff_same_image q (jacobian F x) r u t hu')
111     (Komorebi.AffinePair.digit_correction_iff_same_image q (jacobian G x) s v t hv')
112 
113 /-- Individual polynomial solvability is included in the unconditioned
114 criterion, together with exactly the common compatibility relation. -/
115 theorem joint_lift_iff_compatible_corrections (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
116     (F : Fin e → MvPolynomial (Fin d) ℤ)
117     (G : Fin f → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
118     (r : Fin e → ℤ) (s : Fin f → ℤ)
119     (hr : evalSystem F x = (q : ℤ)^L • r)
120     (hs : evalSystem G x = (q : ℤ)^L • s) :
121     HasJointLift q L F G x ↔ ∃ u v : Fin d → ℤ,
122       (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • u) i) ∧
123       (∀ i, (q : ℤ)^(L+1) ∣ evalSystem G (x + (q : ℤ)^L • v) i) ∧
124       (Submodule.Quotient.mk u : SharedObstruction q F G x) =
125         Submodule.Quotient.mk v := by
126   constructor
127   · rintro ⟨y, hy, hF, hG⟩
128     obtain ⟨t, rfl⟩ := (same_residue_iff ((q : ℤ)^L) x y).mp hy
129     exact ⟨t, t, hF, hG, rfl⟩
130   · rintro ⟨u, v, hu, hv, huv⟩
131     exact (joint_lift_iff_class_eq q L hq hL F G x u v r s hr hs hu hv).mpr huv
132 
133 /-- Every pair of actual lower-level polynomial solutions has a finite common
134 quotient and an exact criterion for the next simultaneous lift. -/
135 theorem finite_polynomial_pair_compatibility (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
136     (F : Fin e → MvPolynomial (Fin d) ℤ)
137     (G : Fin f → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
138     (hxF : ∀ i, (q : ℤ)^L ∣ evalSystem F x i)
139     (hxG : ∀ i, (q : ℤ)^L ∣ evalSystem G x i) :
140     Finite (SharedObstruction q F G x) ∧
141       (HasJointLift q L F G x ↔ ∃ u v : Fin d → ℤ,
142         (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F (x + (q : ℤ)^L • u) i) ∧
143         (∀ i, (q : ℤ)^(L+1) ∣ evalSystem G (x + (q : ℤ)^L • v) i) ∧
144         (Submodule.Quotient.mk u : SharedObstruction q F G x) =
145           Submodule.Quotient.mk v) := by
146   obtain ⟨r, hr⟩ := Komorebi.PolynomialObstruction.residual_exists q L F x hxF
147   obtain ⟨s, hs⟩ := Komorebi.PolynomialObstruction.residual_exists q L G x hxG
148   exact ⟨shared_obstruction_finite q hq F G x,
149     joint_lift_iff_compatible_corrections q L hq hL F G x r s hr hs⟩
150 
151 #print axioms SharedObstruction
152 #print axioms HasJointLift
153 #print axioms shared_obstruction_finite
154 #print axioms joint_lift_iff_digit_correction
155 #print axioms left_class_independent
156 #print axioms right_class_independent
157 #print axioms joint_lift_iff_class_eq
158 #print axioms joint_lift_iff_compatible_corrections
159 #print axioms finite_polynomial_pair_compatibility
160 
161 end Komorebi.PolynomialShared

Back to source controls