Source: ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.Derivative
1import ProCGroups.FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom
3/-!
4# Fox differential: completed — free pro-\(C\) — uniqueness — derivative
6The principal declarations in this module are:
8- `freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect`
9 Any continuous semidirect lift with the prescribed generator components has the canonical free
10 pro-\(C\) completed Fox derivative vector as its left component.
11- `freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential`
12 Continuous completed crossed differentials on a free pro-\(C\) source are uniquely determined by
13 their standard generator values, provided their semidirect graph is continuous.
14- `freeProCZCCompletedCrossedDifferential_ext`
15 Extensionality for continuous completed crossed differentials on a free pro-\(C\) source. The
16 continuity hypotheses are put on the associated semidirect homomorphisms, which is the form used
17 by the completed Fox construction before the target topology is fully structural.
18- `freeProCZCCompletedFoxRightHom_eq_of_continuousCrossedDifferential`
19 The coefficient homomorphism of a continuous completed crossed differential agrees with the right
20 component of the canonical free pro-\(C\) semidirect lift.
21-/
23namespace FoxDifferential
25noncomputable section
27open ProCGroups.FreeProC
29universe u
32variable {C : ProCGroups.FiniteGroupClass.{u}}
33variable {X F H : Type u}
34variable [TopologicalSpace X]
35variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
36variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
37variable [DecidableEq X]
38variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
39variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
40variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
42section ProfiniteTarget
44variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
45variable [T2Space (ZCCompletedFoxSemidirect C X H)]
46variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
48/--
49Any continuous semidirect lift with the prescribed generator components has the canonical free
50pro-\(C\) completed Fox derivative vector as its left component.
51-/
52theorem freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect
53 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
54 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
55 (φ : X → H)
56 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
57 (f : F →* ZCCompletedFoxSemidirect C X H)
58 (hf : Continuous f)
59 (hleft :
60 ∀ x : X, (f (ι x)).left =
61 Pi.single x (1 : ZCCompletedGroupAlgebra C H))
62 (hright : ∀ x : X, (f (ι x)).right = φ x) :
63 (fun g : F => (f g).left) =
64 freeProCZCCompletedFoxDerivativeVector
65 (C := C) hι htarget φ hφ := by
66 have hgenerator :
67 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x := by
68 intro x
69 apply ZCCompletedFoxSemidirect.ext
70 · exact hleft x
71 · exact hright x
72 have hf_eq := hι.lift_unique htarget
73 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ hf hgenerator
74 funext g
75 rw [hf_eq]
76 rfl
78/--
79Continuous completed crossed differentials on a free pro-\(C\) source are uniquely determined by
80their standard generator values, provided their semidirect graph is continuous.
81-/
82theorem freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential
83 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
84 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
85 (ψ : F →* H)
86 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
87 (ZCFreeFoxCoordinates C (X := X) (H := H)))
88 (hcontinuous :
89 Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
90 (X := X) ψ delta))
91 (hbasis :
92 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
93 (fun g : F => delta g) =
94 fun g : F =>
95 freeProCZCCompletedFoxDerivativeVector
96 (C := C) hι htarget (fun x : X => ψ (ι x))
97 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
98 (C := C) hι ψ delta hcontinuous hbasis) g := by
99 have hleft :
100 ∀ x : X,
101 (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
102 (X := X) ψ delta (ι x)).left =
103 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
104 intro x
105 exact hbasis x
106 have hright :
107 ∀ x : X,
108 (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
109 (X := X) ψ delta (ι x)).right = ψ (ι x) := by
110 intro x
111 rfl
112 have hunique := freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect
113 (C := C) hι htarget (fun x : X => ψ (ι x))
114 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
115 (C := C) hι ψ delta hcontinuous hbasis)
116 (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
117 (X := X) ψ delta)
118 hcontinuous hleft hright
119 simpa using hunique
121omit [DecidableEq X] in
122/--
123Extensionality for continuous completed crossed differentials on a free pro-\(C\) source. The
124continuity hypotheses are put on the associated semidirect homomorphisms, which is the form used
125by the completed Fox construction before the target topology is fully structural.
126-/
127theorem freeProCZCCompletedCrossedDifferential_ext
128 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
129 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
130 (ψ : F →* H)
131 (delta epsilon :
132 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
133 (ZCFreeFoxCoordinates C (X := X) (H := H)))
134 (hdelta_continuous :
135 Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
136 (X := X) ψ delta))
137 (hepsilon_continuous :
138 Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
139 (X := X) ψ epsilon))
140 (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
141 delta = epsilon := by
142 let f : F →* ZCCompletedFoxSemidirect C X H :=
143 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
144 (X := X) ψ delta
145 let g : F →* ZCCompletedFoxSemidirect C X H :=
146 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
147 (X := X) ψ epsilon
148 have hfg : ∀ x : X, f (ι x) = g (ι x) := by
149 intro x
150 apply ZCCompletedFoxSemidirect.ext
151 · exact hbasis x
152 · rfl
153 have hsemidirect : f = g := hι.hom_ext htarget hdelta_continuous hepsilon_continuous hfg
154 apply CrossedHom.ext
155 intro a
156 exact congrArg
157 (fun q : F →* ZCCompletedFoxSemidirect C X H => (q a).left)
158 hsemidirect
160/--
161The coefficient homomorphism of a continuous completed crossed differential agrees with the
162right component of the canonical free pro-\(C\) semidirect lift.
163-/
164theorem freeProCZCCompletedFoxRightHom_eq_of_continuousCrossedDifferential
165 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
166 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
167 (ψ : F →* H)
168 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
169 (ZCFreeFoxCoordinates C (X := X) (H := H)))
170 (hcontinuous :
171 Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
172 (X := X) ψ delta))
173 (hbasis :
174 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
175 ψ =
176 freeProCZCCompletedFoxRightHom
177 (C := C) hι htarget (fun x : X => ψ (ι x))
178 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
179 (C := C) hι ψ delta hcontinuous hbasis) := by
180 apply MonoidHom.ext
181 intro g
182 have hgenerator :
183 ∀ x : X,
184 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
185 (X := X) ψ delta (ι x) =
186 freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)) x := by
187 intro x
188 apply ZCCompletedFoxSemidirect.ext
189 · exact hbasis x
190 · rfl
191 have hsemidirect := hι.lift_unique htarget
192 (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)))
193 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
194 (C := C) hι ψ delta hcontinuous hbasis)
195 (f := freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
196 (X := X) ψ delta)
197 hcontinuous hgenerator
198 change ψ g =
199 ((hι.lift htarget
200 (freeProCZCCompletedFoxSemidirectGenerator (C := C) (fun x : X => ψ (ι x)))
201 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
202 (C := C) hι ψ delta hcontinuous hbasis)) g).right
203 exact congrArg
204 (fun f : F →* ZCCompletedFoxSemidirect C X H => (f g).right) hsemidirect
206end ProfiniteTarget
208end
210end FoxDifferential