TopologyDenseCompletion.lean

1 import PaperIRelease.TopologyTransport
2 import Mathlib.Topology.Algebra.GroupCompletion
3 import Mathlib.Topology.Algebra.Module.LocallyConvex
4 
5 /-!
6 # Dense presentations with the transported locally convex topology
7 
8 The uniformity is explicitly pulled back along the presentation map.
9 The comparison map is constructed by the universal property of completion.
10 Its inverse, linearity, uniqueness, and intertwining are proved here.
11 -/
12 
13 noncomputable section
14 open Set Function UniformSpace Topology
15 
16 namespace PaperIRelease.TopologyDenseCompletion
17 
18 section Transport
19 
20 variable {𝕜 E X : Type*} [Ring 𝕜]
21 variable [AddCommGroup E] [Module 𝕜 E]
22 variable [AddCommGroup X] [Module 𝕜 X] [UniformSpace X]
23 
24 /-- The uniformity transported from the image of the linear presentation. -/
25 @[instance_reducible]
26 def transportedUniformity (j : E →ₗ[𝕜] X) : UniformSpace E :=
27   UniformSpace.comap j inferInstance
28 
29 /-- Its topology is exactly the subspace topology pulled back along `j`. -/
30 theorem transported_isUniformInducing (j : E →ₗ[𝕜] X) :
31     let : UniformSpace E := transportedUniformity j
32     IsUniformInducing j := by
33   let : UniformSpace E := transportedUniformity j
34   exact ⟨rfl⟩
35 
36 /-- Pulling back the linear topology preserves local convexity. -/
37 theorem transported_locallyConvex [PartialOrder 𝕜] [IsOrderedRing 𝕜]
38     [LocallyConvexSpace 𝕜 X] (j : E →ₗ[𝕜] X) :
39     let : UniformSpace E := transportedUniformity j
40     LocallyConvexSpace 𝕜 E := by
41   let : UniformSpace E := transportedUniformity j
42   exact (transported_isUniformInducing j).isInducing.locallyConvexSpace
43 
44 /-- The transported additive uniformity is compatible with the group law. -/
45 theorem transported_uniformAddGroup [IsUniformAddGroup X] (j : E →ₗ[𝕜] X) :
46     let : UniformSpace E := transportedUniformity j
47     IsUniformAddGroup E := by
48   let : UniformSpace E := transportedUniformity j
49   exact (transported_isUniformInducing j).isUniformAddGroup j
50 
51 /-- Scalar multiplication is uniformly continuous in the transported topology. -/
52 theorem transported_uniformConstSMul [UniformContinuousConstSMul 𝕜 X]
53     (j : E →ₗ[𝕜] X) :
54     let : UniformSpace E := transportedUniformity j
55     UniformContinuousConstSMul 𝕜 E := by
56   let : UniformSpace E := transportedUniformity j
57   exact (transported_isUniformInducing j).uniformContinuousConstSMul (map_smul j)
58 
59 end Transport
60 
61 section Completion
62 
63 variable {𝕜 E X : Type*} [Ring 𝕜]
64 variable [AddCommGroup E] [Module 𝕜 E] [UniformSpace E]
65 variable [IsUniformAddGroup E] [UniformContinuousConstSMul 𝕜 E]
66 variable [AddCommGroup X] [Module 𝕜 X] [UniformSpace X]
67 variable [IsUniformAddGroup X] [UniformContinuousConstSMul 𝕜 X]
68 variable [CompleteSpace X] [T0Space X]
69 
70 /-- The complete target with its dense presentation map is an abstract
71 completion, because the domain carries the transported uniformity. -/
72 def presentationCompletion (j : E →ₗ[𝕜] X)
73     (hj : IsUniformInducing j) (hd : DenseRange j) : AbstractCompletion E where
74   space := X
75   coe := j
76   uniformStruct := inferInstance
77   complete := inferInstance
78   separation := inferInstance
79   isUniformInducing := hj
80   dense := hd
81 
82 /-- The canonical uniform isomorphism extending the dense presentation. -/
83 def completionUniformEquiv (j : E →ₗ[𝕜] X)
84     (hj : IsUniformInducing j) (hd : DenseRange j) : Completion E ≃ᵤ X :=
85   Completion.cPkg.compareEquiv (presentationCompletion j hj hd)
86 
87 omit [IsUniformAddGroup E] [UniformContinuousConstSMul 𝕜 E]
88   [IsUniformAddGroup X] [UniformContinuousConstSMul 𝕜 X] in
89 @[simp]
90 theorem completionUniformEquiv_apply_coe (j : E →ₗ[𝕜] X)
91     (hj : IsUniformInducing j) (hd : DenseRange j) (x : E) :
92     completionUniformEquiv j hj hd (x : Completion E) = j x :=
93   Completion.cPkg.compare_coe (presentationCompletion j hj hd) x
94 
95 /-- The completed presentation is a topological linear isomorphism. -/
96 def completionLinearEquiv (j : E →ₗ[𝕜] X)
97     (hj : IsUniformInducing j) (hd : DenseRange j) : Completion E ≃L[𝕜] X where
98   toEquiv := (completionUniformEquiv j hj hd).toEquiv
99   map_add' x y := by
100     induction x, y using Completion.induction_on₂ with
101     | hp =>
102       exact isClosed_eq
103         ((completionUniformEquiv j hj hd).continuous.comp (continuous_fst.add continuous_snd))
104         (((completionUniformEquiv j hj hd).continuous.comp continuous_fst).add
105           ((completionUniformEquiv j hj hd).continuous.comp continuous_snd))
106     | ih x y => simp only [← Completion.coe_add, Equiv.toFun_as_coe,
107         UniformEquiv.coe_toEquiv, completionUniformEquiv_apply_coe, map_add]
108   map_smul' c x := by
109     induction x using Completion.induction_on with
110     | hp =>
111       exact isClosed_eq
112         ((completionUniformEquiv j hj hd).continuous.comp (continuous_const_smul c))
113         ((completionUniformEquiv j hj hd).continuous.const_smul c)
114     | ih x => simp only [← Completion.coe_smul, Equiv.toFun_as_coe,
115         UniformEquiv.coe_toEquiv, completionUniformEquiv_apply_coe, map_smul,
116         RingHom.id_apply]
117   continuous_toFun := (completionUniformEquiv j hj hd).continuous
118   continuous_invFun := (completionUniformEquiv j hj hd).symm.continuous
119 
120 @[simp]
121 theorem completionLinearEquiv_apply_coe (j : E →ₗ[𝕜] X)
122     (hj : IsUniformInducing j) (hd : DenseRange j) (x : E) :
123     completionLinearEquiv j hj hd (x : Completion E) = j x :=
124   completionUniformEquiv_apply_coe j hj hd x
125 
126 /-- The canonical extension is the unique continuous extension. -/
127 theorem completionLinearEquiv_unique (j : E →ₗ[𝕜] X)
128     (hj : IsUniformInducing j) (hd : DenseRange j)
129     (g : Completion E → X) (hg : Continuous g)
130     (hext : ∀ x : E, g (x : Completion E) = j x) :
131     g = completionLinearEquiv j hj hd := by
132   apply Completion.denseRange_coe.equalizer hg
133     (completionLinearEquiv j hj hd).continuous
134   funext x
135   exact (hext x).trans (completionLinearEquiv_apply_coe j hj hd x).symm
136 
137 omit [IsUniformAddGroup E] [UniformContinuousConstSMul 𝕜 E]
138   [UniformContinuousConstSMul 𝕜 X] [CompleteSpace X] [T0Space X] in
139 /-- Intertwining with a continuous target operator makes the algebraic
140 operator on the presentation uniformly continuous in the induced topology. -/
141 theorem presentation_action_uniformContinuous (j : E →ₗ[𝕜] X)
142     (hj : IsUniformInducing j) (T : E →ₗ[𝕜] E) (B : X →L[𝕜] X)
143     (hintertwine : ∀ x, j (T x) = B (j x)) : UniformContinuous T := by
144   apply hj.uniformContinuous_iff.mpr
145   have h : (j : E → X) ∘ T = B ∘ j := funext hintertwine
146   rw [h]
147   exact B.uniformContinuous.comp hj.uniformContinuous
148 
149 /-- The uniquely extended action operator, constructed by conjugation
150 through the canonical completion isomorphism. -/
151 def completedAction (j : E →ₗ[𝕜] X)
152     (hj : IsUniformInducing j) (hd : DenseRange j) (B : X →L[𝕜] X) :
153     Completion E →L[𝕜] Completion E :=
154   (completionLinearEquiv j hj hd).symm.toContinuousLinearMap.comp
155     (B.comp (completionLinearEquiv j hj hd).toContinuousLinearMap)
156 
157 @[simp]
158 theorem completedAction_apply_coe (j : E →ₗ[𝕜] X)
159     (hj : IsUniformInducing j) (hd : DenseRange j)
160     (T : E →ₗ[𝕜] E) (B : X →L[𝕜] X)
161     (hintertwine : ∀ x, j (T x) = B (j x)) (x : E) :
162     completedAction j hj hd B (x : Completion E) = (T x : Completion E) := by
163   apply (completionLinearEquiv j hj hd).injective
164   simp [completedAction, ← hintertwine]
165 
166 /-- The completion isomorphism intertwines the entire extended action. -/
167 theorem completion_intertwines (j : E →ₗ[𝕜] X)
168     (hj : IsUniformInducing j) (hd : DenseRange j) (B : X →L[𝕜] X) :
169     (completionLinearEquiv j hj hd).toContinuousLinearMap.comp
170         (completedAction j hj hd B) =
171       B.comp (completionLinearEquiv j hj hd).toContinuousLinearMap := by
172   ext x
173   simp [completedAction]
174 
175 end Completion
176 
177 section QuotientPresentation
178 
179 variable {𝕜 F X : Type*} [Ring 𝕜]
180 variable [AddCommGroup F] [Module 𝕜 F]
181 variable [AddCommGroup X] [Module 𝕜 X] [UniformSpace X]
182 variable [IsUniformAddGroup X] [UniformContinuousConstSMul 𝕜 X]
183 variable [CompleteSpace X] [T0Space X]
184 
185 /-- The actual injective map induced on the quotient of a presentation by
186 its relation module. No topology on the free module is presupposed. -/
187 def quotientEmbedding (f : F →ₗ[𝕜] X) : (F ⧸ f.ker) →ₗ[𝕜] X :=
188   f.range.subtype.comp f.quotKerEquivRange.toLinearMap
189 
190 omit [UniformSpace X] [IsUniformAddGroup X] [UniformContinuousConstSMul 𝕜 X]
191   [CompleteSpace X] [T0Space X] in
192 @[simp]
193 theorem quotientEmbedding_apply_mk (f : F →ₗ[𝕜] X) (x : F) :
194     quotientEmbedding f (f.ker.mkQ x) = f x :=
195   f.quotKerEquivRange_apply_mk x
196 
197 omit [UniformSpace X] [IsUniformAddGroup X] [UniformContinuousConstSMul 𝕜 X]
198   [CompleteSpace X] [T0Space X] in
199 theorem quotientEmbedding_injective (f : F →ₗ[𝕜] X) :
200     Injective (quotientEmbedding f) :=
201   Subtype.val_injective.comp f.quotKerEquivRange.injective
202 
203 omit [IsUniformAddGroup X] [UniformContinuousConstSMul 𝕜 X]
204   [CompleteSpace X] [T0Space X] in
205 theorem quotientEmbedding_dense (f : F →ₗ[𝕜] X) (hd : DenseRange f) :
206     DenseRange (quotientEmbedding f) := by
207   apply hd.mono
208   rintro x ⟨y, rfl⟩
209   exact ⟨f.ker.mkQ y, quotientEmbedding_apply_mk f y⟩
210 
211 /-- Completion of the quotient by the actual kernel of the presentation,
212 equipped with the topology transported from the target. This applies to
213 free seed evaluation and to the restriction of a quotient realization to
214 any subspace with dense image. -/
215 def completedQuotientEquiv (f : F →ₗ[𝕜] X) (hd : DenseRange f) :
216     letI : UniformSpace (F ⧸ f.ker) := transportedUniformity (quotientEmbedding f)
217     letI : IsUniformAddGroup (F ⧸ f.ker) :=
218       transported_uniformAddGroup (quotientEmbedding f)
219     letI : UniformContinuousConstSMul 𝕜 (F ⧸ f.ker) :=
220       transported_uniformConstSMul (quotientEmbedding f)
221     Completion (F ⧸ f.ker) ≃L[𝕜] X := by
222   letI : UniformSpace (F ⧸ f.ker) := transportedUniformity (quotientEmbedding f)
223   letI : IsUniformAddGroup (F ⧸ f.ker) :=
224     transported_uniformAddGroup (quotientEmbedding f)
225   letI : UniformContinuousConstSMul 𝕜 (F ⧸ f.ker) :=
226     transported_uniformConstSMul (quotientEmbedding f)
227   exact completionLinearEquiv (quotientEmbedding f)
228     (transported_isUniformInducing (quotientEmbedding f)) (quotientEmbedding_dense f hd)
229 
230 /-- The canonical completed quotient sends a represented class to its
231 original presentation value. -/
232 theorem completedQuotientEquiv_apply_mk (f : F →ₗ[𝕜] X) (hd : DenseRange f) (x : F) :
233     letI : UniformSpace (F ⧸ f.ker) := transportedUniformity (quotientEmbedding f)
234     letI : IsUniformAddGroup (F ⧸ f.ker) :=
235       transported_uniformAddGroup (quotientEmbedding f)
236     letI : UniformContinuousConstSMul 𝕜 (F ⧸ f.ker) :=
237       transported_uniformConstSMul (quotientEmbedding f)
238     completedQuotientEquiv f hd (f.ker.mkQ x : Completion (F ⧸ f.ker)) = f x := by
239   let : UniformSpace (F ⧸ f.ker) := transportedUniformity (quotientEmbedding f)
240   let : IsUniformAddGroup (F ⧸ f.ker) :=
241     transported_uniformAddGroup (quotientEmbedding f)
242   let : UniformContinuousConstSMul 𝕜 (F ⧸ f.ker) :=
243     transported_uniformConstSMul (quotientEmbedding f)
244   exact (completionLinearEquiv_apply_coe (quotientEmbedding f)
245     (transported_isUniformInducing (quotientEmbedding f))
246     (quotientEmbedding_dense f hd) (f.ker.mkQ x)).trans (quotientEmbedding_apply_mk f x)
247 
248 end QuotientPresentation
249 
250 end PaperIRelease.TopologyDenseCompletion

Back to source controls