PolynomialPrescribedStep.lean

1 module
2 public import PolynomialPrescribedCounts
3 public import PolynomialSurjectiveStep
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialPrescribedStep
10 open Komorebi.NativeAffine Komorebi.PolynomialObstruction
11 open Komorebi.PolynomialDigitBridge Komorebi.PolynomialPrescribedSystem
12 open Komorebi.PolynomialPrescribedLifts
13 open Komorebi.PolynomialParameterSystem (freePart join)
14 variable {m k e : ℕ}
15 
16 /-- Congruent integer points have the same actual solved-coordinate Jacobian. -/
17 theorem solvedJacobian_eq (q : ℕ) (F : Fin e → MvPolynomial (Fin (m + k)) ℤ)
18     (x y : Fin (m + k) → ℤ) (hxy : ∀ i, (q : ℤ) ∣ y i - x i) :
19     solvedJacobian q F y = solvedJacobian q F x := by
20   have h := PolynomialSurjectiveStep.digitJacobian_eq q F x y hxy
21   apply LinearMap.ext
22   intro u
23   have hu := congrArg (fun A : (Fin (m + k) → ZMod q) →ₗ[ZMod q] (Fin e → ZMod q) =>
24     A (join u 0)) h
25   simpa only [digitJacobian_join, map_zero, add_zero] using hu
26 
27 /-- A positive-depth correction preserves the actual solved block. -/
28 theorem solvedJacobian_shift_eq (q L : ℕ) (hL : 1 ≤ L)
29     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x s : Fin (m + k) → ℤ) :
30     solvedJacobian q F (x + (q : ℤ)^L • s) = solvedJacobian q F x := by
31   apply solvedJacobian_eq
32   intro i
33   change (q : ℤ) ∣ x i + (q : ℤ)^L * s i - x i
34   rw [add_sub_cancel_left]
35   exact dvd_mul_of_dvd_left (dvd_pow_self (q : ℤ) (by omega : L ≠ 0)) _
36 
37 /-- Solved-block surjectivity removes every prescribed one-step obstruction. -/
38 theorem obstruction_zero (q : ℕ)
39     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
40     (hJ : Function.Surjective (solvedJacobian q F x))
41     (r : Fin e → ℤ) (v : Fin k → ZMod q) :
42     PolynomialPrescribedSystem.obstruction q F x r v = 0 := by
43   apply (prescribed_digits_nonempty_iff q F x r v).mp
44   obtain ⟨u, hu⟩ := hJ (-(parameterResidual q F x r v))
45   exact ⟨⟨u, by change parameterResidual q F x r v + solvedJacobian q F x u = 0
46                 rw [hu, add_neg_cancel]⟩⟩
47 
48 /-- Every compatible integer parameter target is attained exactly by an actual
49 next root. Its integer correction retains the supplied parameter quotient,
50 rather than replacing that quotient by a canonical residue representative. -/
51 theorem one_step_lift (q L : ℕ) (hq : 0 < q) (hL : 1 ≤ L)
52     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
53     (hx : ∀ i, (q : ℤ)^L ∣ evalSystem F x i)
54     (hJ : Function.Surjective (solvedJacobian q F x))
55     (t : Fin k → ℤ) (ht : ∀ j, (q : ℤ)^L ∣ t j - freePart x j) :
56     ∃ y : Fin (m + k) → ℤ,
57       (∀ i, (q : ℤ)^L ∣ (y - x) i) ∧
58       (∀ i, (q : ℤ)^(L+1) ∣ evalSystem F y i) ∧
59       freePart y = t ∧ solvedJacobian q F y = solvedJacobian q F x := by
60   choose w hw using ht
61   obtain ⟨r, hr⟩ := residual_exists q L F x hx
62   obtain ⟨u, hu⟩ := hJ (-(parameterResidual q F x r (reduction q k w)))
63   have hcorr : reduction q e r + digitJacobian q F x (join u (reduction q k w)) = 0 := by
64     apply (prescribed_equation_iff q F x r (reduction q k w) u).mp
65     rw [hu, add_neg_cancel]
66   let s : Fin (m + k) → ℤ := join (integerLift q u) w
67   have hs : reduction q (m + k) s = join u (reduction q k w) := by
68     ext i
69     refine Fin.addCases (fun j => ?_) (fun j => ?_) i
70     · change ((join (integerLift q u) w (Fin.castAdd k j) : ℤ) : ZMod q) = _
71       simpa only [PolynomialParameterSystem.join_solved, reduction, LinearMap.coe_mk,
72         AddHom.coe_mk] using
73         congrFun (reduction_integerLift q hq u) j
74     · simp only [reduction, LinearMap.coe_mk, AddHom.coe_mk, s,
75         PolynomialParameterSystem.join_free]
76   refine ⟨x + (q : ℤ)^L • s,
77     (same_residue_iff ((q : ℤ)^L) x _).mpr ⟨s, rfl⟩, ?_, ?_,
78     solvedJacobian_shift_eq q L hL F x s⟩
79   · apply (next_level_iff_digit q L hq hL F x r hr s).mpr
80     rw [map_add, ← reduction_jacobian, hs]
81     exact hcorr
82   · ext j
83     change x (Fin.natAdd m j) + (q : ℤ)^L * s (Fin.natAdd m j) = t j
84     dsimp only [s]
85     rw [PolynomialParameterSystem.join_free]
86     have hj := hw j
87     change t j - x (Fin.natAdd m j) = (q : ℤ)^L * w j at hj
88     omega
89 
90 /-- Surjectivity of the solved block forces its rank to be the equation count. -/
91 theorem solved_rank (p : ℕ) [Fact (Nat.Prime p)]
92     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
93     (hJ : Function.Surjective (solvedJacobian p F x)) :
94     FiniteFiberCounts.rank p (solvedJacobian p F x) = e := by
95   unfold FiniteFiberCounts.rank
96   rw [LinearMap.range_eq_top.mpr hJ, finrank_top, Module.finrank_fin_fun]
97 
98 /-- The exponent m-e is nonnegative as a consequence of solved-block surjectivity. -/
99 theorem solved_dimension (p : ℕ) [Fact (Nat.Prime p)]
100     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
101     (hJ : Function.Surjective (solvedJacobian p F x)) : e ≤ m := by
102   simpa only [Module.finrank_fin_fun] using
103     LinearMap.finrank_le_finrank_of_surjective hJ
104 
105 /-- Every parameter digit has exactly p^(m-e) distinct actual next-level residue
106 lifts when the actual solved block is surjective. -/
107 theorem prescribed_lift_card (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
108     (F : Fin e → MvPolynomial (Fin (m + k)) ℤ) (x : Fin (m + k) → ℤ)
109     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
110     (hJ : Function.Surjective (solvedJacobian p F x)) (v : Fin k → ZMod p) :
111     Nat.card (PrescribedLifts p L F x v) = p ^ (m - e) := by
112   obtain ⟨r, hr⟩ := residual_exists p L F x hx
113   rw [PolynomialPrescribedCounts.lift_card p L hL F x r hr v,
114     ite_eq_left (obstruction_zero p F x hJ r v), solved_rank p F x hJ]
115 
116 end Komorebi.PolynomialPrescribedStep

Back to source controls