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

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

1import ProCGroups.FoxDifferential.Completed.Continuous.Free.Continuity
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Naturality
4/-!
5# Fox differential: completed — continuous — free — rules
7The principal declarations in this module are:
9- `freeProCZCCompletedFoxRightHomContinuousMonoidHom`
10 The right component of the completed free pro-\(C\) Fox lift is bundled as a continuous
11 homomorphism.
12- `freeProCZCCompletedFoxDerivativeVectorContinuousMap`
13 The completed free pro-\(C\) Fox derivative vector is bundled as a continuous map; it is a crossed
14 differential, not a homomorphism.
15- `freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom`
16 The bundled right homomorphism has the expected underlying monoid homomorphism.
17- `freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply`
18 Evaluation of the bundled right homomorphism.
19-/
21namespace FoxDifferential
23noncomputable section
25open scoped BigOperators
27universe u
29variable {C : ProCGroups.FiniteGroupClass.{u}}
30variable {X F H : Type u}
31variable [TopologicalSpace X] [DecidableEq X]
32variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
33variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
34variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36section FreeProCCompletedRules
38variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
39variable [T2Space (ZCCompletedFoxSemidirect C X H)]
40variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
42variable {ι : X → F}
43variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
44variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
45variable (φ : X → H)
46variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
48/--
49The right component of the completed free pro-\(C\) Fox lift is bundled as a continuous
50homomorphism.
51-/
52def freeProCZCCompletedFoxRightHomContinuousMonoidHom : F →ₜ* H where
53 toMonoidHom := freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ
54 continuous_toFun :=
55 continuous_freeProCZCCompletedFoxRightHom (C := C) X H hι htarget φ hφ
57/-- The bundled right homomorphism has the expected underlying monoid homomorphism. -/
58@[simp]
59theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_toMonoidHom :
60 (freeProCZCCompletedFoxRightHomContinuousMonoidHom
61 (C := C) hι htarget φ hφ).toMonoidHom =
62 freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ :=
63 rfl
65/-- Evaluation of the bundled right homomorphism. -/
66@[simp]
67theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply (g : F) :
68 freeProCZCCompletedFoxRightHomContinuousMonoidHom
69 (C := C) hι htarget φ hφ g =
70 freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ g :=
71 rfl
73/-- The bundled right homomorphism has the prescribed generator values. -/
74@[simp]
75theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_generator (x : X) :
76 freeProCZCCompletedFoxRightHomContinuousMonoidHom
77 (C := C) hι htarget φ hφ (ι x) = φ x := by
78 exact freeProCZCCompletedFoxRightHom_generator (C := C) hι htarget φ hφ x
80/--
81The completed free pro-\(C\) Fox derivative vector is bundled as a continuous map; it is a
82crossed differential, not a homomorphism.
83-/
84def freeProCZCCompletedFoxDerivativeVectorContinuousMap :
85 ContinuousMap F (ZCFreeFoxCoordinates C (X := X) (H := H)) where
86 toFun := freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ
87 continuous_toFun :=
88 continuous_freeProCZCCompletedFoxDerivativeVector (C := C) X H hι htarget φ hφ
90/-- Evaluation of the bundled continuous completed Fox derivative vector. -/
91@[simp]
92theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_apply (g : F) :
93 freeProCZCCompletedFoxDerivativeVectorContinuousMap
94 (C := C) hι htarget φ hφ g =
95 freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ g :=
96 rfl
98/-- The bundled continuous completed Fox derivative vector has the prescribed generator values. -/
99@[simp]
100theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_generator (x : X) :
101 freeProCZCCompletedFoxDerivativeVectorContinuousMap
102 (C := C) hι htarget φ hφ (ι x) =
103 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
104 simp only [freeProCZCCompletedFoxDerivativeVectorContinuousMap, ContinuousMap.coe_mk,
105 freeProCZCCompletedFoxDerivativeVector_generator]
107/--
108Restricting the continuous completed Fox derivative to the abstract free group generated by the
109chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
110-/
111theorem zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
112 (w : FreeGroup X) :
113 zcFreeGroupFoxDerivativeVector C
114 ((freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ).comp
115 (FreeGroup.lift ι)) w =
116 freeProCZCCompletedFoxDerivativeVector
117 (C := C) hι htarget φ hφ ((FreeGroup.lift ι) w) := by
118 let ρ : F →* H :=
119 freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ
120 let D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ρ)
121 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
122 freeProCZCCompletedFoxDerivativeVector (C := C) hι htarget φ hφ
123 let δ : ScalarCrossedHom
124 (zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
125 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
126 { toFun := fun w => D ((FreeGroup.lift ι) w)
127 map_mul' := by
128 intro u v
129 simp [ρ, D, map_mul, MonoidHom.comp_apply] }
130 have hbasis :
131 ∀ x : X, δ (FreeGroup.of x) =
132 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
133 intro x
134 change D ((FreeGroup.lift ι) (FreeGroup.of x)) =
135 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
136 rw [FreeGroup.lift_apply_of]
137 exact freeProCZCCompletedFoxDerivativeVector_generator
138 (C := C) hι htarget φ hφ x
139 have hδeq :
140 δ =
141 zcFreeGroupFoxDerivativeVector C
142 (ρ.comp (FreeGroup.lift ι)) :=
143 zcFreeGroupFoxDerivativeVector_unique
144 C (ρ.comp (FreeGroup.lift ι)) δ hbasis
145 exact congrArg
146 (fun d : ScalarCrossedHom
147 (zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
148 (ZCFreeFoxCoordinates C (X := X) (H := H)) => d w)
149 hδeq.symm
151/-- Source restriction and target naturality for the continuous completed Fox derivative. -/
152theorem zcFreeFoxDerivVec_eq_freeProCCompletedFoxDerivVec_comp_lift_mapTarget
154 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
155 (η : H →ₜ* K) (w : FreeGroup X) :
156 zcFreeGroupFoxDerivativeVector C
157 (η.toMonoidHom.comp
158 ((freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ).comp
159 (FreeGroup.lift ι))) w =
160 zcFreeFoxCoordinatesMap (X := X) C hC η
161 (freeProCZCCompletedFoxDerivativeVector
162 (C := C) hι htarget φ hφ ((FreeGroup.lift ι) w)) := by
163 rw [zcFreeGroupFoxDerivativeVector_mapTarget]
164 rw [zcFreeGroupFoxDerivativeVector_eq_freeProCCompletedFoxDerivativeVector_comp_lift
165 (C := C) hι htarget φ hφ w]
167end FreeProCCompletedRules
169section FreeProCConvergingSetCompletedRules
171variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
172variable [T2Space (ZCCompletedFoxSemidirect C X H)]
173variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
175variable {ι : X → F}
176variable (hι :
178variable (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
179variable (φ : X → H)
180variable (hφconv :
182 (G := ZCCompletedFoxSemidirect C X H)
183 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
184variable (hφgen :
186 (G := ZCCompletedFoxSemidirect C X H)
187 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
189omit [TopologicalSpace X] in
190/--
191Restricting the converging-set continuous completed Fox derivative to the abstract free group
192generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
193-/
194theorem zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
195 (w : FreeGroup X) :
196 zcFreeGroupFoxDerivativeVector C
197 ((freeProCZCCompletedFoxRightHomOfConvergingSet
198 (C := C) hι htarget φ hφconv hφgen).comp
199 (FreeGroup.lift ι)) w =
200 freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
201 (C := C) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w) := by
202 let ρ : F →* H :=
203 freeProCZCCompletedFoxRightHomOfConvergingSet
204 (C := C) hι htarget φ hφconv hφgen
205 let D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ρ)
206 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
207 freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
208 (C := C) hι htarget φ hφconv hφgen
209 let δ : ScalarCrossedHom
210 (zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
211 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
212 { toFun := fun w => D ((FreeGroup.lift ι) w)
213 map_mul' := by
214 intro u v
215 simp [ρ, D, map_mul, MonoidHom.comp_apply] }
216 have hbasis :
217 ∀ x : X, δ (FreeGroup.of x) =
218 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
219 intro x
220 change D ((FreeGroup.lift ι) (FreeGroup.of x)) =
221 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
222 rw [FreeGroup.lift_apply_of]
223 exact freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator
224 (C := C) hι htarget φ hφconv hφgen x
225 have hδeq :
226 δ =
227 zcFreeGroupFoxDerivativeVector C
228 (ρ.comp (FreeGroup.lift ι)) :=
229 zcFreeGroupFoxDerivativeVector_unique
230 C (ρ.comp (FreeGroup.lift ι)) δ hbasis
231 exact congrArg
232 (fun d : ScalarCrossedHom
233 (zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
234 (ZCFreeFoxCoordinates C (X := X) (H := H)) => d w)
235 hδeq.symm
237omit [TopologicalSpace X] in
238/--
239Source restriction and target naturality for the converging-set continuous completed Fox
240derivative.
241-/
242theorem zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift_mapTarget
244 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
245 (η : H →ₜ* K) (w : FreeGroup X) :
246 zcFreeGroupFoxDerivativeVector C
247 (η.toMonoidHom.comp
248 ((freeProCZCCompletedFoxRightHomOfConvergingSet
249 (C := C) hι htarget φ hφconv hφgen).comp
250 (FreeGroup.lift ι))) w =
251 zcFreeFoxCoordinatesMap (X := X) C hC η
252 (freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
253 (C := C) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w)) := by
254 rw [zcFreeGroupFoxDerivativeVector_mapTarget]
255 rw [zcFreeFoxDerivVec_eq_freeProCDerivVecOfConvergingSet_comp_lift
256 (C := C) hι htarget φ hφconv hφgen w]
258end FreeProCConvergingSetCompletedRules
260section FreeProCClosedGeneratedCompletedRules
262variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
263variable [T2Space (ZCCompletedFoxSemidirect C X H)]
264variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
266variable {ι : X → F}
267variable (hι :
269variable (φ : X → H)
270variable (htarget :
272 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
273 (ZCCompletedFoxSemidirect C X H)))
274variable (hφconv :
276 (G :=
277 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
278 (ZCCompletedFoxSemidirect C X H)))
279 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
281omit [TopologicalSpace X] in
282/--
283Restricting the closed-generated continuous completed Fox derivative to the abstract free group
284generated by the chosen free pro-\(C\) basis recovers the completed free-group Fox derivative.
285-/
286theorem zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
287 (w : FreeGroup X) :
288 zcFreeGroupFoxDerivativeVector C
289 ((freeProCZCCompletedFoxRightHomViaClosedGenerated
290 (C := C) hι φ htarget hφconv).comp
291 (FreeGroup.lift ι)) w =
292 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
293 (C := C) hι φ htarget hφconv ((FreeGroup.lift ι) w) := by
294 let ρ : F →* H :=
295 freeProCZCCompletedFoxRightHomViaClosedGenerated
296 (C := C) hι φ htarget hφconv
297 let D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ρ)
298 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
299 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
300 (C := C) hι φ htarget hφconv
301 let δ : ScalarCrossedHom
302 (zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
303 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
304 { toFun := fun w => D ((FreeGroup.lift ι) w)
305 map_mul' := by
306 intro u v
307 simp [ρ, D, map_mul, MonoidHom.comp_apply] }
308 have hbasis :
309 ∀ x : X, δ (FreeGroup.of x) =
310 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
311 intro x
312 change D ((FreeGroup.lift ι) (FreeGroup.of x)) =
313 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
314 rw [FreeGroup.lift_apply_of]
315 exact freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
316 (C := C) hι φ htarget hφconv x
317 have hδeq :
318 δ =
319 zcFreeGroupFoxDerivativeVector C
320 (ρ.comp (FreeGroup.lift ι)) :=
321 zcFreeGroupFoxDerivativeVector_unique
322 C (ρ.comp (FreeGroup.lift ι)) δ hbasis
323 exact congrArg
324 (fun d : ScalarCrossedHom
325 (zcCompletedGroupAlgebraScalar C (ρ.comp (FreeGroup.lift ι)))
326 (ZCFreeFoxCoordinates C (X := X) (H := H)) => d w)
327 hδeq.symm
329omit [TopologicalSpace X] in
330/--
331Source restriction and target naturality for the closed-generated continuous completed Fox
332derivative.
333-/
334theorem zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift_mapTarget
336 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
337 (η : H →ₜ* K) (w : FreeGroup X) :
338 zcFreeGroupFoxDerivativeVector C
339 (η.toMonoidHom.comp
340 ((freeProCZCCompletedFoxRightHomViaClosedGenerated
341 (C := C) hι φ htarget hφconv).comp
342 (FreeGroup.lift ι))) w =
343 zcFreeFoxCoordinatesMap (X := X) C hC η
344 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
345 (C := C) hι φ htarget hφconv ((FreeGroup.lift ι) w)) := by
346 rw [zcFreeGroupFoxDerivativeVector_mapTarget]
347 rw [zcFreeFoxDerivVec_eq_freeProCDerivVecViaClosedGen_comp_lift
348 (C := C) hι φ htarget hφconv w]
350end FreeProCClosedGeneratedCompletedRules
352end
354end FoxDifferential