PolynomialPrescribedCounts.lean

1 module
2 public import PolynomialPrescribedLifts
3 public import FiniteFiberCounts
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 open scoped Classical
9 
10 namespace Komorebi.PolynomialPrescribedCounts
11 open Komorebi.PolynomialObstruction Komorebi.PolynomialPrescribedSystem
12 open Komorebi.PolynomialPrescribedLifts
13 variable {m k e : ℕ}
14 
15 /-- The solved-block kernel acts freely and transitively on compatible solved digits.
16 The action is ordinary translation and does not require a chosen valid digit. -/
17 @[instance_reducible] def digitAddTorsor (q : ℕ)
18     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
19     (r : Fin e → ℤ) (v : Fin k → ZMod q) (h : obstruction q F x r v = 0) :
20     AddTorsor (solvedJacobian q F x).ker (PrescribedDigits q F x r v) :=
21   FiniteFiberCounts.fiberAddTorsor (solvedJacobian q F x) (parameterResidual q F x r v)
22     ((prescribed_digits_nonempty_iff q F x r v).mpr h)
23 
24 /-- A chosen valid solved digit identifies all actual prescribed lifts with the kernel. -/
25 def liftEquivKernel (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
26     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
27     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
28     (v : Fin k → ZMod q) (u : PrescribedDigits q F x r v) :
29     PrescribedLifts q L F x v ≃ (solvedJacobian q F x).ker :=
30   (prescribedDigitEquivLifts q L hq hL F x r hr v).symm.trans
31     (FiniteFiberCounts.fiberEquivKernel (solvedJacobian q F x)
32       (parameterResidual q F x r v) u)
33 
34 /-- The actual residue lifts inherit the natural kernel action through their exact
35 digit equivalence. No base lift is chosen to define this torsor. -/
36 @[instance_reducible] def liftAddTorsor (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
37     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
38     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
39     (v : Fin k → ZMod q) (h : obstruction q F x r v = 0) :
40     AddTorsor (solvedJacobian q F x).ker (PrescribedLifts q L F x v) := by
41   let E := prescribedDigitEquivLifts q L hq hL F x r hr v
42   let J := solvedJacobian q F x
43   let b := parameterResidual q F x r v
44   exact {
45     vadd := fun w t => E (FiniteFiberCounts.translate J b w (E.symm t))
46     zero_vadd := by
47       intro t
48       change E (FiniteFiberCounts.translate J b 0 (E.symm t)) = t
49       rw [FiniteFiberCounts.translate_zero, E.apply_symm_apply]
50     add_vadd := by
51       intro w z t
52       change E (FiniteFiberCounts.translate J b (w + z) (E.symm t)) =
53         E (FiniteFiberCounts.translate J b w
54           (E.symm (E (FiniteFiberCounts.translate J b z (E.symm t)))))
55       rw [E.symm_apply_apply, FiniteFiberCounts.translate_add]
56     vsub := fun t u => FiniteFiberCounts.difference J b (E.symm t) (E.symm u)
57     nonempty := by
58       obtain ⟨u⟩ := (prescribed_digits_nonempty_iff q F x r v).mpr h
59       exact ⟨E u⟩
60     vsub_vadd' := by
61       intro t u
62       change E (FiniteFiberCounts.translate J b
63         (FiniteFiberCounts.difference J b (E.symm t) (E.symm u)) (E.symm u)) = t
64       rw [FiniteFiberCounts.translate_difference, E.apply_symm_apply]
65     vadd_vsub' := by
66       intro w t
67       change FiniteFiberCounts.difference J b
68         (E.symm (E (FiniteFiberCounts.translate J b w (E.symm t)))) (E.symm t) = w
69       rw [E.symm_apply_apply, FiniteFiberCounts.difference_translate] }
70 
71 /-- A nonempty prescribed lift set has exactly the solved-kernel cardinality,
72 without requiring the modulus to be prime. -/
73 theorem lift_card_eq_kernel (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
74     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
75     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
76     (v : Fin k → ZMod q) (h : obstruction q F x r v = 0) :
77     Nat.card (PrescribedLifts q L F x v) = Nat.card (solvedJacobian q F x).ker := by
78   obtain ⟨u⟩ := (prescribed_digits_nonempty_iff q F x r v).mpr h
79   exact Nat.card_congr (liftEquivKernel q L hq hL F x r hr v u)
80 
81 /-- The cardinality of the prescribed solved digits obeys rank-nullity over a prime field. -/
82 theorem digit_card (p : ℕ) [Fact (Nat.Prime p)]
83     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
84     (r : Fin e → ℤ) (v : Fin k → ZMod p) :
85     Nat.card (PrescribedDigits p F x r v) =
86       if obstruction p F x r v = 0 then
87         p ^ (m - FiniteFiberCounts.rank p (solvedJacobian p F x)) else 0 := by
88   have hc := FiniteFiberCounts.fiber_card p (solvedJacobian p F x)
89     (parameterResidual p F x r v)
90   change Nat.card (PrescribedDigits p F x r v) =
91     if Nonempty (PrescribedDigits p F x r v) then
92       p ^ (m - FiniteFiberCounts.rank p (solvedJacobian p F x)) else 0 at hc
93   rw [prescribed_digits_nonempty_iff p F x r v] at hc
94   exact hc
95 
96 /-- Exact count of distinct actual next-level roots with the specified parameter digit. -/
97 theorem lift_card (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
98     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
99     (r : Fin e → ℤ) (hr : evalSystem F x = (p : ℤ)^L • r)
100     (v : Fin k → ZMod p) :
101     Nat.card (PrescribedLifts p L F x v) =
102       if obstruction p F x r v = 0 then
103         p ^ (m - FiniteFiberCounts.rank p (solvedJacobian p F x)) else 0 := by
104   have hp : 0 < p := (Fact.out : Nat.Prime p).pos
105   rw [← Nat.card_congr (prescribedDigitEquivLifts p L hp hL F x r hr v)]
106   exact digit_card p F x r v
107 
108 /-- Dimension of the obstruction space for the solved block. -/
109 theorem obstruction_finrank (p : ℕ) [Fact (Nat.Prime p)]
110     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ) :
111     Module.finrank (ZMod p) (PrescribedObstruction p F x) =
112       e - FiniteFiberCounts.rank p (solvedJacobian p F x) :=
113   FiniteFiberCounts.cokernel_finrank p (solvedJacobian p F x)
114 
115 /-- Exact cardinality of the prescribed-parameter obstruction space. -/
116 theorem obstruction_card (p : ℕ) [Fact (Nat.Prime p)]
117     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ) :
118     Nat.card (PrescribedObstruction p F x) =
119       p ^ (e - FiniteFiberCounts.rank p (solvedJacobian p F x)) :=
120   FiniteFiberCounts.cokernel_card p (solvedJacobian p F x)
121 
122 end Komorebi.PolynomialPrescribedCounts

Back to source controls