PolynomialRepresentative.lean

1 module
2 public import PolynomialObstruction
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialRepresentative
9 open Komorebi.NativeAffine Komorebi.PolynomialObstruction
10 variable {d e : ℕ}
11 
12 /-- The reduced actual Jacobian depends only on the point modulo q. -/
13 theorem digit_jacobian_eq (q : ℕ)
14     (F : Fin e → MvPolynomial (Fin d) ℤ) (x y : Fin d → ℤ)
15     (hxy : ∀ i, (q : ℤ) ∣ y i - x i) :
16     digitMap q (jacobian F y) = digitMap q (jacobian F x) := by
17   apply LinearMap.ext
18   intro t
19   have hz : reduction q e (jacobian F y t - jacobian F x t) = 0 := by
20     apply (reduction_zero_iff q _).mpr
21     intro i
22     change (q : ℤ) ∣ (∑ k, MvPolynomial.eval y (MvPolynomial.pderiv k (F i)) * t k) -
23       ∑ k, MvPolynomial.eval x (MvPolynomial.pderiv k (F i)) * t k
24     rw [← Finset.sum_sub_distrib]
25     apply Finset.dvd_sum
26     intro k _
27     rw [← sub_mul]
28     exact dvd_mul_of_dvd_left
29       (Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd (F i) x y q hxy k) _
30   change reduction q e (jacobian F y t) = reduction q e (jacobian F x t)
31   exact sub_eq_zero.mp (by simpa only [map_sub] using hz)
32 
33 /-- Changing an integer representative at positive depth preserves the reduced Jacobian. -/
34 theorem digit_jacobian_shift_eq (q L : ℕ) (hL : 1 ≤ L)
35     (F : Fin e → MvPolynomial (Fin d) ℤ) (x s : Fin d → ℤ) :
36     digitMap q (jacobian F (x + (q : ℤ)^L • s)) = digitMap q (jacobian F x) := by
37   apply digit_jacobian_eq
38   intro i
39   change (q : ℤ) ∣ x i + (q : ℤ)^L * s i - x i
40   rw [add_sub_cancel_left]
41   exact dvd_mul_of_dvd_left (dvd_pow_self (q : ℤ) (by omega : L ≠ 0)) _
42 
43 /-- Exact residuals of two representatives differ by the Jacobian correction modulo q. -/
44 theorem residual_digit_transport (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
45     (F : Fin e → MvPolynomial (Fin d) ℤ) (x s : Fin d → ℤ)
46     (r r' : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
47     (hr' : evalSystem F (x + (q : ℤ)^L • s) = (q : ℤ)^L • r') :
48     reduction q e r' = reduction q e (r + jacobian F x s) := by
49   have hqL : (q : ℤ)^L ≠ 0 := pow_ne_zero _ (Int.natCast_ne_zero.mpr (Nat.ne_of_gt hq))
50   have hz : reduction q e (r' - (r + jacobian F x s)) = 0 := by
51     apply (reduction_zero_iff q _).mpr
52     intro i
53     have ht := taylor_residual_dvd q L hL F x r hr s i
54     rw [hr'] at ht
55     change (q : ℤ)^(L+1) ∣ (q : ℤ)^L * r' i - (q : ℤ)^L * (r + jacobian F x s) i at ht
56     rw [← mul_sub, pow_succ, mul_dvd_mul_iff_left hqL] at ht
57     exact ht
58   exact sub_eq_zero.mp (by simpa only [map_sub] using hz)
59 
60 /-- In the common reduced-Jacobian quotient, the residual class is representative independent. -/
61 theorem residual_class_independent (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
62     (F : Fin e → MvPolynomial (Fin d) ℤ) (x s : Fin d → ℤ)
63     (r r' : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
64     (hr' : evalSystem F (x + (q : ℤ)^L • s) = (q : ℤ)^L • r') :
65     obstruction q (jacobian F x) r' = obstruction q (jacobian F x) r := by
66   unfold obstruction
67   rw [residual_digit_transport q L hq hL F x s r r' hr hr']
68   exact obstruction_representative_independent q (jacobian F x) r s
69 
70 /-- Representative independence stated with a single explicit reduced map,
71 whose cokernel simultaneously identifies the two obstruction modules. -/
72 theorem representative_independence (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
73     (F : Fin e → MvPolynomial (Fin d) ℤ) (x y : Fin d → ℤ)
74     (hxy : ∀ i, (q : ℤ)^L ∣ (y - x) i)
75     (r r' : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ)^L • r)
76     (hr' : evalSystem F y = (q : ℤ)^L • r') :
77     ∃ J : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ZMod q),
78       digitMap q (jacobian F x) = J ∧ digitMap q (jacobian F y) = J ∧
79       (Submodule.Quotient.mk (reduction q e r') : (Fin e → ZMod q) ⧸ LinearMap.range J) =
80       Submodule.Quotient.mk (reduction q e r) := by
81   obtain ⟨s, rfl⟩ := (same_residue_iff ((q : ℤ)^L) x y).mp hxy
82   exact ⟨digitMap q (jacobian F x), rfl, digit_jacobian_shift_eq q L hL F x s,
83     residual_class_independent q L hq hL F x s r r' hr hr'⟩
84 
85 end Komorebi.PolynomialRepresentative

Back to source controls