Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Topology
ProCGroups/FoxDifferential/Completed/Continuous/ClosedGeneratedCoordinates/Topology/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Topology

1import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Equiv
3/-!
4# Fox differential: completed — continuous — closed generated coordinates — topology
6The principal declarations in this module are:
8- `closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula`
9 The coordinate topology on \(A_{\psi}(C)\) transported from the closed-generated coordinate
10 equivalence.
11- `continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula`
12 The closed-generated coordinate equivalence is continuous for the transported coordinate topology
13 on \(A_{\psi}(C)\).
14- `t2Space_closedGenDerivativeCoordinateTopologyZC_of_fundFormula`
15 The coordinate topology transported to \(A_{\psi}(C)\) is Hausdorff.
16- `continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_symm`
17 The inverse of the closed-generated coordinate equivalence is continuous for the transported
18 coordinate topology on \(A_{\psi}(C)\). Equivalently, the displayed family map
19 \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \to A_{\psi}(C)\) is continuous for this topology.
20-/
22namespace CrowellExactSequence
24noncomputable section
26open scoped BigOperators
27open FoxDifferential
29universe u v w
31variable {G H : Type u}
32variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35section ClosedGeneratedCoordinateEquiv
37variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
38variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
39variable (C : ProCGroups.FiniteGroupClass.{u})
40variable (psi : ContinuousMonoidHom G H)
41variable {X : Type u} [Fintype X] [DecidableEq X]
42variable (family : X → G)
43variable
44 (hfree :
46 (C := C) X G family)
47variable
48 (htarget :
50 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
51 (C := C) (fun i : X => psi (family i)) : Subgroup
52 (ZCCompletedFoxSemidirect C X H)))
53variable
54 (hφconv :
56 (G :=
57 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
58 (C := C) (fun i : X => psi (family i)) : Subgroup
59 (ZCCompletedFoxSemidirect C X H)))
60 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
61 (C := C) (fun i : X => psi (family i))))
64/--
65The coordinate topology on \(A_{\psi}(C)\) transported from the closed-generated coordinate
66equivalence.
67-/
68@[implicit_reducible]
69def closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
71 (hφHconv :
73 (G := H) (fun i : X => psi (family i)))
74 (hφHgen :
76 (G := H) (Set.range (fun i : X => psi (family i))))
77 (hfundamental :
78 ∀ g : G,
79 presentedCompletedDifferentialFamilyMapProCInteger
80 (G := G) (H := H) C psi family
81 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
82 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
83 zcUniversalDifferential C psi.toMonoidHom g) :
84 TopologicalSpace
85 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
86 TopologicalSpace.induced
87 (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
88 (G := G) (H := H) C psi family hfree htarget hφconv
89 hH hφHconv hφHgen hfundamental)
90 inferInstance
92/--
93The closed-generated coordinate equivalence is continuous for the transported coordinate
94topology on \(A_{\psi}(C)\).
95-/
96theorem continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula
98 (hφHconv :
100 (G := H) (fun i : X => psi (family i)))
101 (hφHgen :
103 (G := H) (Set.range (fun i : X => psi (family i))))
104 (hfundamental :
105 ∀ g : G,
106 presentedCompletedDifferentialFamilyMapProCInteger
107 (G := G) (H := H) C psi family
108 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
109 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
110 zcUniversalDifferential C psi.toMonoidHom g) :
111 @Continuous
112 (ZCCompletedDifferentialModule C psi.toMonoidHom)
113 (ZCFreeFoxCoordinates C (X := X) (H := H))
114 (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
115 (G := G) (H := H) C psi family hfree htarget hφconv
116 hH hφHconv hφHgen hfundamental)
117 inferInstance
118 (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
119 (G := G) (H := H) C psi family hfree htarget hφconv
120 hH hφHconv hφHgen hfundamental) := by
121 exact continuous_induced_dom
123/-- The coordinate topology transported to \(A_{\psi}(C)\) is Hausdorff. -/
124theorem t2Space_closedGenDerivativeCoordinateTopologyZC_of_fundFormula
126 (hφHconv :
128 (G := H) (fun i : X => psi (family i)))
129 (hφHgen :
131 (G := H) (Set.range (fun i : X => psi (family i))))
132 (hfundamental :
133 ∀ g : G,
134 presentedCompletedDifferentialFamilyMapProCInteger
135 (G := G) (H := H) C psi family
136 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
137 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
138 zcUniversalDifferential C psi.toMonoidHom g) :
139 @T2Space
140 (ZCCompletedDifferentialModule C psi.toMonoidHom)
141 (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
142 (G := G) (H := H) C psi family hfree htarget hφconv
143 hH hφHconv hφHgen hfundamental) := by
144 letI : TopologicalSpace
145 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
146 closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
147 (G := G) (H := H) C psi family hfree htarget hφconv
148 hH hφHconv hφHgen hfundamental
149 let e :=
150 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
151 (G := G) (H := H) C psi family hfree htarget hφconv
152 hH hφHconv hφHgen hfundamental
153 have hcont : Continuous (e :
154 ZCCompletedDifferentialModule C psi.toMonoidHom →
155 ZCFreeFoxCoordinates C (X := X) (H := H)) := by
156 simpa [e] using
157 (continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula
158 (G := G) (H := H) C psi family hfree htarget hφconv
159 hH hφHconv hφHgen hfundamental)
160 exact T2Space.of_injective_continuous e.injective hcont
162/--
163The inverse of the closed-generated coordinate equivalence is continuous for the transported
164coordinate topology on \(A_{\psi}(C)\). Equivalently, the displayed family map
165\(\mathbb{Z}_C\llbracket H\rrbracket^{X} \to A_{\psi}(C)\) is continuous for this topology.
166-/
167theorem continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_symm
169 (hφHconv :
171 (G := H) (fun i : X => psi (family i)))
172 (hφHgen :
174 (G := H) (Set.range (fun i : X => psi (family i))))
175 (hfundamental :
176 ∀ g : G,
177 presentedCompletedDifferentialFamilyMapProCInteger
178 (G := G) (H := H) C psi family
179 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
180 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
181 zcUniversalDifferential C psi.toMonoidHom g) :
182 @Continuous
183 (ZCFreeFoxCoordinates C (X := X) (H := H))
184 (ZCCompletedDifferentialModule C psi.toMonoidHom)
185 inferInstance
186 (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
187 (G := G) (H := H) C psi family hfree htarget hφconv
188 hH hφHconv hφHgen hfundamental)
189 (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
190 (G := G) (H := H) C psi family hfree htarget hφconv
191 hH hφHconv hφHgen hfundamental).symm := by
192 let e :=
193 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
194 (G := G) (H := H) C psi family hfree htarget hφconv
195 hH hφHconv hφHgen hfundamental
196 rw [continuous_induced_rng]
197 change Continuous
198 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
199 e (e.symm x))
200 have hfun :
201 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
202 e (e.symm x)) =
203 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) => x) := by
204 funext x
205 exact e.apply_symm_apply x
206 rw [hfun]
207 exact continuous_id
209/--
210The displayed family map is continuous for the coordinate topology transported to
211\(A_{\psi}(C)\).
212-/
213theorem continuous_presentedCompletedDifferentialFamilyMapZC_coordTopology_of_fundFormula
215 (hφHconv :
217 (G := H) (fun i : X => psi (family i)))
218 (hφHgen :
220 (G := H) (Set.range (fun i : X => psi (family i))))
221 (hfundamental :
222 ∀ g : G,
223 presentedCompletedDifferentialFamilyMapProCInteger
224 (G := G) (H := H) C psi family
225 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
226 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
227 zcUniversalDifferential C psi.toMonoidHom g) :
228 @Continuous
229 (ZCFreeFoxCoordinates C (X := X) (H := H))
230 (ZCCompletedDifferentialModule C psi.toMonoidHom)
231 inferInstance
232 (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
233 (G := G) (H := H) C psi family hfree htarget hφconv
234 hH hφHconv hφHgen hfundamental)
235 (presentedCompletedDifferentialFamilyMapProCInteger
236 (G := G) (H := H) C psi family) := by
237 let e :=
238 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
239 (G := G) (H := H) C psi family hfree htarget hφconv
240 hH hφHconv hφHgen hfundamental
241 change @Continuous
242 (ZCFreeFoxCoordinates C (X := X) (H := H))
243 (ZCCompletedDifferentialModule C psi.toMonoidHom)
244 inferInstance
245 (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
246 (G := G) (H := H) C psi family hfree htarget hφconv
247 hH hφHconv hφHgen hfundamental)
248 (presentedCompletedDifferentialFamilyMapProCInteger
249 (G := G) (H := H) C psi family)
250 have hsymm :
251 e.symm.toLinearMap =
252 presentedCompletedDifferentialFamilyMapProCInteger
253 (G := G) (H := H) C psi family := by
254 simpa [e, closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula]
255 using
256 (presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap
257 (G := G) (H := H) C psi family
258 (isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
259 (G := G) (H := H) C psi family hfree htarget hφconv
260 hH hφHconv hφHgen hfundamental))
261 rw [← hsymm]
262 change @Continuous
263 (ZCFreeFoxCoordinates C (X := X) (H := H))
264 (ZCCompletedDifferentialModule C psi.toMonoidHom)
265 inferInstance
266 (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
267 (G := G) (H := H) C psi family hfree htarget hφconv
268 hH hφHconv hφHgen hfundamental)
269 ((closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
270 (G := G) (H := H) C psi family hfree htarget hφconv
271 hH hφHconv hφHgen hfundamental).symm :
272 ZCFreeFoxCoordinates C (X := X) (H := H) →
273 ZCCompletedDifferentialModule C psi.toMonoidHom)
274 exact
275 continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_symm
276 (G := G) (H := H) C psi family hfree htarget hφconv
277 hH hφHconv hφHgen hfundamental
279/--
280The universal differential \(g \mapsto d(g)\) is continuous for the coordinate topology
281transported to \(A_{\psi}(C)\).
282-/
283theorem continuous_zcUniversalDifferential_coordinateTopology_of_fundamental_formula
285 (hφHconv :
287 (G := H) (fun i : X => psi (family i)))
288 (hφHgen :
290 (G := H) (Set.range (fun i : X => psi (family i))))
291 (hfundamental :
292 ∀ g : G,
293 presentedCompletedDifferentialFamilyMapProCInteger
294 (G := G) (H := H) C psi family
295 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
296 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
297 zcUniversalDifferential C psi.toMonoidHom g) :
298 @Continuous G
299 (ZCCompletedDifferentialModule C psi.toMonoidHom)
300 inferInstance
301 (closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
302 (G := G) (H := H) C psi family hfree htarget hφconv
303 hH hφHconv hφHgen hfundamental)
304 (fun g : G => zcUniversalDifferential C psi.toMonoidHom g) := by
305 let e :=
306 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
307 (G := G) (H := H) C psi family hfree htarget hφconv
308 hH hφHconv hφHgen hfundamental
309 rw [continuous_induced_rng]
310 change Continuous
311 (fun g : G =>
312 e (zcUniversalDifferential C psi.toMonoidHom g))
313 have hfun :
314 (fun g : G =>
315 e (zcUniversalDifferential C psi.toMonoidHom g)) =
316 (fun g : G =>
317 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
318 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) := by
319 funext g
320 exact
321 closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_universal
322 (G := G) (H := H) C psi family hfree htarget hφconv
323 hH hφHconv hφHgen hfundamental g
324 rw [hfun]
325 exact
326 continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
327 (C := C) X H hfree (fun i : X => psi (family i)) htarget hφconv
329/-- Addition is continuous for the transported coordinate topology on \(A_{\psi}(C)\). -/
330theorem continuous_add_closedGenDerivativeCoordinateTopologyZC_of_fundFormula
332 (hφHconv :
334 (G := H) (fun i : X => psi (family i)))
335 (hφHgen :
337 (G := H) (Set.range (fun i : X => psi (family i))))
338 (hfundamental :
339 ∀ g : G,
340 presentedCompletedDifferentialFamilyMapProCInteger
341 (G := G) (H := H) C psi family
342 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
343 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
344 zcUniversalDifferential C psi.toMonoidHom g) :
345 letI : TopologicalSpace
346 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
347 closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
348 (G := G) (H := H) C psi family hfree htarget hφconv
349 hH hφHconv hφHgen hfundamental
350 Continuous (fun p :
351 ZCCompletedDifferentialModule C psi.toMonoidHom ×
352 ZCCompletedDifferentialModule C psi.toMonoidHom =>
353 p.1 + p.2) := by
354 letI : TopologicalSpace
355 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
356 closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
357 (G := G) (H := H) C psi family hfree htarget hφconv
358 hH hφHconv hφHgen hfundamental
359 let e :=
360 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
361 (G := G) (H := H) C psi family hfree htarget hφconv
362 hH hφHconv hφHgen hfundamental
363 have he : Continuous (e :
364 ZCCompletedDifferentialModule C psi.toMonoidHom →
365 ZCFreeFoxCoordinates C (X := X) (H := H)) := by
366 simpa [e] using
367 (continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula
368 (G := G) (H := H) C psi family hfree htarget hφconv
369 hH hφHconv hφHgen hfundamental)
370 rw [continuous_induced_rng]
371 change Continuous
372 (fun p :
373 ZCCompletedDifferentialModule C psi.toMonoidHom ×
374 ZCCompletedDifferentialModule C psi.toMonoidHom =>
375 e (p.1 + p.2))
376 have hcont :=
377 (he.comp continuous_fst).add (he.comp continuous_snd)
378 change Continuous
379 (fun p :
380 ZCCompletedDifferentialModule C psi.toMonoidHom ×
381 ZCCompletedDifferentialModule C psi.toMonoidHom =>
382 e p.1 + e p.2) at hcont
383 have hfun :
384 (fun p :
385 ZCCompletedDifferentialModule C psi.toMonoidHom ×
386 ZCCompletedDifferentialModule C psi.toMonoidHom =>
387 e (p.1 + p.2)) =
388 (fun p :
389 ZCCompletedDifferentialModule C psi.toMonoidHom ×
390 ZCCompletedDifferentialModule C psi.toMonoidHom =>
391 e p.1 + e p.2) := by
392 funext p
393 exact map_add e p.1 p.2
394 rw [hfun]
395 exact hcont
397/-- Negation is continuous for the transported coordinate topology on \(A_{\psi}(C)\). -/
398theorem continuous_neg_closedGenDerivativeCoordinateTopologyZC_of_fundFormula
400 (hφHconv :
402 (G := H) (fun i : X => psi (family i)))
403 (hφHgen :
405 (G := H) (Set.range (fun i : X => psi (family i))))
406 (hfundamental :
407 ∀ g : G,
408 presentedCompletedDifferentialFamilyMapProCInteger
409 (G := G) (H := H) C psi family
410 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
411 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
412 zcUniversalDifferential C psi.toMonoidHom g) :
413 letI : TopologicalSpace
414 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
415 closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
416 (G := G) (H := H) C psi family hfree htarget hφconv
417 hH hφHconv hφHgen hfundamental
418 Continuous
419 (fun a : ZCCompletedDifferentialModule C psi.toMonoidHom => -a) := by
420 letI : TopologicalSpace
421 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
422 closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
423 (G := G) (H := H) C psi family hfree htarget hφconv
424 hH hφHconv hφHgen hfundamental
425 let e :=
426 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
427 (G := G) (H := H) C psi family hfree htarget hφconv
428 hH hφHconv hφHgen hfundamental
429 have he : Continuous (e :
430 ZCCompletedDifferentialModule C psi.toMonoidHom →
431 ZCFreeFoxCoordinates C (X := X) (H := H)) := by
432 simpa [e] using
433 (continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula
434 (G := G) (H := H) C psi family hfree htarget hφconv
435 hH hφHconv hφHgen hfundamental)
436 rw [continuous_induced_rng]
437 change Continuous
438 (fun a : ZCCompletedDifferentialModule C psi.toMonoidHom => e (-a))
439 have hcont := he.neg
440 change Continuous
441 (fun a : ZCCompletedDifferentialModule C psi.toMonoidHom => -(e a)) at hcont
442 have hfun :
443 (fun a : ZCCompletedDifferentialModule C psi.toMonoidHom => e (-a)) =
444 (fun a : ZCCompletedDifferentialModule C psi.toMonoidHom => -(e a)) := by
445 funext a
446 exact map_neg e a
447 rw [hfun]
448 exact hcont
450/--
451Scalar multiplication is continuous for the transported coordinate topology on \(A_{\psi}(C)\).
452-/
453theorem continuous_smul_closedGenDerivativeCoordinateTopologyZC_of_fundFormula
455 (hφHconv :
457 (G := H) (fun i : X => psi (family i)))
458 (hφHgen :
460 (G := H) (Set.range (fun i : X => psi (family i))))
461 (hfundamental :
462 ∀ g : G,
463 presentedCompletedDifferentialFamilyMapProCInteger
464 (G := G) (H := H) C psi family
465 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
466 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
467 zcUniversalDifferential C psi.toMonoidHom g) :
468 letI : TopologicalSpace
469 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
470 closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
471 (G := G) (H := H) C psi family hfree htarget hφconv
472 hH hφHconv hφHgen hfundamental
473 Continuous
474 (fun p :
475 ZCCompletedGroupAlgebra C H ×
476 ZCCompletedDifferentialModule C psi.toMonoidHom =>
477 p.1 • p.2) := by
478 letI : TopologicalSpace
479 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
480 closedGeneratedDerivativeCoordinateTopologyProCInteger_of_fundamental_formula
481 (G := G) (H := H) C psi family hfree htarget hφconv
482 hH hφHconv hφHgen hfundamental
483 let e :=
484 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
485 (G := G) (H := H) C psi family hfree htarget hφconv
486 hH hφHconv hφHgen hfundamental
487 have he : Continuous (e :
488 ZCCompletedDifferentialModule C psi.toMonoidHom →
489 ZCFreeFoxCoordinates C (X := X) (H := H)) := by
490 simpa [e] using
491 (continuous_closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula
492 (G := G) (H := H) C psi family hfree htarget hφconv
493 hH hφHconv hφHgen hfundamental)
494 rw [continuous_induced_rng]
495 change Continuous
496 (fun p :
497 ZCCompletedGroupAlgebra C H ×
498 ZCCompletedDifferentialModule C psi.toMonoidHom =>
499 e (p.1 • p.2))
500 have hfst :
501 Continuous
502 (fun p : ZCCompletedGroupAlgebra C H ×
503 ZCCompletedDifferentialModule C psi.toMonoidHom => p.1) :=
504 continuous_fst
505 have hsnd :
506 Continuous
507 (fun p : ZCCompletedGroupAlgebra C H ×
508 ZCCompletedDifferentialModule C psi.toMonoidHom => e p.2) :=
509 he.comp continuous_snd
510 have hcont :
511 Continuous
512 (fun p : ZCCompletedGroupAlgebra C H ×
513 ZCCompletedDifferentialModule C psi.toMonoidHom =>
514 p.1 • e p.2) :=
515 hfst.smul hsnd
516 have hfun :
517 (fun p : ZCCompletedGroupAlgebra C H ×
518 ZCCompletedDifferentialModule C psi.toMonoidHom =>
519 e (p.1 • p.2)) =
520 (fun p : ZCCompletedGroupAlgebra C H ×
521 ZCCompletedDifferentialModule C psi.toMonoidHom =>
522 p.1 • e p.2) := by
523 funext p
524 exact map_smul e p.1 p.2
525 rw [hfun]
526 exact hcont
528end ClosedGeneratedCoordinateEquiv
530end
532end CrowellExactSequence