PolynomialLiftCounts.lean

1 module
2 public import PolynomialDigitBridge
3 public import ResidueLiftDigits
4 public import FiniteFiberCounts
5 public import IntegerFiniteCokernel
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 open scoped Classical
11 
12 namespace Komorebi.PolynomialLiftCounts
13 open Komorebi.NativeAffine Komorebi.PolynomialObstruction
14 open Komorebi.PolynomialDigitBridge Komorebi.ResidueLiftDigits
15 variable {d e : ℕ}
16 
17 /-- Actual next-level residue classes solving the original polynomial equations
18 and retaining the prescribed lower residue. Evaluation uses their canonical
19 integer representatives; polynomial congruence makes this representative independent. -/
20 abbrev ActualLifts (q L : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ)
21     (x : Fin d → ℤ) :=
22   {y : ResidueFiber q L x // ∀ i, (q : ℤ)^(L+1) ∣
23     evalSystem F (integerLift (q^(L+1)) y.val) i}
24 
25 /-- The residue class represented by a correction solves the actual equations
26 exactly when the finite Jacobian cancels the residual digit. -/
27 theorem digit_residue_solution_iff (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
28     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
29     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
30     (t : Fin d → ZMod q) :
31     (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F
32       (integerLift (q^(L+1)) (digitEquivResidue q L hq x t).val) i) ↔
33       reduction q e r + digitJacobian q F x t = 0 := by
34   rw [← digit_solution_iff q L hq hL F x r hr t]
35   apply forall_congr'
36   intro i
37   apply dvd_iff_of_dvd_sub
38   apply Komorebi.PolynomialTaylor.eval_dvd_of_dvd
39   intro k
40   exact next_modulus_dvd_val_sub_shift q L hq x t k
41 
42 /-- The correction-digit fiber is precisely the finite set of actual polynomial lifts. -/
43 def digitEquivLifts (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
44     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
45     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r) :
46     DigitSolutions q F x r ≃ ActualLifts q L F x :=
47   Equiv.subtypeEquiv (digitEquivResidue q L hq x)
48     (fun t => (digit_residue_solution_iff q L hq hL F x r hr t).symm)
49 
50 /-- The actual nonempty digit fiber carries its natural kernel torsor structure. -/
51 @[instance_reducible] def digitAddTorsor (q : ℕ) (hq : 0 < q)
52     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) (r : Fin e → ℤ)
53     (h : obstruction q (jacobian F x) r = 0) :
54     AddTorsor (digitJacobian q F x).ker (DigitSolutions q F x r) :=
55   FiniteFiberCounts.fiberAddTorsor (digitJacobian q F x) (reduction q e r)
56     ((digit_solutions_nonempty_iff q hq F x r).mpr h)
57 
58 /-- A chosen valid digit identifies all distinct next-level lifts with the kernel. -/
59 def liftEquivKernel (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
60     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
61     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
62     (u : DigitSolutions q F x r) :
63     ActualLifts q L F x ≃ (digitJacobian q F x).ker :=
64   (digitEquivLifts q L hq hL F x r hr).symm.trans
65     (FiniteFiberCounts.fiberEquivKernel (digitJacobian q F x) (reduction q e r) u)
66 
67 /-- The previously constructed obstruction is the actual residue-ring cokernel. -/
68 def obstructionEquiv (q : ℕ) (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
69     Obstruction q (jacobian F x) ≃ₗ[ℤ]
70       ((Fin e → ZMod q) ⧸ (digitJacobian q F x).range) :=
71   IntegerFiniteCokernel.cokernelEquiv q (jacobian F x) (digitJacobian q F x)
72     (reduction_jacobian q F x)
73 
74 @[simp] theorem obstructionEquiv_class (q : ℕ)
75     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) (r : Fin e → ℤ) :
76     obstructionEquiv q F x (obstruction q (jacobian F x) r) =
77       Submodule.Quotient.mk (reduction q e r) := rfl
78 
79 /-- Exact count of distinct polynomial lift classes; an obstruction gives zero. -/
80 theorem lift_card (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
81     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
82     (r : Fin e → ℤ) (hr : evalSystem F x = (p : ℤ)^L • r) :
83     Nat.card (ActualLifts p L F x) =
84       if obstruction p (jacobian F x) r = 0 then
85         p ^ (d - FiniteFiberCounts.rank p (digitJacobian p F x)) else 0 := by
86   have hp : 0 < p := (Fact.out : Nat.Prime p).pos
87   have hc := FiniteFiberCounts.fiber_card p (digitJacobian p F x) (reduction p e r)
88   change Nat.card (DigitSolutions p F x r) =
89     if Nonempty (DigitSolutions p F x r) then
90       p ^ (d - FiniteFiberCounts.rank p (digitJacobian p F x)) else 0 at hc
91   rw [digit_solutions_nonempty_iff p hp F x r] at hc
92   rw [← Nat.card_congr (digitEquivLifts p L hp hL F x r hr)]
93   exact hc
94 
95 /-- Exact cardinality of the original obstruction group, not just a surrogate. -/
96 theorem obstruction_card (p : ℕ) [Fact (Nat.Prime p)]
97     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ) :
98     Nat.card (Obstruction p (jacobian F x)) =
99       p ^ (e - FiniteFiberCounts.rank p (digitJacobian p F x)) := by
100   rw [Nat.card_congr (obstructionEquiv p F x).toEquiv]
101   exact FiniteFiberCounts.cokernel_card p (digitJacobian p F x)
102 
103 /-- Counts and residual are obtained from the actual lower polynomial solution. -/
104 theorem finite_polynomial_lift_count (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
105     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
106     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i) :
107     ∃ r : Fin e → ℤ,
108       evalSystem F x = (p : ℤ)^L • r ∧
109       Nat.card (ActualLifts p L F x) =
110         (if obstruction p (jacobian F x) r = 0 then
111           p ^ (d - FiniteFiberCounts.rank p (digitJacobian p F x)) else 0) ∧
112       Nat.card (Obstruction p (jacobian F x)) =
113         p ^ (e - FiniteFiberCounts.rank p (digitJacobian p F x)) := by
114   obtain ⟨r, hr⟩ := Komorebi.PolynomialObstruction.residual_exists p L F x hx
115   exact ⟨r, hr, lift_card p L hL F x r hr, obstruction_card p F x⟩
116 
117 end Komorebi.PolynomialLiftCounts

Back to source controls