Digits.lean

1 import PaperX.IntegralCharts
2 import PaperX.Singular
3 
4 /-! Digit expansions with a declared uniformizer and a chosen section of the
5 residue map. The section is not assumed to be a ring homomorphism. -/
6 set_option autoImplicit false
7 namespace PaperX.Digits
8 open IsLocalRing
9 open scoped BigOperators
10 variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
11 variable {π : R} (hπ : Irreducible π)
12 variable (s : ResidueField R → R) (hs : Function.RightInverse s (residue R))
13 
14 /-- An arbitrary residue section can always be chosen to send zero to zero. -/
15 theorem exists_normalized_section : ∃ s : ResidueField R → R,
16     Function.RightInverse s (residue R) ∧ s 0 = 0 := by
17   classical
18   let s : ResidueField R → R := fun a => if a = 0 then 0 else
19     Classical.choose (residue_surjective a)
20   refine ⟨s, ?_, by simp [s]⟩
21   intro a
22   by_cases ha : a = 0
23   · simp [s, ha]
24   · simpa [s, ha] using Classical.choose_spec (residue_surjective a)
25 
26 /-- The finite partial sum in the chosen digits. -/
27 noncomputable def partialSum (a : ℕ → ResidueField R) (n : ℕ) : R :=
28   ∑ j ∈ Finset.range n, π^j * s (a j)
29 
30 @[simp] theorem prefix_zero (a : ℕ → ResidueField R) : partialSum (π := π) s a 0 = 0 := by
31   simp [partialSum]
32 
33 theorem prefix_succ (a : ℕ → ResidueField R) (n : ℕ) :
34     partialSum (π := π) s a (n+1) = partialSum (π := π) s a n + π^n*s (a n) := by
35   exact Finset.sum_range_succ _ _
36 
37 theorem prefix_congr (a b : ℕ → ResidueField R) (n : ℕ)
38     (h : ∀ j < n, a j = b j) : partialSum (π := π) s a n = partialSum (π := π) s b n := by
39   apply Finset.sum_congr rfl
40   intro j hj
41   rw [h j (Finset.mem_range.mp hj)]
42 
43 /-- Each finite partial sum must agree with x through its stated precision. -/
44 def Encodes (a : ℕ → ResidueField R) (x : R) : Prop :=
45   ∀ n, π^n ∣ x - partialSum (π := π) s a n
46 
47 include hπ hs in
48 /-- Removing the selected first digit leaves an exactly divisible remainder. -/
49 theorem remainder_divisible (x : R) : π ∣ x - s (residue R x) := by
50   rw [← Ideal.mem_span_singleton, ← hπ.maximalIdeal_eq, ← residue_eq_zero_iff]
51   simp [hs (residue R x)]
52 
53 noncomputable def tail (x : R) : R := Classical.choose (remainder_divisible hπ s hs x)
54 
55 theorem tail_spec (x : R) : x = s (residue R x) + π * tail hπ s hs x := by
56   have h := Classical.choose_spec (remainder_divisible hπ s hs x)
57   change x - s (residue R x) = π * tail hπ s hs x at h
58   linear_combination h
59 
60 noncomputable def rest (x : R) : ℕ → R
61   | 0 => x
62   | n+1 => tail hπ s hs (rest x n)
63 
64 noncomputable def digits (x : R) (n : ℕ) : ResidueField R := residue R (rest hπ s hs x n)
65 
66 /-- Finite exact identity; no completeness assumption is needed to extract digits. -/
67 theorem remainder_identity (x : R) (n : ℕ) :
68     x = partialSum (π := π) s (digits hπ s hs x) n + π^n * rest hπ s hs x n := by
69   induction n with
70   | zero => simp [rest]
71   | succ n ih =>
72     rw [prefix_succ, pow_succ]
73     change x = partialSum s (digits hπ s hs x) n + π^n*s (residue R (rest hπ s hs x n)) +
74       (π^n*π) * tail hπ s hs (rest hπ s hs x n)
75     have h := tail_spec hπ s hs (rest hπ s hs x n)
76     linear_combination ih + π^n * h
77 
78 theorem digits_encode (x : R) : Encodes (π := π) s (digits hπ s hs x) x := by
79   intro n
80   refine ⟨rest hπ s hs x n, ?_⟩
81   have h := remainder_identity hπ s hs x n
82   linear_combination h
83 
84 include hπ hs in
85 /-- Two streams representing the same element agree at every digit. -/
86 theorem encoding_unique (a b : ℕ → ResidueField R) (x : R)
87     (ha : Encodes (π := π) s a x) (hb : Encodes (π := π) s b x) : a = b := by
88   funext n
89   induction n using Nat.strong_induction_on with
90   | h n ih =>
91     have hpref := prefix_congr (π := π) s a b n ih
92     have hdiff : π^(n+1) ∣ π^n * (s (a n) - s (b n)) := by
93       have h := dvd_sub (hb (n+1)) (ha (n+1))
94       convert h using 1
95       rw [prefix_succ, prefix_succ, hpref]
96       ring
97     rw [pow_succ] at hdiff
98     have hd := (mul_dvd_mul_iff_left (pow_ne_zero n hπ.ne_zero)).mp hdiff
99     have hr : residue R (s (a n) - s (b n)) = 0 := by
100       apply (residue_eq_zero_iff _).mpr
101       rw [hπ.maximalIdeal_eq, Ideal.mem_span_singleton]
102       exact hd
103     simpa only [map_sub, hs _, sub_eq_zero] using hr
104 
105 /-- Differences between successive partial sums have increasing precision. -/
106 theorem prefix_compatible (a : ℕ → ResidueField R) {m n : ℕ} (h : m ≤ n) :
107     π^m ∣ partialSum (π := π) s a n - partialSum (π := π) s a m := by
108   induction n, h using Nat.le_induction with
109   | base => simp
110   | succ n h ih =>
111     rw [prefix_succ]
112     have hd : π^m ∣ π^n * s (a n) := dvd_mul_of_dvd_left (pow_dvd_pow π h) _
113     convert dvd_add ih hd using 1
114     ring
115 
116 variable [IsAdicComplete (maximalIdeal R) R]
117 
118 include hπ in
119 /-- Every digit stream converges to a unique coefficient-ring element. -/
120 theorem stream_reconstructs (a : ℕ → ResidueField R) : ∃! x, Encodes (π := π) s a x := by
121   have hc : ∀ {m n : ℕ}, m ≤ n →
122       partialSum (π := π) s a m ≡ partialSum (π := π) s a n [SMOD maximalIdeal R ^ m • (⊤ : Submodule R R)] := by
123     intro m n h
124     rw [SModEq.sub_mem, Ideal.smul_eq_mul, Ideal.mul_top,
125       hπ.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton]
126     simpa only [neg_sub, dvd_neg] using dvd_neg.mpr (prefix_compatible s a h)
127   obtain ⟨x, hx⟩ := IsPrecomplete.prec (inferInstance : IsPrecomplete (maximalIdeal R) R) hc
128   have hex : Encodes (π := π) s a x := by
129     intro n
130     have h := hx n
131     rw [SModEq.sub_mem, Ideal.smul_eq_mul, Ideal.mul_top,
132       hπ.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at h
133     simpa only [neg_sub, dvd_neg] using dvd_neg.mpr h
134   refine ⟨x, hex, ?_⟩
135   intro y hy
136   apply (IsHausdorff.eq_iff_smodEq (I := maximalIdeal R)).mpr
137   intro n
138   rw [SModEq.sub_mem, Ideal.smul_eq_mul, Ideal.mul_top,
139     hπ.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton]
140   convert dvd_sub (hy n) (hex n) using 1
141   ring
142 
143 /-- Explicit coordinate change between the complete DVR and residue-digit streams. -/
144 noncomputable def digitEquiv : R ≃ (ℕ → ResidueField R) where
145   toFun := digits hπ s hs
146   invFun a := Classical.choose (stream_reconstructs hπ s a)
147   left_inv x := by
148     have h := Classical.choose_spec (stream_reconstructs hπ s (digits hπ s hs x))
149     exact (h.2 x (digits_encode hπ s hs x)).symm
150   right_inv a := by
151     apply encoding_unique hπ s hs _ a
152     · exact digits_encode hπ s hs _
153     · exact (Classical.choose_spec (stream_reconstructs hπ s a)).1
154 
155 omit [IsAdicComplete (maximalIdeal R) R] in
156 /-- Positive-depth values are precisely streams whose constant digit is zero. -/
157 theorem positive_depth_iff (x : R) :
158     x ∈ maximalIdeal R ↔ digits hπ s hs x 0 = 0 := by
159   exact (residue_eq_zero_iff x).symm
160 
161 
162 omit [IsAdicComplete (maximalIdeal R) R] in
163 include hπ in
164 /-- Membership in the maximal ideal supplies one uniformizer factor. -/
165 theorem maximal_divisible (x : R) (hx : x ∈ maximalIdeal R) : π ∣ x := by
166   rw [hπ.maximalIdeal_eq, Ideal.mem_span_singleton] at hx
167   exact hx
168 
169 /-- Dividing a positive-depth value by the declared uniformizer is a bijection. -/
170 noncomputable def uniformizerEquiv : maximalIdeal R ≃ R where
171   toFun x := Classical.choose (maximal_divisible hπ x.val x.property)
172   invFun y := ⟨π*y, by rw [hπ.maximalIdeal_eq, Ideal.mem_span_singleton]; exact dvd_mul_right π y⟩
173   left_inv x := by
174     apply Subtype.ext
175     exact (Classical.choose_spec (maximal_divisible hπ x.val x.property)).symm
176   right_inv y := by
177     apply mul_left_cancel₀ hπ.ne_zero
178     exact (Classical.choose_spec (maximal_divisible hπ (π*y) (by
179       rw [hπ.maximalIdeal_eq, Ideal.mem_span_singleton]
180       exact dvd_mul_right π y))).symm
181 
182 /-- Arbitrary streams, now indexed from the first positive digit. -/
183 noncomputable def positiveDigitEquiv : maximalIdeal R ≃ (ℕ → ResidueField R) :=
184   (uniformizerEquiv hπ).trans (digitEquiv hπ s hs)
185 
186 /-- The positive-depth expansion has an error divisible by π^(n+1). -/
187 theorem positive_encoding (x : maximalIdeal R) (n : ℕ) :
188     π^(n+1) ∣ x.val - π*partialSum (π := π) s (positiveDigitEquiv hπ s hs x) n := by
189   have hx : x.val = π * uniformizerEquiv hπ x :=
190     Classical.choose_spec (maximal_divisible hπ x.val x.property)
191   have he := digits_encode hπ s hs (uniformizerEquiv hπ x) n
192   rw [hx, pow_succ']
193   change π*π^n ∣ π * uniformizerEquiv hπ x - π*partialSum s (digits hπ s hs (uniformizerEquiv hπ x)) n
194   rw [← mul_sub]
195   exact mul_dvd_mul_left π he
196 
197 /-- Complete smooth formal maps are exactly d independent positive digit streams. -/
198 noncomputable def integralPointDigitEquiv (d : ℕ) :
199     PaperX.IntegralCharts.IntegralPoint (R := R) d ≃ (Fin d → ℕ → ResidueField R) :=
200   (PaperX.IntegralCharts.integralPointEquiv d).trans
201     (Equiv.piCongrRight fun _ => positiveDigitEquiv hπ s hs)
202 
203 /-- The stream equivalence reconstructs each actual formal parameter with the
204 correct shifted precision. -/
205 theorem parameter_digit_expansion {d : ℕ}
206     (f : PaperX.IntegralCharts.IntegralPoint (R := R) d) (i : Fin d) (n : ℕ) :
207     π^(n+1) ∣ f.val (MvPowerSeries.X i) -
208       π * partialSum (π := π) s (integralPointDigitEquiv hπ s hs d f i) n := by
209   exact positive_encoding hπ s hs (PaperX.IntegralCharts.integralParameters f i) n
210 
211 end PaperX.Digits
212 

Back to source controls