PolynomialPrescribedLifts_attempt01.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     rw [← t.property, join_parts]
40     exact t.val.property)⟩
41   left_inv u := by
42     apply Subtype.ext
43     exact solvedPart_join u.val v
44   right_inv t := by
45     apply Subtype.ext
46     apply Subtype.ext
47     change join (solvedPart t.val.val) v = t.val.val
48     rw [← t.property, join_parts]
49 
50 /-- The unrestricted digit-to-lift equivalence retains exactly the parameter
51 constraint, including for composite moduli and the degenerate modulus one. -/
52 def restrictedDigitEquivLifts (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
53     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
54     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
55     (v : Fin k → ZMod q) :
56     {t : DigitSolutions q F x r // freePart t.val = v} ≃ PrescribedLifts q L F x v :=
57   Equiv.subtypeEquiv (digitEquivLifts q L hq hL F x r hr) (fun t => by
58     change freePart t.val = v ↔
59       freePart (digitResidue q L x t.val) = digitResidue q L (freePart x) v
60     rw [freePart_digitResidue]
61     constructor
62     · intro h
63       rw [h]
64     · intro h
65       exact digitResidue_injective q L hq (freePart x) h)
66 
67 /-- The prescribed solved-digit fiber parametrizes exactly the actual next-level
68 polynomial residues having the prescribed parameter digits. -/
69 def prescribedDigitEquivLifts (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
70     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
71     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
72     (v : Fin k → ZMod q) :
73     PrescribedDigits q F x r v ≃ PrescribedLifts q L F x v :=
74   (prescribedDigitEquivRestricted q F x r v).trans
75     (restrictedDigitEquivLifts q L hq hL F x r hr v)
76 
77 /-- The equivalence sends a solved digit to its actual shifted residue vector. -/
78 @[simp] theorem prescribedDigitEquivLifts_apply (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
79     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
80     (r : Fin e → ℤ) (hr : evalSystem F x = (q : ℤ) ^ L • r)
81     (v : Fin k → ZMod q) (u : PrescribedDigits q F x r v) :
82     (prescribedDigitEquivLifts q L hq hL F x r hr v u).val.val.val =
83       digitResidue q L x (join u.val v) := rfl
84 
85 end Komorebi.PolynomialPrescribedLifts

Back to source controls