PolynomialPrescribedLifts.lean

1 module
2 public import PolynomialPrescribedSystem
3 public import PolynomialLiftCounts
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialPrescribedLifts
10 open Komorebi.NativeAffine Komorebi.PolynomialObstruction
11 open Komorebi.PolynomialDigitBridge Komorebi.PolynomialLiftCounts
12 open Komorebi.PolynomialParameterSystem Komorebi.ResidueLiftDigits
13 open Komorebi.PolynomialPrescribedSystem
14 variable {m k e : ℕ}
15 
16 /-- Actual polynomial residue lifts whose free coordinates have the prescribed
17 next-level residue classes. The condition fixes residue classes, not chosen
18 integer representatives of the parameter digits. -/
19 abbrev PrescribedLifts (q L : ℕ)
20     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
21     (v : Fin k → ZMod q) :=
22   {y : ActualLifts q L F x //
23     freePart y.val.val = digitResidue q L (freePart x) v}
24 
25 /-- Taking the free coordinates commutes with forming actual digit residues. -/
26 theorem freePart_digitResidue (q L : ℕ) (x : Fin (m + k) → ℤ)
27     (t : Fin (m + k) → ZMod q) :
28     freePart (digitResidue q L x t) = digitResidue q L (freePart x) (freePart t) := rfl
29 
30 /-- Solved correction digits are precisely full correction solutions with the
31 specified parameter digit. -/
32 def prescribedDigitEquivRestricted (q : ℕ)
33     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
34     (r : Fin e → ℤ) (v : Fin k → ZMod q) :
35     PrescribedDigits q F x r v ≃ {t : DigitSolutions q F x r // freePart t.val = v} where
36   toFun u := ⟨⟨join u.val v, (prescribed_equation_iff q F x r v u.val).mp u.property⟩,
37     freePart_join u.val v⟩
38   invFun t := ⟨solvedPart t.val.val, (prescribed_equation_iff q F x r v _).mpr (by
39     have hjoin : join (solvedPart t.val.val) v = t.val.val := by
40       calc
41         join (solvedPart t.val.val) v = join (solvedPart t.val.val) (freePart t.val.val) :=
42           congrArg (join (solvedPart t.val.val)) t.property.symm
43         _ = t.val.val := join_parts t.val.val
44     rw [hjoin]
45     exact t.val.property)⟩
46   left_inv u := by
47     apply Subtype.ext
48     exact solvedPart_join u.val v
49   right_inv t := by
50     apply Subtype.ext
51     apply Subtype.ext
52     change join (solvedPart t.val.val) v = t.val.val
53     calc
54       join (solvedPart t.val.val) v = join (solvedPart t.val.val) (freePart t.val.val) :=
55         congrArg (join (solvedPart t.val.val)) t.property.symm
56       _ = t.val.val := join_parts t.val.val
57 
58 /-- The unrestricted digit-to-lift equivalence retains exactly the parameter
59 constraint, including for composite moduli and the degenerate modulus one. -/
60 def restrictedDigitEquivLifts (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
61     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
62     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
63     (v : Fin k → ZMod q) :
64     {t : DigitSolutions q F x r // freePart t.val = v} ≃ PrescribedLifts q L F x v :=
65   Equiv.subtypeEquiv (digitEquivLifts q L hq hL F x r hr) (fun t => by
66     change freePart t.val = v ↔
67       freePart (digitResidue q L x t.val) = digitResidue q L (freePart x) v
68     rw [freePart_digitResidue]
69     constructor
70     · intro h
71       rw [h]
72     · intro h
73       exact digitResidue_injective q L hq (freePart x) h)
74 
75 /-- The prescribed solved-digit fiber parametrizes exactly the actual next-level
76 polynomial residues having the prescribed parameter digits. -/
77 def prescribedDigitEquivLifts (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
78     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
79     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
80     (v : Fin k → ZMod q) :
81     PrescribedDigits q F x r v ≃ PrescribedLifts q L F x v :=
82   (prescribedDigitEquivRestricted q F x r v).trans
83     (restrictedDigitEquivLifts q L hq hL F x r hr v)
84 
85 /-- The equivalence sends a solved digit to its actual shifted residue vector. -/
86 @[simp] theorem prescribedDigitEquivLifts_apply (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
87     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
88     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
89     (v : Fin k → ZMod q) (u : PrescribedDigits q F x r v) :
90     (prescribedDigitEquivLifts q L hq hL F x r hr v u).val.val.val =
91       digitResidue q L x (join u.val v) := rfl
92 
93 end Komorebi.PolynomialPrescribedLifts

Back to source controls