ReleaseSmithSign.lean

1 import KomorebiVerification.PaperII.SmithDyadic
2 import KomorebiVerification.PaperII.ResultantSeparation
3 import Mathlib.NumberTheory.Padics.PadicIntegers
4 import Mathlib.LinearAlgebra.Matrix.ToLin
5 
6 /-! The displayed sign projectors on the actual p-adic standard lattice. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace Komorebi.PaperII.PadicSign
10 open scoped Matrix
11 open ResultantSeparation
12 variable (p : Nat) [Fact p.Prime]
13 
14 /-- Precisely the vectors with p-adic integer coordinates. -/
15 def standardLattice : Submodule (PadicInt p) (Fin 2 → Padic p) where
16   carrier := {x | ∀ i, x i ∈ PadicInt.subring p}
17   zero_mem' _i := (PadicInt.subring p).zero_mem
18   add_mem' hx hy i := (PadicInt.subring p).add_mem (hx i) (hy i)
19   smul_mem' c _x hx i := (PadicInt.subring p).mul_mem c.property (hx i)
20 
21 def positiveSign : Module.End (Padic p) (Fin 2 → Padic p) :=
22   Matrix.toLin' (SmithDyadic.positiveSignProjector.map (Rat.castHom (Padic p)))
23 
24 def negativeSign : Module.End (Padic p) (Fin 2 → Padic p) :=
25   Matrix.toLin' (SmithDyadic.negativeSignProjector.map (Rat.castHom (Padic p)))
26 
27 theorem positiveSign_apply (x : Fin 2 → Padic p) :
28     positiveSign p x = ![x 0 + (2 : Padic p)⁻¹ * x 1, 0] := by
29   ext i
30   fin_cases i <;> simp [positiveSign, Matrix.toLin'_apply, Matrix.mulVec,
31     dotProduct, Fin.sum_univ_two, SmithDyadic.positiveSignProjector]
32 
33 theorem negativeSign_apply (x : Fin 2 → Padic p) :
34     negativeSign p x = ![-((2 : Padic p)⁻¹ * x 1), x 1] := by
35   ext i
36   fin_cases i <;> simp [negativeSign, Matrix.toLin'_apply, Matrix.mulVec,
37     dotProduct, Fin.sum_univ_two, SmithDyadic.negativeSignProjector, div_eq_mul_inv, neg_mul]
38 
39 theorem positiveSign_twice (x : Fin 2 → Padic p) :
40     (2 : Padic p) • positiveSign p x = ![2 * x 0 + x 1, 0] := by
41   rw [positiveSign_apply]
42   ext i
43   fin_cases i <;> simp [mul_add]
44 
45 theorem negativeSign_twice (x : Fin 2 → Padic p) :
46     (2 : Padic p) • negativeSign p x = ![-x 1, 2 * x 1] := by
47   rw [negativeSign_apply]
48   ext i
49   fin_cases i <;> simp
50 
51 theorem twice_positive_preserves :
52     PreservesLattice ((2 : Padic p) • positiveSign p) (standardLattice p).toAddSubgroup := by
53   intro x hx
54   change ∀ i, (((2 : Padic p) • positiveSign p) x) i ∈ PadicInt.subring p
55   rw [LinearMap.smul_apply, positiveSign_twice]
56   intro i
57   fin_cases i
58   · exact (PadicInt.subring p).add_mem ((PadicInt.subring p).mul_mem
59       (by simp) (hx 0)) (hx 1)
60   · exact (PadicInt.subring p).zero_mem
61 
62 theorem twice_negative_preserves :
63     PreservesLattice ((2 : Padic p) • negativeSign p) (standardLattice p).toAddSubgroup := by
64   intro x hx
65   change ∀ i, (((2 : Padic p) • negativeSign p) x) i ∈ PadicInt.subring p
66   rw [LinearMap.smul_apply, negativeSign_twice]
67   intro i
68   fin_cases i
69   · exact (PadicInt.subring p).neg_mem (hx 1)
70   · exact (PadicInt.subring p).mul_mem (by simp) (hx 1)
71 
72 theorem half_integral_of_odd (hp : p ≠ 2) : (2 : Padic p)⁻¹ ∈ PadicInt.subring p := by
73   rw [PadicInt.mem_subring_iff, norm_inv]
74   have hc : p.Coprime 2 := (Fact.out : p.Prime).coprime_iff_not_dvd.mpr (by
75     intro h
76     rcases (Nat.dvd_prime Nat.prime_two).mp h with h | h
77     · exact (Fact.out : p.Prime).ne_one h
78     · exact hp h)
79   have hn : ‖(2 : Padic p)‖ = 1 := (Padic.norm_natCast_eq_one_iff (p := p)).mpr hc
80   rw [hn, inv_one]
81 
82 theorem positive_preserves_of_odd (hp : p ≠ 2) :
83     PreservesLattice (positiveSign p) (standardLattice p).toAddSubgroup := by
84   intro x hx
85   change ∀ i, positiveSign p x i ∈ PadicInt.subring p
86   rw [positiveSign_apply]
87   intro i
88   fin_cases i
89   · exact (PadicInt.subring p).add_mem (hx 0)
90       ((PadicInt.subring p).mul_mem (half_integral_of_odd p hp) (hx 1))
91   · exact (PadicInt.subring p).zero_mem
92 
93 theorem negative_preserves_of_odd (hp : p ≠ 2) :
94     PreservesLattice (negativeSign p) (standardLattice p).toAddSubgroup := by
95   intro x hx
96   change ∀ i, negativeSign p x i ∈ PadicInt.subring p
97   rw [negativeSign_apply]
98   intro i
99   fin_cases i
100   · exact (PadicInt.subring p).neg_mem
101       ((PadicInt.subring p).mul_mem (half_integral_of_odd p hp) (hx 1))
102   · exact hx 1
103 
104 
105 local instance : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
106 
107 theorem dyadic_half_norm : ‖(2 : Padic 2)⁻¹‖ = 2 := by
108   have hn : ‖(2 : Padic 2)‖ = (2 : ℝ)⁻¹ := Padic.norm_p
109   rw [norm_inv, hn]
110   norm_num
111 
112 theorem positive_dyadic_not_preserves :
113     ¬ PreservesLattice (positiveSign 2) (standardLattice 2).toAddSubgroup := by
114   intro h
115   have hx : (![0, 1] : Fin 2 → Padic 2) ∈ (standardLattice 2).toAddSubgroup := by
116     intro i
117     fin_cases i <;> simp
118   have hi := h ![0, 1] hx
119   have hn : ‖(2 : Padic 2)⁻¹‖ ≤ 1 := by
120     simpa [positiveSign_apply] using hi 0
121   rw [dyadic_half_norm] at hn
122   norm_num at hn
123 
124 theorem negative_dyadic_not_preserves :
125     ¬ PreservesLattice (negativeSign 2) (standardLattice 2).toAddSubgroup := by
126   intro h
127   have hx : (![0, 1] : Fin 2 → Padic 2) ∈ (standardLattice 2).toAddSubgroup := by
128     intro i
129     fin_cases i <;> simp
130   have hi := h ![0, 1] hx
131   have hn : ‖(2 : Padic 2)⁻¹‖ ≤ 1 := by
132     simpa [negativeSign_apply] using hi 0
133   rw [dyadic_half_norm] at hn
134   norm_num at hn
135 
136 theorem positive_dyadic_clears_one :
137     IsSeparationWeight (2 : Padic 2) (positiveSign 2) (standardLattice 2).toAddSubgroup 1 := by
138   simpa only [IsSeparationWeight, pow_one] using twice_positive_preserves 2
139 
140 theorem negative_dyadic_clears_one :
141     IsSeparationWeight (2 : Padic 2) (negativeSign 2) (standardLattice 2).toAddSubgroup 1 := by
142   simpa only [IsSeparationWeight, pow_one] using twice_negative_preserves 2
143 
144 theorem positive_dyadic_finite :
145     HasFiniteSeparationWeight (2 : Padic 2) (positiveSign 2) (standardLattice 2).toAddSubgroup :=
146   ⟨1, positive_dyadic_clears_one⟩
147 
148 theorem negative_dyadic_finite :
149     HasFiniteSeparationWeight (2 : Padic 2) (negativeSign 2) (standardLattice 2).toAddSubgroup :=
150   ⟨1, negative_dyadic_clears_one⟩
151 
152 /-- The least clearing exponent on the actual Z_2 standard lattice is exactly one. -/
153 theorem positive_dyadic_separationWeight : separationWeight positive_dyadic_finite = 1 := by
154   apply Nat.le_antisymm (separationWeight_le_of_clears _ positive_dyadic_clears_one)
155   apply Nat.one_le_iff_ne_zero.mpr
156   intro hz
157   have h := separationWeight_clears positive_dyadic_finite
158   rw [hz] at h
159   exact positive_dyadic_not_preserves (by simpa [IsSeparationWeight] using h)
160 
161 theorem negative_dyadic_separationWeight : separationWeight negative_dyadic_finite = 1 := by
162   apply Nat.le_antisymm (separationWeight_le_of_clears _ negative_dyadic_clears_one)
163   apply Nat.one_le_iff_ne_zero.mpr
164   intro hz
165   have h := separationWeight_clears negative_dyadic_finite
166   rw [hz] at h
167   exact negative_dyadic_not_preserves (by simpa [IsSeparationWeight] using h)
168 
169 end Komorebi.PaperII.PadicSign
170 #print axioms Komorebi.PaperII.PadicSign.positive_preserves_of_odd
171 #print axioms Komorebi.PaperII.PadicSign.twice_negative_preserves
172 
173 #print axioms Komorebi.PaperII.PadicSign.positive_dyadic_separationWeight
174 #print axioms Komorebi.PaperII.PadicSign.negative_dyadic_separationWeight

Back to source controls