PolynomialSmoothCounts.lean

1 module
2 public import PolynomialIntegerTower
3 public import PolynomialLiftCounts
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialSmoothCounts
10 open Komorebi.NativeAffine Komorebi.PolynomialObstruction
11 open Komorebi.PolynomialDigitBridge Komorebi.PolynomialLiftCounts
12 open Komorebi.PolynomialIntegerTower
13 variable {d e : ℕ}
14 
15 /-- A surjective reduced Jacobian has rank equal to the number of equations. -/
16 theorem smooth_rank (p : ℕ) [Fact (Nat.Prime p)]
17     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
18     (hJ : Function.Surjective (digitJacobian p F x)) :
19     FiniteFiberCounts.rank p (digitJacobian p F x) = e := by
20   unfold FiniteFiberCounts.rank
21   rw [LinearMap.range_eq_top.mpr hJ, finrank_top, Module.finrank_fin_fun]
22 
23 /-- The dimension bound implicit in Jacobian surjectivity is an actual consequence. -/
24 theorem smooth_dimension (p : ℕ) [Fact (Nat.Prime p)]
25     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
26     (hJ : Function.Surjective (digitJacobian p F x)) : e ≤ d := by
27   simpa only [Module.finrank_fin_fun] using
28     LinearMap.finrank_le_finrank_of_surjective hJ
29 
30 /-- At every smooth lower root, there are exactly p^(d-e) distinct next-level
31 residue classes solving the original polynomial equations. -/
32 theorem smooth_lift_card (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
33     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
34     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
35     (hJ : Function.Surjective (digitJacobian p F x)) :
36     Nat.card (ActualLifts p L F x) = p^(d-e) := by
37   have hp : 0 < p := (Fact.out : Nat.Prime p).pos
38   obtain ⟨r, hr⟩ := Komorebi.PolynomialObstruction.residual_exists p L F x hx
39   obtain ⟨t, ht⟩ := hJ (-(reduction p e r))
40   have hnonempty : Nonempty (DigitSolutions p F x r) := by
41     refine ⟨⟨t, ?_⟩⟩
42     rw [ht, add_neg_cancel]
43   have ho := (digit_solutions_nonempty_iff p hp F x r).mp hnonempty
44   rw [lift_card p L hL F x r hr, ite_eq_left ho, smooth_rank p F x hJ]
45 
46 /-- At a smooth point the original finite obstruction group has one element. -/
47 theorem smooth_obstruction_card (p : ℕ) [Fact (Nat.Prime p)]
48     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
49     (hJ : Function.Surjective (digitJacobian p F x)) :
50     Nat.card (Obstruction p (jacobian F x)) = 1 := by
51   rw [obstruction_card p F x, smooth_rank p F x hJ, Nat.sub_self, pow_zero]
52 
53 /-- A compatible infinite tower through a smooth root has the same exact
54 number of possible next-level residue lifts at every stage. -/
55 theorem exists_regular_tower (p L : ℕ) [Fact (Nat.Prime p)] (hL : 1 ≤ L)
56     (F : Fin e → MvPolynomial (Fin d) ℤ) (x : Fin d → ℤ)
57     (hx : ∀ i, (p : ℤ)^L ∣ evalSystem F x i)
58     (hJ : Function.Surjective (digitJacobian p F x)) :
59     ∃ z : ℕ → Fin d → ℤ,
60       z 0 = x ∧
61       (∀ n i, (p : ℤ)^(L+n) ∣ evalSystem F (z n) i) ∧
62       (∀ n i, (p : ℤ)^(L+n) ∣ (z (n+1) - z n) i) ∧
63       (∀ n, Function.Surjective (digitJacobian p F (z n))) ∧
64       (∀ n, Nat.card (ActualLifts p (L+n) F (z n)) = p^(d-e)) := by
65   have hp : 0 < p := (Fact.out : Nat.Prime p).pos
66   obtain ⟨z, hz0, hroot, hstep, hsurj⟩ := exists_compatible_tower p L hp hL F x hx hJ
67   refine ⟨z, hz0, hroot, hstep, hsurj, ?_⟩
68   intro n
69   exact smooth_lift_card p (L+n) (by omega) F (z n) (hroot n) (hsurj n)
70 
71 end Komorebi.PolynomialSmoothCounts

Back to source controls