Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity
ProCGroups/FoxDifferential/Completed/Continuous/Free/Continuity/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity

1import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Derivative
2import ProCGroups.FoxDifferential.Completed.Continuous.Topology
4/-!
5# Fox differential: completed — continuous — free — continuity
7The principal declarations in this module are:
9- `continuous_freeProCZCCompletedFoxSemidirectGenerator`
10 The completed Fox semidirect generator map is continuous when both component maps are continuous.
11- `continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete`
12 The completed Fox semidirect generator map is continuous for a discrete generating space.
13- `continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential`
14 A crossed-differential graph into the completed Fox semidirect target is continuous when both its
15 component maps are continuous.
16- `continuous_freeProCZCCompletedFoxRightHom`
17 The target-group component of the free pro-\(C\) completed Fox semidirect lift is continuous.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open scoped BigOperators
27universe u
30variable {C : ProCGroups.FiniteGroupClass.{u}}
31variable (X H : Type u) [DecidableEq X]
32variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34/--
35The completed Fox semidirect generator map is continuous when both component maps are
36continuous.
37-/
38theorem continuous_freeProCZCCompletedFoxSemidirectGenerator
39 [TopologicalSpace X]
40 (φ : X → H)
41 (hleft : Continuous (fun x : X =>
42 Pi.single x (1 : ZCCompletedGroupAlgebra C H)))
43 (hφ : Continuous φ) :
44 Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) := by
45 rw [continuous_induced_rng]
46 exact hleft.prodMk hφ
48/-- The completed Fox semidirect generator map is continuous for a discrete generating space. -/
49theorem continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
50 [TopologicalSpace X] [DiscreteTopology X] (φ : X → H) :
51 Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) :=
52 continuous_of_discreteTopology
54variable {F : Type u}
55variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
56variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
58omit
59 [DecidableEq X] [IsTopologicalGroup F]
60 [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
61/--
62A crossed-differential graph into the completed Fox semidirect target is continuous when both
63its component maps are continuous.
64-/
65theorem continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
66 (ψ : F →* H)
67 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
68 (ZCFreeFoxCoordinates C (X := X) (H := H)))
69 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ) :
70 Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
71 (C := C) (X := X) (F := F) (H := H) ψ delta) := by
72 rw [continuous_induced_rng]
73 exact hdelta_continuous.prodMk hψ_continuous
75variable [TopologicalSpace X]
77section ProfiniteTarget
79variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
80variable [T2Space (ZCCompletedFoxSemidirect C X H)]
81variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
83/-- The target-group component of the free pro-\(C\) completed Fox semidirect lift is continuous. -/
84theorem continuous_freeProCZCCompletedFoxRightHom
85 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
86 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
87 (φ : X → H)
88 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
89 Continuous (freeProCZCCompletedFoxRightHom
90 (C := C) hι htarget φ hφ) := by
91 change Continuous (fun g : F =>
92 (freeProCZCCompletedFoxSemidirectLift
93 (C := C) hι htarget φ hφ g).right)
94 exact (continuous_zcCompletedFoxSemidirect_right C X H).comp
95 (continuous_freeProCZCCompletedFoxSemidirectLift
96 (C := C) hι htarget φ hφ)
98omit
99 [TopologicalSpace X] in
100/-- The right component of the converging-set completed Fox semidirect lift is continuous. -/
101theorem continuous_freeProCZCCompletedFoxRightHomOfConvergingSet
102 {ι : X → F}
104 (C := C) X F ι)
105 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
106 (φ : X → H)
107 (hφconv :
109 (G := ZCCompletedFoxSemidirect C X H)
110 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
111 (hφgen :
113 (G := ZCCompletedFoxSemidirect C X H)
114 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
115 Continuous (freeProCZCCompletedFoxRightHomOfConvergingSet
116 (C := C) hι htarget φ hφconv hφgen) := by
117 change Continuous (fun g : F =>
118 (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
119 (C := C) hι htarget φ hφconv hφgen g).right)
120 exact (continuous_zcCompletedFoxSemidirect_right C X H).comp
121 (continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
122 (C := C) hι htarget φ hφconv hφgen)
124section ProfiniteCodomain
126variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
128omit
129 [TopologicalSpace X] in
130/--
131The right component of the converging-set semidirect Fox lift is exactly the universal
132free-pro-\(C\) lift of its generator values.
133-/
134theorem freeProCZCCompletedFoxRightHomOfConvergingSet_eq_lift
135 {ι : X → F}
137 (C := C) X F ι)
139 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
140 (φ : X → H)
141 (hφconv :
143 (G := ZCCompletedFoxSemidirect C X H)
144 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
145 (hφgen :
147 (G := ZCCompletedFoxSemidirect C X H)
148 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
150 (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
151 freeProCZCCompletedFoxRightHomOfConvergingSet
152 (C := C) hι htarget φ hφconv hφgen =
153 hι.lift hH φ hφHconv hφHgen := by
154 apply hι.lift_unique hH φ hφHconv hφHgen
155 · exact continuous_freeProCZCCompletedFoxRightHomOfConvergingSet
156 (C := C) X H hι htarget φ hφconv hφgen
157 · intro x
158 simp only [freeProCZCCompletedFoxRightHomOfConvergingSet_generator]
160end ProfiniteCodomain
162omit
163 [TopologicalSpace X] in
164/--
165The closed-generated completed Fox semidirect lift is continuous as a map to the full semidirect
166target.
167-/
168theorem continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
169 {ι : X → F}
171 (C := C) X F ι)
172 (φ : X → H)
173 (htarget :
175 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
176 (ZCCompletedFoxSemidirect C X H)))
177 (hφconv :
179 (G :=
180 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
181 (ZCCompletedFoxSemidirect C X H)))
182 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
183 Continuous (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
184 (C := C) hι φ htarget hφconv) := by
185 change Continuous (fun g : F =>
186 (freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
187 (C := C) hι φ htarget hφconv g :
188 ZCCompletedFoxSemidirect C X H))
189 exact continuous_subtype_val.comp
190 (freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
191 (C := C) hι φ htarget hφconv).continuous_toFun
193omit
194 [TopologicalSpace X] in
195/-- The right component of the closed-generated completed Fox semidirect lift is continuous. -/
196theorem continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated
197 {ι : X → F}
199 (C := C) X F ι)
200 (φ : X → H)
201 (htarget :
203 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
204 (ZCCompletedFoxSemidirect C X H)))
205 (hφconv :
207 (G :=
208 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
209 (ZCCompletedFoxSemidirect C X H)))
210 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
211 Continuous (freeProCZCCompletedFoxRightHomViaClosedGenerated
212 (C := C) hι φ htarget hφconv) := by
213 change Continuous (fun g : F =>
214 (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
215 (C := C) hι φ htarget hφconv g).right)
216 exact (continuous_zcCompletedFoxSemidirect_right C X H).comp
217 (continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
218 (C := C) X H hι φ htarget hφconv)
220section ProfiniteCodomain
222variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
224omit
225 [TopologicalSpace X] in
226/--
227The right component of the closed-generated semidirect Fox lift is the universal free-pro-\(C\)
228lift of its generator values.
229-/
230theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift
231 {ι : X → F}
233 (C := C) X F ι)
235 (φ : X → H)
236 (htarget :
238 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
239 (ZCCompletedFoxSemidirect C X H)))
240 (hφconv :
242 (G :=
243 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
244 (ZCCompletedFoxSemidirect C X H)))
245 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
247 (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
248 freeProCZCCompletedFoxRightHomViaClosedGenerated
249 (C := C) hι φ htarget hφconv =
250 hι.lift hH φ hφHconv hφHgen := by
251 apply hι.lift_unique hH φ hφHconv hφHgen
252 · exact continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated
253 (C := C) X H hι φ htarget hφconv
254 · intro x
255 simp only [freeProCZCCompletedFoxRightHomViaClosedGenerated_generator]
257omit
258 [TopologicalSpace X] in
259/--
260The right component of the closed-generated semidirect Fox lift is the intended continuous
261homomorphism with the same generator values.
262-/
263theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
264 {ι : X → F}
266 (C := C) X F ι)
268 (φ : X → H)
269 (htarget :
271 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
272 (ZCCompletedFoxSemidirect C X H)))
273 (hφconv :
275 (G :=
276 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
277 (ZCCompletedFoxSemidirect C X H)))
278 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
280 (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
281 (ψ : F →ₜ* H)
282 (hψ_gen : ∀ x : X, ψ (ι x) = φ x) :
283 freeProCZCCompletedFoxRightHomViaClosedGenerated
284 (C := C) hι φ htarget hφconv =
285 ψ.toMonoidHom := by
286 have hright_lift :
287 freeProCZCCompletedFoxRightHomViaClosedGenerated
288 (C := C) hι φ htarget hφconv =
289 hι.lift hH φ hφHconv hφHgen :=
290 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift
291 (C := C) X H hι hH φ htarget hφconv hφHconv hφHgen
292 have hψ_lift :
293 ψ.toMonoidHom = hι.lift hH φ hφHconv hφHgen := by
294 apply hι.lift_unique hH φ hφHconv hφHgen
295 · exact ψ.continuous_toFun
296 · exact hψ_gen
297 exact hright_lift.trans hψ_lift.symm
299end ProfiniteCodomain
301omit
302 [TopologicalSpace X] in
303/-- The derivative-vector component of the closed-generated semidirect lift is continuous. -/
304theorem continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
305 {ι : X → F}
307 (C := C) X F ι)
308 (φ : X → H)
309 (htarget :
311 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
312 (ZCCompletedFoxSemidirect C X H)))
313 (hφconv :
315 (G :=
316 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
317 (ZCCompletedFoxSemidirect C X H)))
318 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
319 Continuous (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
320 (C := C) hι φ htarget hφconv) := by
321 change Continuous (fun g : F =>
322 (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
323 (C := C) hι φ htarget hφconv g).left)
324 exact (continuous_zcCompletedFoxSemidirect_left C X H).comp
325 (continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
326 (C := C) X H hι φ htarget hφconv)
328/--
329The completed Fox derivative-vector component of the free pro-\(C\) semidirect lift is
330continuous.
331-/
332theorem continuous_freeProCZCCompletedFoxDerivativeVector
333 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
334 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
335 (φ : X → H)
336 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
337 Continuous (freeProCZCCompletedFoxDerivativeVector
338 (C := C) hι htarget φ hφ) := by
339 change Continuous (fun g : F =>
340 (freeProCZCCompletedFoxSemidirectLift
341 (C := C) hι htarget φ hφ g).left)
342 exact (continuous_zcCompletedFoxSemidirect_left C X H).comp
343 (continuous_freeProCZCCompletedFoxSemidirectLift
344 (C := C) hι htarget φ hφ)
346omit
347 [TopologicalSpace X] in
348/--
349The derivative-vector component of the converging-set completed Fox semidirect lift is
350continuous.
351-/
352theorem continuous_freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
353 {ι : X → F}
355 (C := C) X F ι)
356 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
357 (φ : X → H)
358 (hφconv :
360 (G := ZCCompletedFoxSemidirect C X H)
361 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
362 (hφgen :
364 (G := ZCCompletedFoxSemidirect C X H)
365 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
366 Continuous (freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
367 (C := C) hι htarget φ hφconv hφgen) := by
368 change Continuous (fun g : F =>
369 (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
370 (C := C) hι htarget φ hφconv hφgen g).left)
371 exact (continuous_zcCompletedFoxSemidirect_left C X H).comp
372 (continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
373 (C := C) hι htarget φ hφconv hφgen)
375end ProfiniteTarget
377/--
378The semidirect generator map attached to a continuous crossed differential is continuous once
379the component maps are continuous.
380-/
381theorem continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
382 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
383 (ψ : F →* H)
384 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
385 (ZCFreeFoxCoordinates C (X := X) (H := H)))
386 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
387 (hbasis :
388 ∀ x : X, delta (ι x) =
389 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
390 Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x))) :=
391 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
392 (C := C) hι ψ delta
393 (continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
394 (C := C) (X := X) (F := F) (H := H)
395 ψ delta hdelta_continuous hψ_continuous)
396 hbasis
398section ProfiniteTarget
400variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
401variable [T2Space (ZCCompletedFoxSemidirect C X H)]
402variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
404/--
405Continuous completed crossed differentials with continuous coefficient homomorphism are uniquely
406identified with the canonical free pro-\(C\) completed Fox derivative vector.
407-/
408theorem freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDiff_components
409 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
410 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
411 (ψ : F →* H)
412 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
413 (ZCFreeFoxCoordinates C (X := X) (H := H)))
414 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
415 (hbasis :
416 ∀ x : X, delta (ι x) =
417 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
418 (fun g : F => delta g) =
419 fun g : F =>
420 freeProCZCCompletedFoxDerivativeVector
421 (C := C) hι htarget (fun x : X => ψ (ι x))
422 (continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
423 (C := C) X H hι ψ delta hdelta_continuous hψ_continuous hbasis) g :=
424 freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential
425 (C := C) hι htarget ψ delta
426 (continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
427 (C := C) (X := X) (F := F) (H := H)
428 ψ delta hdelta_continuous hψ_continuous)
429 hbasis
431end ProfiniteTarget
433end
435end FoxDifferential