Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom
1import ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift
3/-!
4# Fox differential: completed — free pro-\(C\) — uniqueness — semidirect hom
6The principal declarations in this module are:
8- `freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential`
9 A completed crossed differential and its coefficient homomorphism combine into a semidirect
10 homomorphism.
11- `freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left`
12 The semidirect homomorphism attached to a crossed differential has \(\delta\) as its left
13 component.
14- `freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_right`
15 The semidirect homomorphism attached to a crossed differential has \(\psi\)s its right component.
16- `continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential`
17 If a crossed-differential semidirect homomorphism is continuous and has the standard generator
18 coordinates, then the corresponding semidirect generator map is continuous.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.FreeProC
27universe u
30variable {C : ProCGroups.FiniteGroupClass.{u}}
31variable {X F H : Type u}
32variable [TopologicalSpace X]
33variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
34variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
35variable [DecidableEq X]
36variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
37variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
38variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
40/--
41A completed crossed differential and its coefficient homomorphism combine into a semidirect
42homomorphism.
43-/
44def freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
45 (ψ : F →* H)
46 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
47 (ZCFreeFoxCoordinates C (X := X) (H := H))) :
48 F →* ZCCompletedFoxSemidirect C X H where
49 toFun g := { left := delta g, right := ψ g }
50 map_one' := by
51 apply ZCCompletedFoxSemidirect.ext
52 · exact delta.map_one
53 · simp only [map_one, ZCCompletedFoxSemidirect.one_right]
54 map_mul' g h := by
55 apply ZCCompletedFoxSemidirect.ext
56 · exact delta.map_mul g h
57 · simp only [map_mul, ZCCompletedFoxSemidirect.mul_right]
59omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] [DecidableEq X]
60 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
61 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
62/--
63The semidirect homomorphism attached to a crossed differential has \(\delta\) as its left
64component.
65-/
66@[simp]
67theorem freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_left
68 (ψ : F →* H)
69 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
70 (ZCFreeFoxCoordinates C (X := X) (H := H)))
71 (g : F) :
72 (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
73 (X := X) ψ delta g).left = delta g :=
74 rfl
76omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] [DecidableEq X]
77 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
78 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
79/--
80The semidirect homomorphism attached to a crossed differential has \(\psi\)s its right
81component.
82-/
83@[simp]
84theorem freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential_right
85 (ψ : F →* H)
86 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
87 (ZCFreeFoxCoordinates C (X := X) (H := H)))
88 (g : F) :
89 (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
90 (X := X) ψ delta g).right = ψ g :=
91 rfl
93omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
94/--
95If a crossed-differential semidirect homomorphism is continuous and has the standard generator
96coordinates, then the corresponding semidirect generator map is continuous.
97-/
98theorem continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
99 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
100 (ψ : F →* H)
101 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
102 (ZCFreeFoxCoordinates C (X := X) (H := H)))
103 (hcontinuous :
104 Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
105 (X := X) ψ delta))
106 (hbasis :
107 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
108 Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x))) := by
109 have hgenerator :
110 (fun x : X =>
111 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
112 (X := X) ψ delta (ι x)) =
113 freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)) := by
114 funext x
115 apply ZCCompletedFoxSemidirect.ext
116 · exact hbasis x
117 · rfl
118 rw [← hgenerator]
119 exact hcontinuous.comp hι.continuous_ι
122end
124end FoxDifferential