PolynomialPrescribedSystem.lean

1 module
2 
3 public import PolynomialParameterSystem
4 public import FiniteFiberCounts
5 
6 @[expose] public section
7 
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PolynomialPrescribedSystem
12 
13 open scoped BigOperators
14 open Komorebi.NativeAffine Komorebi.PolynomialDigitBridge
15 open Komorebi.FiniteFiberCounts
16 
17 variable {m k e : ℕ}
18 
19 /-- The actual Jacobian block for the coordinates that may be solved. -/
20 def solvedJacobian (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
21     (x : Fin (m + k) → ℤ) : (Fin m → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q) where
22   toFun u i := ∑ j,
23     (MvPolynomial.eval x (MvPolynomial.pderiv (Fin.castAdd k j) (F i)) : ZMod q) * u j
24   map_add' u v := by ext i; simp [mul_add, Finset.sum_add_distrib]
25   map_smul' a u := by
26     ext i
27     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
28     rw [Finset.mul_sum]
29     apply Finset.sum_congr rfl
30     intro j _
31     ring
32 
33 /-- The actual Jacobian block for the prescribed parameter coordinates. -/
34 def parameterJacobian (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
35     (x : Fin (m + k) → ℤ) : (Fin k → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q) where
36   toFun v i := ∑ j,
37     (MvPolynomial.eval x (MvPolynomial.pderiv (Fin.natAdd m j) (F i)) : ZMod q) * v j
38   map_add' u v := by ext i; simp [mul_add, Finset.sum_add_distrib]
39   map_smul' a u := by
40     ext i
41     simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
42     rw [Finset.mul_sum]
43     apply Finset.sum_congr rfl
44     intro j _
45     ring
46 
47 /-- The full Jacobian splits into the two actual coordinate blocks. -/
48 theorem digitJacobian_join (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
49     (x : Fin (m + k) → ℤ) (u : Fin m → ZMod q) (v : Fin k → ZMod q) :
50     digitJacobian q F x (PolynomialParameterSystem.join u v) =
51       solvedJacobian q F x u + parameterJacobian q F x v := by
52   ext i
53   simp [digitJacobian, solvedJacobian, parameterJacobian, Fin.sum_univ_add]
54 
55 /-- A prescribed parameter digit shifts the residual by its actual Jacobian image. -/
56 def parameterResidual (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
57     (x : Fin (m + k) → ℤ) (r : Fin e → ℤ) (v : Fin k → ZMod q) : Fin e → ZMod q :=
58   reduction q e r + parameterJacobian q F x v
59 
60 /-- The obstruction lies in the cokernel of the solved block alone. -/
61 abbrev PrescribedObstruction (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
62     (x : Fin (m + k) → ℤ) :=
63   (Fin e → ZMod q) ⧸ (solvedJacobian q F x).range
64 
65 /-- The actual residual class after imposing the parameter digit. -/
66 def obstruction (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
67     (x : Fin (m + k) → ℤ) (r : Fin e → ℤ) (v : Fin k → ZMod q) :
68     PrescribedObstruction q F x :=
69   Submodule.Quotient.mk (parameterResidual q F x r v)
70 
71 /-- The solved-coordinate digits compatible with the prescribed parameter digit. -/
72 abbrev PrescribedDigits (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
73     (x : Fin (m + k) → ℤ) (r : Fin e → ℤ) (v : Fin k → ZMod q) :=
74   Fiber (solvedJacobian q F x) (parameterResidual q F x r v)
75 
76 /-- The prescribed correction equation is exactly the full digit equation. -/
77 theorem prescribed_equation_iff (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
78     (x : Fin (m + k) → ℤ) (r : Fin e → ℤ) (v : Fin k → ZMod q) (u : Fin m → ZMod q) :
79     parameterResidual q F x r v + solvedJacobian q F x u = 0 ↔
80       reduction q e r + digitJacobian q F x (PolynomialParameterSystem.join u v) = 0 := by
81   rw [digitJacobian_join]
82   simp only [parameterResidual, add_assoc, add_comm (parameterJacobian q F x v)]
83 
84 /-- Vanishing of the solved-block obstruction is precisely digit existence. -/
85 theorem prescribed_digits_nonempty_iff (q : ℕ)
86     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
87     (x : Fin (m + k) → ℤ) (r : Fin e → ℤ) (v : Fin k → ZMod q) :
88     Nonempty (PrescribedDigits q F x r v) ↔ obstruction q F x r v = 0 := by
89   exact fiber_nonempty_iff_class_zero (solvedJacobian q F x) (parameterResidual q F x r v)
90 
91 /-- Positive moduli give a finite correction problem, including composite moduli. -/
92 theorem prescribed_digits_finite (q : ℕ) (hq : 0 < q)
93     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
94     (x : Fin (m + k) → ℤ) (r : Fin e → ℤ) (v : Fin k → ZMod q) :
95     Finite (PrescribedDigits q F x r v) := by
96   let : NeZero q := ⟨Nat.ne_of_gt hq⟩
97   unfold PrescribedDigits Fiber
98   infer_instance
99 
100 end Komorebi.PolynomialPrescribedSystem

Back to source controls