Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift
ProCGroups/FoxDifferential/Completed/FreeProC/SemidirectLift/Source

Source: ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectLift

1import ProCGroups.FoxDifferential.Completed.Semidirect
2import ProCGroups.FreeProC.Basic
4/-!
5# Fox differential: completed — free pro-\(C\) — semidirect lift
7The principal declarations in this module are:
9- `freeProCZCCompletedFoxSemidirectGenerator`
10 The generator map into the completed Fox semidirect target attached to a basis-value map
11 \(\varphi: X \to H\).
12- `freeProCZCCompletedFoxSemidirectClosedGeneratedTarget`
13 The closed subgroup of the completed Fox semidirect target generated by the Fox graph generators.
14- `freeProCZCCompletedFoxSemidirectGenerator_left`
15 The generator map has the expected left coordinate.
16- `freeProCZCCompletedFoxSemidirectGenerator_right`
17 The generator map has the expected right coordinate.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.FreeProC
26universe u
29variable {C : ProCGroups.FiniteGroupClass.{u}}
30variable {X F H : Type u}
31variable [TopologicalSpace X]
32variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
33variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
34variable [DecidableEq X]
35variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36variable [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
37variable [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)]
39/--
40The generator map into the completed Fox semidirect target attached to a basis-value map
41\(\varphi: X \to H\).
42-/
43def freeProCZCCompletedFoxSemidirectGenerator (φ : X → H) :
44 X → ZCCompletedFoxSemidirect C X H :=
45 fun x =>
46 { left := Pi.single x (1 : ZCCompletedGroupAlgebra C H)
47 right := φ x }
49omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
50 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
51/-- The generator map has the expected left coordinate. -/
52@[simp]
53theorem freeProCZCCompletedFoxSemidirectGenerator_left
54 (φ : X → H) (x : X) :
55 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x).left =
56 Pi.single x (1 : ZCCompletedGroupAlgebra C H) :=
57 rfl
59omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
60 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
61/-- The generator map has the expected right coordinate. -/
62@[simp]
63theorem freeProCZCCompletedFoxSemidirectGenerator_right
64 (φ : X → H) (x : X) :
65 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x).right = φ x :=
66 rfl
68omit [TopologicalSpace X]
69 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
70/--
71For a finite generator set, the completed Fox semidirect generator map automatically converges
72to \(1\).
73-/
74theorem freeProCZCCompletedFoxSemidirectGenerator_convergesToOneAlongOpenSubgroups_of_finite
75 [Finite X] (φ : X → H) :
76 FamilyConvergesToOneAlongOpenSubgroups
77 (G := ZCCompletedFoxSemidirect C X H)
78 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) := by
79 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain
80 (G := ZCCompletedFoxSemidirect C X H)
81 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
83omit [TopologicalSpace X] in
84/--
85The closed subgroup of the completed Fox semidirect target generated by the Fox graph
86generators.
87-/
88def freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (φ : X → H) :
89 ClosedSubgroup (ZCCompletedFoxSemidirect C X H) :=
91 (G := ZCCompletedFoxSemidirect C X H)
92 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
94omit [TopologicalSpace X] in
95/-- If the ambient completed Fox semidirect target has an open-normal \(C\)-basis, then so does the
96closed target generated by the Fox graph generators, by closed-subgroup permanence. -/
97theorem freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_hasOpenNormalBasisInClass
100 (hAmbient :
101 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
102 (φ : X → H) :
104 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
105 (C := C) φ : Subgroup
106 (ZCCompletedFoxSemidirect C X H)) :=
108 hForm.isomClosed hHer.subgroupClosed hAmbient
109 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ)
111omit [TopologicalSpace X] in
112/-- The Fox graph generator map, with codomain restricted to the closed subgroup it generates. -/
113def freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (φ : X → H) :
114 X →
115 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
116 (C := C) φ : Subgroup
117 (ZCCompletedFoxSemidirect C X H)) :=
119 (G := ZCCompletedFoxSemidirect C X H)
120 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
122omit [TopologicalSpace X] in
123/--
124The closed-generated Fox semidirect generator has underlying value equal to the corresponding
125semidirect generator.
126-/
127@[simp]
128theorem freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val
129 (φ : X → H) (x : X) :
130 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ x :
131 ZCCompletedFoxSemidirect C X H) =
132 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
133 rfl
135omit [TopologicalSpace X] in
136/-- Each Fox graph generator belongs to the closed subgroup generated by the Fox graph. -/
137@[simp]
138theorem freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget
139 (φ : X → H) (x : X) :
140 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x ∈
141 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
142 (C := C) φ : Subgroup
143 (ZCCompletedFoxSemidirect C X H)) := by
144 simpa using
145 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ x).2
147omit [TopologicalSpace X] in
148/--
149The completed semidirect Fox graph of every abstract free-group word lies in the closed subgroup
150generated by the Fox graph generators.
151-/
152theorem zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget
153 (φ : X → H) (w : FreeGroup X) :
154 zcCompletedFoxSemidirectLift C (FreeGroup.lift φ) w ∈
155 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
156 (C := C) φ : Subgroup
157 (ZCCompletedFoxSemidirect C X H)) := by
158 induction w using FreeGroup.induction_on with
159 | C1 =>
160 simp only [map_one, one_mem]
161 | of x =>
162 have hpoint :
163 zcCompletedFoxSemidirectLift C
164 (FreeGroup.lift φ) (FreeGroup.of x) =
165 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x := by
166 simp only [zcCompletedFoxSemidirectLift, FreeGroup.lift_apply_of,
167 freeProCZCCompletedFoxSemidirectGenerator]
168 rw [hpoint]
169 exact
170 freeProCZCCompletedFoxSemidirectGenerator_mem_closedGeneratedTarget (C := C) φ x
171 | inv_of x hx =>
172 simpa [map_inv] using
173 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
174 (C := C) φ : Subgroup
175 (ZCCompletedFoxSemidirect C X H)).inv_mem hx
176 | mul u v hu hv =>
177 simpa [map_mul] using
178 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
179 (C := C) φ : Subgroup
180 (ZCCompletedFoxSemidirect C X H)).mul_mem hu hv
182omit [TopologicalSpace X] in
183/--
184Equivalently, the pair consisting of the completed free Fox derivative vector and the target
185word value belongs to the closed generated Fox graph.
186-/
187theorem freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
188 (φ : X → H) (w : FreeGroup X) :
189 ({ left :=
190 zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w,
191 right := FreeGroup.lift φ w } :
192 ZCCompletedFoxSemidirect C X H) ∈
193 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
194 (C := C) φ : Subgroup
195 (ZCCompletedFoxSemidirect C X H)) := by
196 simpa [zcCompletedFoxSemidirectLift_eq] using
197 zcCompletedFoxSemidirectLift_freeGroupLift_mem_closedGeneratedTarget
198 (C := C) φ w
200omit [TopologicalSpace X] in
201/--
202If an abstract free-group word maps trivially to the target group, its completed Fox derivative
203vector gives a genuine cycle point \((D w, 1)\) in the closed generated Fox graph.
204-/
205theorem freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel
206 (φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
207 ({ left :=
208 zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w,
209 right := (1 : H) } :
210 ZCCompletedFoxSemidirect C X H) ∈
211 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
212 (C := C) φ : Subgroup
213 (ZCCompletedFoxSemidirect C X H)) := by
214 simpa [hw] using
215 freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
216 (C := C) φ w
218omit [TopologicalSpace X] in
219/--
220The algebraic kernel-word cycle points in the completed Fox semidirect product. These are the
221points \((D w, 1)\) obtained from abstract free-group words whose target value is 1. The
222remaining density step for the completed Fox cycles is formulated using the closure of this set.
223-/
224def freeProCZCCompletedFoxSemidirectKernelCycleSet (φ : X → H) :
225 Set (ZCCompletedFoxSemidirect C X H) :=
226 { y | ∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
227 y =
228 ({ left :=
229 zcFreeGroupFoxDerivativeVector C
230 (FreeGroup.lift φ) w,
231 right := (1 : H) } :
232 ZCCompletedFoxSemidirect C X H) }
235omit [TopologicalSpace X] in
236/--
237The completed Fox boundary-cycle set inside the completed Fox semidirect product. Its points are
238exactly the pairs \((v,1)\) whose coordinate vector is killed by the source-shaped completed Fox
239boundary. The remaining density step can be expressed as saying that this boundary-cycle set is
240contained in the closure of the algebraic kernel-word cycle set.
241-/
242def freeProCZCCompletedFoxSemidirectBoundaryCycleSet [Fintype X] (φ : X → H) :
243 Set (ZCCompletedFoxSemidirect C X H) :=
244 { y | y.right = 1 ∧
245 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) y.left = 0 }
247omit [TopologicalSpace X]
248 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
249 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
250/--
251The genuine completed Fox graph point \((D w, \varphi(w))\) attached to an abstract free-group
252word.
253-/
254def freeProCZCCompletedFoxSemidirectGraphWordPoint (φ : X → H) (w : FreeGroup X) :
255 ZCCompletedFoxSemidirect C X H :=
256 { left :=
257 zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w,
258 right := FreeGroup.lift φ w }
260omit [TopologicalSpace X]
261 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
262 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
263/--
264The left component of a semidirect graph-word point is the completed free-group Fox derivative
265vector of the word.
266-/
267@[simp]
268theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_left
269 (φ : X → H) (w : FreeGroup X) :
270 (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w).left =
271 zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w :=
272 rfl
274omit [TopologicalSpace X]
275 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
276 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
277/--
278The right component of a semidirect graph-word point is \(\mathrm{FreeGroup.lift}(\varphi)(w)\).
279-/
280@[simp]
281theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_right
282 (φ : X → H) (w : FreeGroup X) :
283 (freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w).right =
284 FreeGroup.lift φ w :=
285 rfl
287omit [TopologicalSpace X]
288 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
289 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
290/-- The set of all completed Fox graph points attached to abstract free-group words. -/
291def freeProCZCCompletedFoxSemidirectGraphWordSet (φ : X → H) :
292 Set (ZCCompletedFoxSemidirect C X H) :=
293 { y | ∃ w : FreeGroup X,
294 y = freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w }
296omit [TopologicalSpace X]
297 [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
298 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
299/--
300Membership in the completed Fox semidirect graph word set is equivalent to the displayed
301coordinate condition.
302-/
303theorem mem_freeProCZCCompletedFoxSemidirectGraphWordSet_iff
304 {φ : X → H}
305 {y : ZCCompletedFoxSemidirect C X H} :
306 y ∈ freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ ↔
307 ∃ w : FreeGroup X,
308 y = freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w := by
309 rfl
311omit [TopologicalSpace X] in
312/--
313Every completed graph-word point lies in the closed subgroup generated by the Fox graph
314generators.
315-/
316theorem freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget
317 (φ : X → H) (w : FreeGroup X) :
318 freeProCZCCompletedFoxSemidirectGraphWordPoint (C := C) φ w ∈
319 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
320 (C := C) φ : Subgroup
321 (ZCCompletedFoxSemidirect C X H)) := by
322 simpa [freeProCZCCompletedFoxSemidirectGraphWordPoint] using
323 freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec
324 (C := C) φ w
326omit [TopologicalSpace X] in
327/-- The graph-word set lies in the closed subgroup generated by the Fox graph generators. -/
328theorem freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget
329 (φ : X → H) :
330 freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ ⊆
331 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
332 (C := C) φ : Subgroup
333 (ZCCompletedFoxSemidirect C X H)) : Set
334 (ZCCompletedFoxSemidirect C X H)) := by
335 rintro y ⟨w, rfl⟩
336 exact freeProCZCCompletedFoxSemidirectGraphWordPoint_mem_closedGeneratedTarget
337 (C := C) φ w
339omit [TopologicalSpace X] in
340/-- The closure of the graph-word set remains in the closed generated Fox graph target. -/
341theorem closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget
342 (φ : X → H) :
343 closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ) ⊆
344 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
345 (C := C) φ : Subgroup
346 (ZCCompletedFoxSemidirect C X H)) : Set
347 (ZCCompletedFoxSemidirect C X H)) :=
348 closure_minimal
349 (freeProCZCCompletedFoxSemidirectGraphWordSet_subset_closedGeneratedTarget
350 (C := C) φ)
351 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ).isClosed'
353omit [TopologicalSpace X] in
354/--
355Graph-word density places every completed boundary cycle in the closed generated Fox graph
356target.
357-/
358theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_graphWord_density
359 [Fintype X] (φ : X → H)
360 (hdensity :
361 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
362 closure (freeProCZCCompletedFoxSemidirectGraphWordSet (C := C) φ)) :
363 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
364 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
365 (C := C) φ : Subgroup
366 (ZCCompletedFoxSemidirect C X H)) : Set
367 (ZCCompletedFoxSemidirect C X H)) := by
368 exact subset_trans hdensity
369 (closure_freeProCZCFoxSemiGraphWordSet_subset_closedGenTarget
370 (C := C) φ)
372omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
373 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
374/--
375A kernel word has zero completed Fox boundary. This is the completed Fox fundamental formula
376applied before taking closures: if \(w\) maps to \(1\), then the Euler boundary of its Fox
377derivative vector is zero.
378-/
379theorem zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel
380 [Fintype X] (φ : X → H) {w : FreeGroup X}
381 (hw : FreeGroup.lift φ w = 1) :
382 zcFreeGroupFoxBoundary C (FreeGroup.lift φ)
383 (zcFreeGroupFoxDerivativeVector C (FreeGroup.lift φ) w) = 0 := by
384 rw [zcFreeGroupFoxBoundary_derivativeVector]
385 exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
386 (C := C) (ψ := FreeGroup.lift φ) hw
388omit [TopologicalSpace X] in
389omit [TopologicalSpace (ZCCompletedFoxSemidirect C X H)] [IsTopologicalGroup
390 (ZCCompletedFoxSemidirect C X H)] in
391/-- Every algebraic kernel-word cycle point is an actual completed Fox boundary cycle. -/
392theorem freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
393 [Fintype X] (φ : X → H) :
394 freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ⊆
395 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ := by
396 intro y hy
397 rcases hy with ⟨w, hw, rfl⟩
398 constructor
399 · rfl
400 · exact zcFreeGroupFoxBoundary_zcFreeGroupFoxDerivativeVector_of_kernel
401 (C := C) φ hw
403omit [TopologicalSpace X] in
404/--
405The boundary-cycle points form an actual subgroup of the completed Fox semidirect product.
406Algebraically this is the additive kernel of the source-shaped completed Fox boundary, embedded
407as the right-trivial subgroup \((v,1)\).
408-/
409def freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
410 [Fintype X] (φ : X → H) :
411 Subgroup (ZCCompletedFoxSemidirect C X H) where
412 carrier := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ
413 one_mem' := by
414 constructor
415 · rfl
416 · simp only [ZCCompletedFoxSemidirect.one_left, map_zero]
417 mul_mem' := by
418 intro a b ha hb
419 rcases ha with ⟨ha_right, ha_boundary⟩
420 rcases hb with ⟨hb_right, hb_boundary⟩
421 constructor
422 · simp only [ZCCompletedFoxSemidirect.mul_right, ha_right, hb_right, mul_one]
423 · calc
424 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) (a * b).left
425 = zcFreeGroupFoxBoundary C (FreeGroup.lift φ)
426 (a.left + b.left) := by
427 simp only [ZCCompletedFoxSemidirect.mul_left, ha_right, map_one, one_smul, map_add]
428 _ = zcFreeGroupFoxBoundary C (FreeGroup.lift φ) a.left +
429 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) b.left := by
430 rw [map_add]
431 _ = 0 := by
432 simp only [ha_boundary, hb_boundary, add_zero]
433 inv_mem' := by
434 intro a ha
435 rcases ha with ⟨ha_right, ha_boundary⟩
436 constructor
437 · simp only [ZCCompletedFoxSemidirect.inv_right, ha_right, inv_one]
438 · calc
439 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) a⁻¹.left
440 = zcFreeGroupFoxBoundary C (FreeGroup.lift φ) (-a.left) := by
441 simp only [ZCCompletedFoxSemidirect.inv_left, ha_right, inv_one, map_one,
442 one_smul, map_neg]
443 _ = -zcFreeGroupFoxBoundary C (FreeGroup.lift φ) a.left := by
444 rw [map_neg]
445 _ = 0 := by
446 simp only [ha_boundary, neg_zero]
448omit [TopologicalSpace X] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect C X H)]
449 [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
450/--
451The \(\mathbb{Z}_C\)-completed differential-module boundary is the finite-stage boundary
452obtained from the source and target coordinates.
453-/
454@[simp]
455theorem freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup_coe
456 [Fintype X] (φ : X → H) :
457 ((freeProCZCCompletedFoxSemidirectBoundaryCycleSubgroup
458 (C := C) φ : Subgroup
459 (ZCCompletedFoxSemidirect C X H)) : Set
460 (ZCCompletedFoxSemidirect C X H)) =
461 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ :=
462 rfl
464omit [TopologicalSpace X] [DecidableEq X] [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
465/--
466The completed Fox boundary-cycle set is closed whenever the two semidirect projections and the
467source-shaped completed Fox boundary are continuous. This is the topological half of the density
468frontier: algebraic kernel-word cycles stay inside actual boundary cycles after taking closure.
469-/
470theorem isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous
471 [Fintype X] [T1Space H]
472 [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
473 [T1Space (ZCCompletedGroupAlgebra C H)]
474 (φ : X → H)
475 (hleft :
476 Continuous
477 (fun y : ZCCompletedFoxSemidirect C X H => y.left))
478 (hright :
479 Continuous
480 (fun y : ZCCompletedFoxSemidirect C X H => y.right))
481 (hboundary :
482 Continuous
483 (zcFreeGroupFoxBoundary C (FreeGroup.lift φ))) :
484 IsClosed (freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ) := by
485 have hright_closed :
486 IsClosed
487 ((fun y : ZCCompletedFoxSemidirect C X H => y.right) ⁻¹'
488 ({1} : Set H)) :=
489 isClosed_singleton.preimage hright
490 have hboundary_closed :
491 IsClosed
492 ((fun y : ZCCompletedFoxSemidirect C X H =>
493 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) y.left) ⁻¹'
494 ({0} : Set (ZCCompletedGroupAlgebra C H))) :=
495 isClosed_singleton.preimage (hboundary.comp hleft)
496 change IsClosed
497 (((fun y : ZCCompletedFoxSemidirect C X H => y.right) ⁻¹' ({1} : Set H)) ∩
498 ((fun y : ZCCompletedFoxSemidirect C X H =>
499 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) y.left) ⁻¹'
500 ({0} : Set (ZCCompletedGroupAlgebra C H))))
501 exact hright_closed.inter hboundary_closed
503omit [TopologicalSpace X] in
504omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
505/--
506Closure of algebraic kernel-word cycle points remains inside the actual completed Fox
507boundary-cycle set, assuming the displayed boundary-cycle set is topologically closed.
508-/
509theorem closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous
510 [Fintype X] [T1Space H]
511 [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
512 [T1Space (ZCCompletedGroupAlgebra C H)]
513 (φ : X → H)
514 (hleft :
515 Continuous
516 (fun y : ZCCompletedFoxSemidirect C X H => y.left))
517 (hright :
518 Continuous
519 (fun y : ZCCompletedFoxSemidirect C X H => y.right))
520 (hboundary :
521 Continuous
522 (zcFreeGroupFoxBoundary C (FreeGroup.lift φ))) :
523 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) ⊆
524 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ := by
525 exact
526 closure_minimal
527 (freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_boundaryCycleSet
528 (C := C) φ)
529 (isClosed_freeProCZCCompletedFoxSemidirectBoundaryCycleSet_of_continuous
530 (C := C) φ hleft hright hboundary)
532omit [TopologicalSpace X] in
533omit [IsTopologicalGroup (ZCCompletedFoxSemidirect C X H)] in
534/--
535With the continuity inputs in place, the remaining density statement is equivalently the claim
536that the closure of algebraic kernel-word cycle points is exactly the boundary-cycle set.
537-/
538theorem closure_freeProCZCFoxSemiKernelCycleSet_eq_boundaryCycleSet_iff_density
539 [Fintype X] [T1Space H]
540 [TopologicalSpace (ZCCompletedGroupAlgebra C H)]
541 [T1Space (ZCCompletedGroupAlgebra C H)]
542 {φ : X → H}
543 (hleft :
544 Continuous
545 (fun y : ZCCompletedFoxSemidirect C X H => y.left))
546 (hright :
547 Continuous
548 (fun y : ZCCompletedFoxSemidirect C X H => y.right))
549 (hboundary :
550 Continuous
551 (zcFreeGroupFoxBoundary C (FreeGroup.lift φ))) :
552 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) =
553 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ↔
554 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
555 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) := by
556 constructor
557 · intro h y hy
558 simpa [h] using hy
559 · intro hdensity
560 ext y
561 constructor
562 · intro hy
563 exact
564 closure_freeProCZCFoxSemiKernelCycleSet_subset_boundaryCycleSet_of_continuous
565 (C := C) φ hleft hright hboundary hy
566 · intro hy
567 exact hdensity hy
569omit [TopologicalSpace X] in
570/-- Every algebraic kernel-word cycle point lies in the closed generated Fox graph target. -/
571theorem freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget
572 (φ : X → H) :
573 freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ ⊆
574 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
575 (C := C) φ : Subgroup
576 (ZCCompletedFoxSemidirect C X H)) : Set
577 (ZCCompletedFoxSemidirect C X H)) := by
578 intro y hy
579 rcases hy with ⟨w, hw, rfl⟩
580 exact
581 freeProCZCFoxClosedGenTarget_mem_of_freeFoxDerivVec_kernel
582 (C := C) φ hw
584omit [TopologicalSpace X] in
585/--
586The closure of algebraic kernel-word cycle points is still contained in the closed generated Fox
587graph target.
588-/
589theorem closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
590 (φ : X → H) :
591 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ) ⊆
592 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
593 (C := C) φ : Subgroup
594 (ZCCompletedFoxSemidirect C X H)) : Set
595 (ZCCompletedFoxSemidirect C X H)) := by
596 exact
597 closure_minimal
598 (freeProCZCCompletedFoxSemidirectKernelCycleSet_subset_closedGeneratedTarget
599 (C := C) φ)
600 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ).isClosed'
602omit [TopologicalSpace X] in
603/--
604If the boundary-cycle set is dense in the algebraic kernel-word closure, then every completed
605Fox boundary cycle belongs to the closed subgroup generated by the Fox graph.
606-/
607theorem freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_density
608 [Fintype X] (φ : X → H)
609 (hdensity :
610 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
611 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)) :
612 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
613 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
614 (C := C) φ : Subgroup
615 (ZCCompletedFoxSemidirect C X H)) : Set
616 (ZCCompletedFoxSemidirect C X H)) := by
617 intro y hy
618 exact
619 closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
620 (C := C) φ (hdensity hy)
622omit [TopologicalSpace X] in
623/-- Pointwise form of the closure step for algebraic kernel-word cycle points. -/
624theorem freeProCZCFoxClosedGenTarget_mem_of_mem_closure_kernelCycleSet
625 (φ : X → H)
626 {y : ZCCompletedFoxSemidirect C X H}
627 (hy :
628 y ∈ closure
629 (freeProCZCCompletedFoxSemidirectKernelCycleSet (C := C) φ)) :
630 y ∈
631 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
632 (C := C) φ : Subgroup
633 (ZCCompletedFoxSemidirect C X H)) :=
634 closure_freeProCZCFoxSemiKernelCycleSet_subset_closedGenTarget
635 (C := C) φ hy
637omit [TopologicalSpace X] in
638/-- The restricted Fox graph generators topologically generate their closed generated target. -/
639theorem freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates
640 (φ : X → H) :
642 (G :=
643 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
644 (C := C) φ : Subgroup
645 (ZCCompletedFoxSemidirect C X H)))
646 (Set.range
647 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :=
649 (G := ZCCompletedFoxSemidirect C X H)
650 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
652omit [TopologicalSpace X] in
653/-- For a finite generator set, the restricted Fox graph generators converge to \(1\). -/
654theorem freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
655 [Finite X] (φ : X → H) :
656 FamilyConvergesToOneAlongOpenSubgroups
657 (G :=
658 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
659 (ZCCompletedFoxSemidirect C X H)))
660 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ) := by
661 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain
662 (G :=
663 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
664 (ZCCompletedFoxSemidirect C X H)))
665 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)
667section Lifts
669variable [CompactSpace (ZCCompletedFoxSemidirect C X H)]
670variable [T2Space (ZCCompletedFoxSemidirect C X H)]
671variable [TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H)]
673omit [TopologicalSpace X] in
674/--
675The completed Fox semidirect lift into the closed target generated by the graph generators. This
676is the converging-set version needed when the graph generators do not generate the whole
677semidirect product.
678-/
679def freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
680 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
681 (φ : X → H)
682 (htarget :
684 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
685 (ZCCompletedFoxSemidirect C X H)))
686 (hφconv :
687 FamilyConvergesToOneAlongOpenSubgroups
688 (G :=
689 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
690 (ZCCompletedFoxSemidirect C X H)))
691 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
692 F →*
693 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
694 (ZCCompletedFoxSemidirect C X H)) := by
695 letI : CompactSpace
696 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
697 (ZCCompletedFoxSemidirect C X H)) := by
698 exact
699 (show IsClosed
700 (((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
701 (C := C) φ : Subgroup (ZCCompletedFoxSemidirect C X H)) :
702 Set (ZCCompletedFoxSemidirect C X H))) from
703 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
704 (C := C) φ).isClosed').isClosedEmbedding_subtypeVal.compactSpace
705 exact hι.lift htarget
706 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)
707 hφconv
708 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates (C := C) φ)
710omit [TopologicalSpace X] in
711/-- Continuous homomorphism form of the closed-generated semidirect lift. -/
712def freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
713 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
714 (φ : X → H)
715 (htarget :
717 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
718 (ZCCompletedFoxSemidirect C X H)))
719 (hφconv :
720 FamilyConvergesToOneAlongOpenSubgroups
721 (G :=
722 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
723 (ZCCompletedFoxSemidirect C X H)))
724 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
725 F →ₜ*
726 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
727 (ZCCompletedFoxSemidirect C X H)) := by
728 letI : CompactSpace
729 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
730 (ZCCompletedFoxSemidirect C X H)) := by
731 exact
732 (show IsClosed
733 (((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
734 (C := C) φ : Subgroup (ZCCompletedFoxSemidirect C X H)) :
735 Set (ZCCompletedFoxSemidirect C X H))) from
736 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
737 (C := C) φ).isClosed').isClosedEmbedding_subtypeVal.compactSpace
738 exact hι.liftHom htarget
739 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)
740 hφconv
741 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates (C := C) φ)
743omit [TopologicalSpace X] in
744/--
745Forgetting continuity from the closed-generated semidirect lift homomorphism recovers the
746underlying closed-generated semidirect lift.
747-/
748@[simp]
749theorem freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_toMonoidHom
750 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
751 (φ : X → H)
752 (htarget :
754 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
755 (ZCCompletedFoxSemidirect C X H)))
756 (hφconv :
757 FamilyConvergesToOneAlongOpenSubgroups
758 (G :=
759 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
760 (ZCCompletedFoxSemidirect C X H)))
761 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
762 (freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
763 (C := C) hι φ htarget hφconv).toMonoidHom =
764 freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
765 (C := C) hι φ htarget hφconv :=
766 rfl
768omit [TopologicalSpace X] in
769/--
770The closed-generated semidirect lift sends each free pro-\(C\) generator to the corresponding
771closed-generated Fox semidirect generator.
772-/
773@[simp 900]
774theorem freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator
775 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
776 (φ : X → H)
777 (htarget :
779 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
780 (ZCCompletedFoxSemidirect C X H)))
781 (hφconv :
782 FamilyConvergesToOneAlongOpenSubgroups
783 (G :=
784 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
785 (ZCCompletedFoxSemidirect C X H)))
786 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
787 (x : X) :
788 freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
789 (C := C) hι φ htarget hφconv (ι x) =
790 freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ x := by
791 letI : CompactSpace
792 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
793 (ZCCompletedFoxSemidirect C X H)) := by
794 exact
795 (show IsClosed
796 (((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
797 (C := C) φ : Subgroup (ZCCompletedFoxSemidirect C X H)) :
798 Set (ZCCompletedFoxSemidirect C X H))) from
799 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
800 (C := C) φ).isClosed').isClosedEmbedding_subtypeVal.compactSpace
801 exact (hι.lift_spec htarget
802 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)
803 hφconv
804 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates (C := C)
805 φ)).2 x
807omit [TopologicalSpace X] in
808/--
809The closed-generated semidirect lift is surjective onto the closed target generated by the Fox
810graph generators. This is the mathematically valid replacement for the generally false claim
811that the Fox graph generators fill the whole completed semidirect product: the universal map
812from the free pro-\(C\) group is onto exactly the closed subgroup generated by those graph
813generators.
814-/
815theorem freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective
816 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
817 (φ : X → H)
818 [T2Space
819 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
820 (ZCCompletedFoxSemidirect C X H))]
821 (htarget :
823 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
824 (ZCCompletedFoxSemidirect C X H)))
825 (hφconv :
826 FamilyConvergesToOneAlongOpenSubgroups
827 (G :=
828 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
829 (ZCCompletedFoxSemidirect C X H)))
830 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
831 Function.Surjective
832 (freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
833 (C := C) hι φ htarget hφconv) := by
834 refine
836 (f := freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
837 (C := C) hι φ htarget hφconv)
838 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_topologicallyGenerates (C := C)
839 φ) ?_
840 rintro y ⟨x, rfl⟩
841 refine ⟨ι x, ?_⟩
842 change
843 freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
844 (C := C) hι φ htarget hφconv (ι x) =
845 freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ x
846 exact freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator
847 (C := C) hι φ htarget hφconv x
849omit [TopologicalSpace X] in
850/--
851The lift through the closed generated subgroup, composed with the inclusion into the full
852completed Fox semidirect product.
853-/
854def freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
855 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
856 (φ : X → H)
857 (htarget :
859 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
860 (ZCCompletedFoxSemidirect C X H)))
861 (hφconv :
862 FamilyConvergesToOneAlongOpenSubgroups
863 (G :=
864 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
865 (ZCCompletedFoxSemidirect C X H)))
866 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
867 F →* ZCCompletedFoxSemidirect C X H :=
868 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
869 (ZCCompletedFoxSemidirect C X H)).subtype.comp
870 (freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
871 (C := C) hι φ htarget hφconv)
873omit [TopologicalSpace X] in
874/--
875Elementwise form of the semidirect lift theorem, formulated in the ambient completed Fox
876semidirect product. Every element of the closed Fox graph target has a preimage under the free
877pro-\(C\) semidirect lift.
878-/
879theorem freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget
880 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
881 (φ : X → H)
882 [T2Space
883 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
884 (ZCCompletedFoxSemidirect C X H))]
885 (htarget :
887 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
888 (ZCCompletedFoxSemidirect C X H)))
889 (hφconv :
890 FamilyConvergesToOneAlongOpenSubgroups
891 (G :=
892 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
893 (ZCCompletedFoxSemidirect C X H)))
894 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
895 {y : ZCCompletedFoxSemidirect C X H}
896 (hy : y ∈
897 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
898 (ZCCompletedFoxSemidirect C X H))) :
899 ∃ g : F,
900 freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
901 (C := C) hι φ htarget hφconv g = y := by
902 let yclosed :
903 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
904 (ZCCompletedFoxSemidirect C X H)) :=
905 ⟨y, hy⟩
906 rcases
907 freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_surjective
908 (C := C) hι φ htarget hφconv yclosed with
909 ⟨g, hg⟩
910 change
911 (freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
912 (C := C) hι φ htarget hφconv).toMonoidHom g = yclosed at hg
913 rw [freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated_toMonoidHom] at hg
914 refine ⟨g, ?_⟩
915 simpa [freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated, yclosed] using
916 congrArg Subtype.val hg
918omit [TopologicalSpace X] in
919/--
920The closed-generated semidirect lift into the ambient semidirect product sends each free
921pro-\(C\) generator to the corresponding Fox semidirect generator.
922-/
923@[simp]
924theorem freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator
925 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
926 (φ : X → H)
927 (htarget :
929 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
930 (ZCCompletedFoxSemidirect C X H)))
931 (hφconv :
932 FamilyConvergesToOneAlongOpenSubgroups
933 (G :=
934 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
935 (ZCCompletedFoxSemidirect C X H)))
936 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
937 (x : X) :
938 freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
939 (C := C) hι φ htarget hφconv (ι x) =
940 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x := by
941 simp only [freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated, MonoidHom.coe_comp,
942 Subgroup.coe_subtype,
943 Function.comp_apply, freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator,
944 freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator_val]
946omit [TopologicalSpace X] in
947/-- The right component of the closed-generated semidirect lift. -/
948def freeProCZCCompletedFoxRightHomViaClosedGenerated
949 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
950 (φ : X → H)
951 (htarget :
953 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
954 (ZCCompletedFoxSemidirect C X H)))
955 (hφconv :
956 FamilyConvergesToOneAlongOpenSubgroups
957 (G :=
958 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
959 (ZCCompletedFoxSemidirect C X H)))
960 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
961 F →* H :=
962 (ZCCompletedFoxSemidirect.rightMonoidHom C X H).comp
963 (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
964 (C := C) hι φ htarget hφconv)
966omit [TopologicalSpace X] in
967/--
968The right component of the closed-generated semidirect lift sends each generator to its
969prescribed value \(\varphi(x)\).
970-/
971@[simp]
972theorem freeProCZCCompletedFoxRightHomViaClosedGenerated_generator
973 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
974 (φ : X → H)
975 (htarget :
977 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
978 (ZCCompletedFoxSemidirect C X H)))
979 (hφconv :
980 FamilyConvergesToOneAlongOpenSubgroups
981 (G :=
982 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
983 (ZCCompletedFoxSemidirect C X H)))
984 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
985 (x : X) :
986 freeProCZCCompletedFoxRightHomViaClosedGenerated
987 (C := C) hι φ htarget hφconv (ι x) = φ x := by
988 simp only [freeProCZCCompletedFoxRightHomViaClosedGenerated, MonoidHom.coe_comp,
989 Function.comp_apply,
990 freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator,
991 ZCCompletedFoxSemidirect.rightMonoidHom_apply,
992 freeProCZCCompletedFoxSemidirectGenerator_right]
994omit [TopologicalSpace X] in
995/-- The scalar crossed homomorphism given by the left component of the
996closed-generated semidirect lift. -/
997def freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
998 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
999 (φ : X → H)
1000 (htarget :
1002 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
1003 (ZCCompletedFoxSemidirect C X H)))
1004 (hφconv :
1005 FamilyConvergesToOneAlongOpenSubgroups
1006 (G :=
1007 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
1008 (ZCCompletedFoxSemidirect C X H)))
1009 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ)) :
1010 ScalarCrossedHom
1011 (zcCompletedGroupAlgebraScalar C
1012 (freeProCZCCompletedFoxRightHomViaClosedGenerated
1013 (C := C) hι φ htarget hφconv))
1014 (ZCFreeFoxCoordinates C (X := X) (H := H)) where
1015 toFun g :=
1016 (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
1017 (C := C) hι φ htarget hφconv g).left
1018 map_mul' g h := by
1019 have hmul := congrArg ZCCompletedFoxSemidirect.left
1020 (map_mul
1021 (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
1022 (C := C) hι φ htarget hφconv) g h)
1023 simpa only [ZCCompletedFoxSemidirect.mul_left,
1024 freeProCZCCompletedFoxRightHomViaClosedGenerated,
1025 scalarCrossedAction_apply, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp,
1026 Function.comp_apply, ZCCompletedFoxSemidirect.rightMonoidHom_apply] using hmul
1028omit [TopologicalSpace X] in
1029/--
1030The derivative-vector component of the closed-generated semidirect lift has standard basis value
1031at each generator.
1033@[simp]
1034theorem freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
1035 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1036 (φ : X → H)
1037 (htarget :
1039 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
1040 (ZCCompletedFoxSemidirect C X H)))
1041 (hφconv :
1042 FamilyConvergesToOneAlongOpenSubgroups
1043 (G :=
1044 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (C := C) φ : Subgroup
1045 (ZCCompletedFoxSemidirect C X H)))
1046 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (C := C) φ))
1047 (x : X) :
1048 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1049 (C := C) hι φ htarget hφconv (ι x) =
1050 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1051 change
1052 (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
1053 (C := C) hι φ htarget hφconv (ι x)).left =
1054 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
1055 rw [freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator]
1056 rfl
1058/-- The continuous completed Fox semidirect lift from a free pro-\(C\) source. -/
1059def freeProCZCCompletedFoxSemidirectLift
1060 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1061 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1062 (φ : X → H)
1063 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1064 F →* ZCCompletedFoxSemidirect C X H :=
1065 hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ
1067/--
1068The continuous homomorphism form of the completed Fox semidirect lift from a free pro-\(C\)
1069source.
1071def freeProCZCCompletedFoxSemidirectLiftHom
1072 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1073 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1074 (φ : X → H)
1075 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1076 F →ₜ* ZCCompletedFoxSemidirect C X H :=
1077 hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ
1079/--
1080Forgetting continuity from the continuous semidirect lift gives the underlying semidirect lift.
1082@[simp]
1083theorem freeProCZCCompletedFoxSemidirectLiftHom_toMonoidHom
1084 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1085 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1086 (φ : X → H)
1087 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1088 (freeProCZCCompletedFoxSemidirectLiftHom
1089 (C := C) hι htarget φ hφ).toMonoidHom =
1090 freeProCZCCompletedFoxSemidirectLift
1091 (C := C) hι htarget φ hφ :=
1092 rfl
1094/-- The free pro-\(C\) semidirect lift is continuous. -/
1095theorem continuous_freeProCZCCompletedFoxSemidirectLift
1096 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1097 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1098 (φ : X → H)
1099 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1100 Continuous (freeProCZCCompletedFoxSemidirectLift
1101 (C := C) hι htarget φ hφ) :=
1102 (freeProCZCCompletedFoxSemidirectLiftHom
1103 (C := C) hι htarget φ hφ).continuous_toFun
1105/-- The free pro-\(C\) semidirect lift has the prescribed completed Fox generator values. -/
1106@[simp]
1107theorem freeProCZCCompletedFoxSemidirectLift_generator
1108 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1109 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1110 (φ : X → H)
1111 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1112 (x : X) :
1113 freeProCZCCompletedFoxSemidirectLift
1114 (C := C) hι htarget φ hφ (ι x) =
1115 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
1116 (hι.lift_spec htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ).2 x
1118/-- The continuous semidirect lift has the prescribed completed Fox generator values. -/
1119@[simp]
1120theorem freeProCZCCompletedFoxSemidirectLiftHom_generator
1121 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1122 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1123 (φ : X → H)
1124 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1125 (x : X) :
1126 freeProCZCCompletedFoxSemidirectLiftHom
1127 (C := C) hι htarget φ hφ (ι x) =
1128 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
1129 hι.liftHom_apply htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ) hφ x
1131omit [TopologicalSpace X] in
1132/--
1133The completed Fox semidirect lift from a converging-set free pro-\(C\) source. The generator map
1134into the semidirect target is required to converge to \(1\) and topologically generate the
1135target, matching the universal property of a free pro-\(C\) group on a converging set.
1137def freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1138 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1139 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1140 (φ : X → H)
1141 (hφconv :
1142 FamilyConvergesToOneAlongOpenSubgroups
1143 (G := ZCCompletedFoxSemidirect C X H)
1144 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1145 (hφgen :
1147 (G := ZCCompletedFoxSemidirect C X H)
1148 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
1149 F →* ZCCompletedFoxSemidirect C X H :=
1150 hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
1151 hφconv hφgen
1153omit [TopologicalSpace X] in
1154/-- Continuous homomorphism form of the converging-set completed Fox semidirect lift. -/
1155def freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
1156 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1157 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1158 (φ : X → H)
1159 (hφconv :
1160 FamilyConvergesToOneAlongOpenSubgroups
1161 (G := ZCCompletedFoxSemidirect C X H)
1162 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1163 (hφgen :
1165 (G := ZCCompletedFoxSemidirect C X H)
1166 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
1167 F →ₜ* ZCCompletedFoxSemidirect C X H :=
1168 hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
1169 hφconv hφgen
1171omit [TopologicalSpace X] in
1172/--
1173Forgetting continuity from the converging-set semidirect lift homomorphism gives the unbundled
1174lift.
1176@[simp]
1177theorem freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_toMonoidHom
1178 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1179 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1180 (φ : X → H)
1181 (hφconv :
1182 FamilyConvergesToOneAlongOpenSubgroups
1183 (G := ZCCompletedFoxSemidirect C X H)
1184 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1185 (hφgen :
1187 (G := ZCCompletedFoxSemidirect C X H)
1188 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
1189 (freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
1190 (C := C) hι htarget φ hφconv hφgen).toMonoidHom =
1191 freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1192 (C := C) hι htarget φ hφconv hφgen :=
1193 rfl
1195omit [TopologicalSpace X] in
1196/-- The completed Fox semidirect lift associated to a converging generator family is continuous. -/
1197theorem continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1198 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1199 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1200 (φ : X → H)
1201 (hφconv :
1202 FamilyConvergesToOneAlongOpenSubgroups
1203 (G := ZCCompletedFoxSemidirect C X H)
1204 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1205 (hφgen :
1207 (G := ZCCompletedFoxSemidirect C X H)
1208 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
1209 Continuous (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1210 (C := C) hι htarget φ hφconv hφgen) :=
1211 (freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
1212 (C := C) hι htarget φ hφconv hφgen).continuous_toFun
1214omit [TopologicalSpace X] in
1215/-- The converging-set semidirect lift has the prescribed generator values. -/
1216@[simp]
1217theorem freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator
1218 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1219 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1220 (φ : X → H)
1221 (hφconv :
1222 FamilyConvergesToOneAlongOpenSubgroups
1223 (G := ZCCompletedFoxSemidirect C X H)
1224 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1225 (hφgen :
1227 (G := ZCCompletedFoxSemidirect C X H)
1228 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
1229 (x : X) :
1230 freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1231 (C := C) hι htarget φ hφconv hφgen (ι x) =
1232 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
1233 (hι.lift_spec htarget (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)
1234 hφconv hφgen).2 x
1236omit [TopologicalSpace X] in
1237/--
1238The converging-set semidirect lift is surjective once its prescribed generator values
1239topologically generate the semidirect target.
1241theorem freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet_surjective
1242 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1243 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1244 (φ : X → H)
1245 (hφconv :
1246 FamilyConvergesToOneAlongOpenSubgroups
1247 (G := ZCCompletedFoxSemidirect C X H)
1248 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1249 (hφgen :
1251 (G := ZCCompletedFoxSemidirect C X H)
1252 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
1253 Function.Surjective
1254 (freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
1255 (C := C) hι htarget φ hφconv hφgen) := by
1256 refine
1258 (f := freeProCZCCompletedFoxSemidirectLiftHomOfConvergingSet
1259 (C := C) hι htarget φ hφconv hφgen)
1260 hφgen ?_
1261 rintro y ⟨x, rfl⟩
1262 refine ⟨ι x, ?_⟩
1263 change
1264 freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1265 (C := C) hι htarget φ hφconv hφgen (ι x) =
1266 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x
1267 exact freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator
1268 (C := C) hι htarget φ hφconv hφgen x
1270omit [TopologicalSpace X] in
1271/-- The right component of the converging-set semidirect lift. -/
1272def freeProCZCCompletedFoxRightHomOfConvergingSet
1273 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1274 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1275 (φ : X → H)
1276 (hφconv :
1277 FamilyConvergesToOneAlongOpenSubgroups
1278 (G := ZCCompletedFoxSemidirect C X H)
1279 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1280 (hφgen :
1282 (G := ZCCompletedFoxSemidirect C X H)
1283 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
1284 F →* H :=
1285 (ZCCompletedFoxSemidirect.rightMonoidHom C X H).comp
1286 (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1287 (C := C) hι htarget φ hφconv hφgen)
1289omit [TopologicalSpace X] in
1290/-- The scalar crossed homomorphism given by the left component of the
1291converging-set semidirect lift. -/
1292def freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
1293 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1294 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1295 (φ : X → H)
1296 (hφconv :
1297 FamilyConvergesToOneAlongOpenSubgroups
1298 (G := ZCCompletedFoxSemidirect C X H)
1299 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1300 (hφgen :
1302 (G := ZCCompletedFoxSemidirect C X H)
1303 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))) :
1304 ScalarCrossedHom
1305 (zcCompletedGroupAlgebraScalar C
1306 (freeProCZCCompletedFoxRightHomOfConvergingSet
1307 (C := C) hι htarget φ hφconv hφgen))
1308 (ZCFreeFoxCoordinates C (X := X) (H := H)) where
1309 toFun g :=
1310 (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1311 (C := C) hι htarget φ hφconv hφgen g).left
1312 map_mul' g h := by
1313 have hmul := congrArg ZCCompletedFoxSemidirect.left
1314 (map_mul
1315 (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1316 (C := C) hι htarget φ hφconv hφgen) g h)
1317 simpa only [ZCCompletedFoxSemidirect.mul_left,
1318 freeProCZCCompletedFoxRightHomOfConvergingSet,
1319 ZCCompletedFoxSemidirect.rightMonoidHom,
1320 scalarCrossedAction_apply, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp,
1321 MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply] using hmul
1323omit [TopologicalSpace X] in
1324/--
1325The right component of the converging-set semidirect lift sends each generator to its prescribed
1326value \(\varphi(x)\).
1328@[simp]
1329theorem freeProCZCCompletedFoxRightHomOfConvergingSet_generator
1330 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1331 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1332 (φ : X → H)
1333 (hφconv :
1334 FamilyConvergesToOneAlongOpenSubgroups
1335 (G := ZCCompletedFoxSemidirect C X H)
1336 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1337 (hφgen :
1339 (G := ZCCompletedFoxSemidirect C X H)
1340 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
1341 (x : X) :
1342 freeProCZCCompletedFoxRightHomOfConvergingSet
1343 (C := C) hι htarget φ hφconv hφgen (ι x) = φ x := by
1344 simp only [freeProCZCCompletedFoxRightHomOfConvergingSet, MonoidHom.coe_comp, Function.comp_apply,
1345 freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator,
1346 ZCCompletedFoxSemidirect.rightMonoidHom_apply,
1347 freeProCZCCompletedFoxSemidirectGenerator_right]
1349omit [TopologicalSpace X] in
1350/--
1351The derivative-vector component of the converging-set semidirect lift has standard basis value
1352at each generator.
1354@[simp]
1355theorem freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator
1356 {ι : X → F} (hι : IsEpimorphicallyFreeProCGroupOnConvergingSet (C := C) X F ι)
1357 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1358 (φ : X → H)
1359 (hφconv :
1360 FamilyConvergesToOneAlongOpenSubgroups
1361 (G := ZCCompletedFoxSemidirect C X H)
1362 (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1363 (hφgen :
1365 (G := ZCCompletedFoxSemidirect C X H)
1366 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)))
1367 (x : X) :
1368 freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
1369 (C := C) hι htarget φ hφconv hφgen (ι x) =
1370 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1371 change
1372 (freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
1373 (C := C) hι htarget φ hφconv hφgen (ι x)).left =
1374 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
1375 rw [freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator]
1376 rfl
1378section Categorical
1380/--
1381The categorical completed Fox semidirect lift from a free pro-\(C\) source is bundled as a
1382morphism in ProCGrp.
1384def freeProCZCCompletedFoxSemidirectLiftMorphism
1387 (ZCCompletedFoxSemidirect C X H))
1388 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1389 (φ : X → H)
1390 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1391 ProCGrp.of C (ProfiniteGrp.of F) hFC ⟶
1393 (ProfiniteGrp.of
1394 (ZCCompletedFoxSemidirect C X H))
1395 hTargetC :=
1396 CategoryTheory.ObjectProperty.homMk
1397 (ProfiniteGrp.ofHom
1398 (freeProCZCCompletedFoxSemidirectLiftHom
1399 (C := C) hι hTargetC φ hφ))
1401/--
1402The underlying continuous homomorphism of the categorical completed Fox semidirect lift is the
1403free pro-\(C\) continuous homomorphism supplied by liftHom.
1405@[simp]
1406theorem freeProCZCCompletedFoxSemidirectLiftMorphism_hom
1409 (ZCCompletedFoxSemidirect C X H))
1410 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1411 (φ : X → H)
1412 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1414 (freeProCZCCompletedFoxSemidirectLiftMorphism
1415 (C := C) hFC hTargetC hι φ hφ) =
1416 freeProCZCCompletedFoxSemidirectLiftHom
1417 (C := C) hι hTargetC φ hφ :=
1418 rfl
1420/--
1421The underlying homomorphism of the categorical completed Fox semidirect lift is the unbundled
1422completed Fox semidirect lift.
1424@[simp]
1425theorem freeProCZCCompletedFoxSemidirectLiftMorphism_hom_toMonoidHom
1428 (ZCCompletedFoxSemidirect C X H))
1429 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1430 (φ : X → H)
1431 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1433 (freeProCZCCompletedFoxSemidirectLiftMorphism
1434 (C := C) hFC hTargetC hι φ hφ)).toMonoidHom =
1435 freeProCZCCompletedFoxSemidirectLift
1436 (C := C) hι hTargetC φ hφ :=
1437 rfl
1439/-- The categorical completed Fox semidirect lift has the prescribed generator values. -/
1440@[simp]
1441theorem freeProCZCCompletedFoxSemidirectLiftMorphism_generator
1444 (ZCCompletedFoxSemidirect C X H))
1445 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1446 (φ : X → H)
1447 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1448 (x : X) :
1449 freeProCZCCompletedFoxSemidirectLiftMorphism
1450 (C := C) hFC hTargetC hι φ hφ (ι x) =
1451 freeProCZCCompletedFoxSemidirectGenerator (C := C) φ x :=
1452 freeProCZCCompletedFoxSemidirectLiftHom_generator
1453 (C := C) hι hTargetC φ hφ x
1455/--
1456The left component of the categorical completed Fox semidirect lift has the standard Fox
1457coordinate on each generator.
1459@[simp]
1460theorem freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator
1463 (ZCCompletedFoxSemidirect C X H))
1464 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1465 (φ : X → H)
1466 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1467 (x : X) :
1468 (freeProCZCCompletedFoxSemidirectLiftMorphism
1469 (C := C) hFC hTargetC hι φ hφ (ι x)).left =
1470 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1471 rw [freeProCZCCompletedFoxSemidirectLiftMorphism_generator]
1472 rfl
1474/--
1475The right component of the categorical completed Fox semidirect lift has the prescribed
1476generator value.
1478@[simp]
1479theorem freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator
1482 (ZCCompletedFoxSemidirect C X H))
1483 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1484 (φ : X → H)
1485 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1486 (x : X) :
1487 (freeProCZCCompletedFoxSemidirectLiftMorphism
1488 (C := C) hFC hTargetC hι φ hφ (ι x)).right = φ x := by
1489 rw [freeProCZCCompletedFoxSemidirectLiftMorphism_generator]
1490 rfl
1492end Categorical
1494/--
1495The left component of the free pro-\(C\) semidirect lift has the standard Fox coordinate on each
1496generator.
1498@[simp]
1499theorem freeProCZCCompletedFoxSemidirectLift_left_generator
1500 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1501 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1502 (φ : X → H)
1503 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1504 (x : X) :
1505 (freeProCZCCompletedFoxSemidirectLift
1506 (C := C) hι htarget φ hφ (ι x)).left =
1507 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1508 rw [freeProCZCCompletedFoxSemidirectLift_generator]
1509 rfl
1511/--
1512The left component of the continuous free pro-\(C\) semidirect lift has the standard Fox
1513coordinate on each generator.
1515@[simp]
1516theorem freeProCZCCompletedFoxSemidirectLiftHom_left_generator
1517 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1518 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1519 (φ : X → H)
1520 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1521 (x : X) :
1522 (freeProCZCCompletedFoxSemidirectLiftHom
1523 (C := C) hι htarget φ hφ (ι x)).left =
1524 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1525 rw [freeProCZCCompletedFoxSemidirectLiftHom_generator]
1526 rfl
1528/-- The right component of the free pro-\(C\) semidirect lift has the prescribed generator value. -/
1529@[simp]
1530theorem freeProCZCCompletedFoxSemidirectLift_right_generator
1531 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1532 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1533 (φ : X → H)
1534 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1535 (x : X) :
1536 (freeProCZCCompletedFoxSemidirectLift
1537 (C := C) hι htarget φ hφ (ι x)).right = φ x := by
1538 rw [freeProCZCCompletedFoxSemidirectLift_generator]
1539 rfl
1541/--
1542The right component of the continuous free pro-\(C\) semidirect lift has the prescribed
1543generator value.
1545@[simp]
1546theorem freeProCZCCompletedFoxSemidirectLiftHom_right_generator
1547 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1548 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1549 (φ : X → H)
1550 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1551 (x : X) :
1552 (freeProCZCCompletedFoxSemidirectLiftHom
1553 (C := C) hι htarget φ hφ (ι x)).right = φ x := by
1554 rw [freeProCZCCompletedFoxSemidirectLiftHom_generator]
1555 rfl
1557/-- The target-group component of the continuous completed Fox semidirect lift. -/
1558def freeProCZCCompletedFoxRightHom
1559 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1560 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1561 (φ : X → H)
1562 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1563 F →* H where
1564 toFun g := (freeProCZCCompletedFoxSemidirectLift
1565 (C := C) hι htarget φ hφ g).right
1566 map_one' := by
1567 simp only [map_one, ZCCompletedFoxSemidirect.one_right]
1568 map_mul' g h := by
1569 simp only [map_mul, ZCCompletedFoxSemidirect.mul_right]
1571/--
1572The right component of the continuous completed Fox semidirect lift is the associated
1573homomorphism.
1575@[simp]
1576theorem freeProCZCCompletedFoxRightHom_apply
1577 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1578 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1579 (φ : X → H)
1580 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1581 (g : F) :
1582 freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ g =
1583 (freeProCZCCompletedFoxSemidirectLift
1584 (C := C) hι htarget φ hφ g).right :=
1585 rfl
1587/-- The target-group component has the prescribed generator values. -/
1588@[simp]
1589theorem freeProCZCCompletedFoxRightHom_generator
1590 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1591 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1592 (φ : X → H)
1593 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1594 (x : X) :
1595 freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ (ι x) = φ x := by
1596 rw [freeProCZCCompletedFoxRightHom_apply,
1597 freeProCZCCompletedFoxSemidirectLift_right_generator]
1599/-- The completed Fox derivative is the scalar crossed homomorphism obtained from
1600the left component of the continuous free pro-\(C\) semidirect lift. -/
1601def freeProCZCCompletedFoxDerivativeVector
1602 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1603 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1604 (φ : X → H)
1605 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ)) :
1606 ScalarCrossedHom
1607 (zcCompletedGroupAlgebraScalar C
1608 (freeProCZCCompletedFoxRightHom (C := C) hι htarget φ hφ))
1609 (ZCFreeFoxCoordinates C (X := X) (H := H)) where
1610 toFun g :=
1611 (freeProCZCCompletedFoxSemidirectLift
1612 (C := C) hι htarget φ hφ g).left
1613 map_mul' g h := by
1614 have hmul := congrArg ZCCompletedFoxSemidirect.left
1615 (map_mul (freeProCZCCompletedFoxSemidirectLift
1616 (C := C) hι htarget φ hφ) g h)
1617 simpa only [ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHom,
1618 scalarCrossedAction_apply, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_mk,
1619 OneHom.coe_mk] using hmul
1621/--
1622The free pro-\(C\) completed Fox derivative vector has the standard coordinate value on
1623generators.
1625@[simp]
1626theorem freeProCZCCompletedFoxDerivativeVector_generator
1627 {ι : X → F} (hι : IsFreeProCGroup (C := C) ι)
1628 (htarget : ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H))
1629 (φ : X → H)
1630 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C := C) φ))
1631 (x : X) :
1632 freeProCZCCompletedFoxDerivativeVector
1633 (C := C) hι htarget φ hφ (ι x) =
1634 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1635 change (freeProCZCCompletedFoxSemidirectLift
1636 (C := C) hι htarget φ hφ (ι x)).left =
1637 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
1638 rw [freeProCZCCompletedFoxSemidirectLift_left_generator]
1640end Lifts
1642end
1644end FoxDifferential