PolynomialRepresentativeContract.lean

1 module
2 public import PolynomialRepresentative
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialRepresentativeContract
9 
10 /-- Both actual reduced Jacobians are identified with one map before comparing
11 the residual classes in its single quotient; no arbitrary presentation claim. -/
12 theorem explicit_representative_contract (d e q L : ℕ)
13     (hq : 0 < q) (hL : 1 ≤ L)
14     (F : Fin e → MvPolynomial (Fin d) ℤ) (x y : Fin d → ℤ)
15     (hxy : ∀ i, (q : ℤ)^L ∣ y i - x i)
16     (r r' : Fin e → ℤ)
17     (hr : (fun i => MvPolynomial.eval x (F i)) = (q : ℤ)^L • r)
18     (hr' : (fun i => MvPolynomial.eval y (F i)) = (q : ℤ)^L • r') :
19     ∃ J : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ZMod q),
20       NativeAffine.digitMap q (PolynomialObstruction.jacobian F x) = J ∧
21       NativeAffine.digitMap q (PolynomialObstruction.jacobian F y) = J ∧
22       (Submodule.Quotient.mk (fun i => (r' i : ZMod q)) :
23         (Fin e → ZMod q) ⧸ LinearMap.range J) =
24       Submodule.Quotient.mk (fun i => (r i : ZMod q)) :=
25   PolynomialRepresentative.representative_independence q L hq hL F x y hxy r r' hr hr'
26 
27 end Komorebi.PolynomialRepresentativeContract

Back to source controls