DensePadicIsometry.lean

1 /-
2 Author: Komorebi P.
3 
4 An isometric map on the natural-number points of the p-adic integers extends
5 uniquely to an isometric bijection of the p-adic integers.
6 -/
7 module
8 
9 public import Mathlib.NumberTheory.Padics.ProperSpace
10 public import Mathlib.Topology.MetricSpace.Isometry
11 public import Mathlib.Topology.UniformSpace.UniformEmbedding
12 public import CompactSelfIsometry
13 
14 @[expose] public section
15 
16 namespace KomorebiPaperIX.DensePadicIsometry
17 
18 variable (p : ℕ) [Fact p.Prime]
19 
20 /-- Interpret the prescribed values as a function on the natural-cast range,
21 equipped with the metric induced by the p-adic integers. -/
22 noncomputable def onNaturalRange (f : ℕ → ℤ_[p])
23     (x : Set.range (Nat.cast : ℕ → ℤ_[p])) : ℤ_[p] :=
24   f x.property.choose
25 
26 theorem onNaturalRange_nat (f : ℕ → ℤ_[p]) (n : ℕ) :
27     onNaturalRange p f ⟨(n : ℤ_[p]), ⟨n, rfl⟩⟩ = f n := by
28   unfold onNaturalRange
29   congr 1
30   exact Nat.cast_injective (Exists.choose_spec (show ∃ m : ℕ, (m : ℤ_[p]) = n from ⟨n, rfl⟩))
31 
32 theorem onNaturalRange_isometry (f : ℕ → ℤ_[p])
33     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
34     Isometry (onNaturalRange p f) := by
35   apply Isometry.of_dist_eq
36   intro x y
37   change dist (f x.property.choose) (f y.property.choose) = dist (x : ℤ_[p]) (y : ℤ_[p])
38   rw [hdist, x.property.choose_spec, y.property.choose_spec]
39 
40 /-- Continuous extension from the dense natural-cast range. -/
41 noncomputable def extension (f : ℕ → ℤ_[p]) : ℤ_[p] → ℤ_[p] :=
42   PadicInt.denseRange_natCast.extend (onNaturalRange p f)
43 
44 theorem extension_continuous (f : ℕ → ℤ_[p])
45     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
46     Continuous (extension p f) :=
47   (PadicInt.denseRange_natCast.uniformContinuous_extend
48     (onNaturalRange_isometry p f hdist).uniformContinuous).continuous
49 
50 theorem extension_nat (f : ℕ → ℤ_[p])
51     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) (n : ℕ) :
52     extension p f (n : ℤ_[p]) = f n := by
53   exact (PadicInt.denseRange_natCast.extend_of_ind
54     (onNaturalRange_isometry p f hdist).uniformContinuous
55     ⟨(n : ℤ_[p]), ⟨n, rfl⟩⟩).trans (onNaturalRange_nat p f n)
56 
57 theorem extension_isometry (f : ℕ → ℤ_[p])
58     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
59     Isometry (extension p f) := by
60   have hc := extension_continuous p f hdist
61   have heq : (fun z : ℤ_[p] × ℤ_[p] => dist (extension p f z.1) (extension p f z.2)) =
62       (fun z : ℤ_[p] × ℤ_[p] => dist z.1 z.2) := by
63     apply (PadicInt.denseRange_natCast.prodMap PadicInt.denseRange_natCast).equalizer
64       ((hc.comp continuous_fst).dist (hc.comp continuous_snd))
65       (continuous_fst.dist continuous_snd)
66     funext z
67     change dist (extension p f (z.1 : ℤ_[p])) (extension p f (z.2 : ℤ_[p])) = _
68     rw [extension_nat p f hdist, extension_nat p f hdist]
69     exact hdist z.1 z.2
70   exact Isometry.of_dist_eq (fun x y => congrFun heq (x, y))
71 
72 /-- Agreement on every natural number determines the entire continuous map. -/
73 theorem extension_unique (f : ℕ → ℤ_[p])
74     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p]))
75     (g : ℤ_[p] → ℤ_[p]) (hg : Continuous g)
76     (hgnat : ∀ n : ℕ, g (n : ℤ_[p]) = f n) : g = extension p f := by
77   apply PadicInt.denseRange_natCast.equalizer hg (extension_continuous p f hdist)
78   funext n
79   exact (hgnat n).trans (extension_nat p f hdist n).symm
80 
81 theorem extension_surjective (f : ℕ → ℤ_[p])
82     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
83     Function.Surjective (extension p f) :=
84   CompactSelfIsometry.surjective (extension_isometry p f hdist)
85 
86 /-- The prescribed isometry on natural-number points determines an isometric
87 bijection of the entire space of p-adic integers. -/
88 noncomputable def extensionEquiv (f : ℕ → ℤ_[p])
89     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
90     ℤ_[p] ≃ᵢ ℤ_[p] where
91   toEquiv := Equiv.ofBijective (extension p f)
92     ⟨(extension_isometry p f hdist).injective, extension_surjective p f hdist⟩
93   isometry_toFun := extension_isometry p f hdist
94 
95 theorem extensionEquiv_apply (f : ℕ → ℤ_[p])
96     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p]))
97     (x : ℤ_[p]) : extensionEquiv p f hdist x = extension p f x := rfl
98 
99 theorem extensionEquiv_nat (f : ℕ → ℤ_[p])
100     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) (n : ℕ) :
101     extensionEquiv p f hdist (n : ℤ_[p]) = f n :=
102   extension_nat p f hdist n
103 
104 theorem extensionEquiv_unique_continuous (f : ℕ → ℤ_[p])
105     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p]))
106     (g : ℤ_[p] → ℤ_[p]) (hg : Continuous g)
107     (hgnat : ∀ n : ℕ, g (n : ℤ_[p]) = f n) : g = extensionEquiv p f hdist :=
108   extension_unique p f hdist g hg hgnat
109 
110 theorem extensionEquiv_unique (f : ℕ → ℤ_[p])
111     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p]))
112     (e : ℤ_[p] ≃ᵢ ℤ_[p]) (henat : ∀ n : ℕ, e (n : ℤ_[p]) = f n) :
113     e = extensionEquiv p f hdist := by
114   apply IsometryEquiv.ext
115   exact congrFun (extensionEquiv_unique_continuous p f hdist e e.continuous henat)
116 
117 theorem existsUnique_extensionEquiv (f : ℕ → ℤ_[p])
118     (hdist : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
119     ∃! e : ℤ_[p] ≃ᵢ ℤ_[p], ∀ n : ℕ, e (n : ℤ_[p]) = f n :=
120   ⟨extensionEquiv p f hdist, extensionEquiv_nat p f hdist,
121     fun e he => extensionEquiv_unique p f hdist e he⟩
122 
123 end KomorebiPaperIX.DensePadicIsometry

Back to source controls