FoxDifferential/Completed/FreeProC/SemidirectLift.lean
1import FoxDifferential.Completed.Semidirect
2import ProCGroups.FreeProC.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/FreeProC/SemidirectLift.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Free pro-C completed Fox calculus
15Free pro-C sources are treated through completed Fox derivatives, stage projections, density arguments, and semidirect lift formulas.
16-/
17namespace FoxDifferential
19noncomputable section
21open ProCGroups.FreeProC
23universe u
26variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
27variable {X F H : Type u}
28variable [TopologicalSpace X]
29variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
30variable [DecidableEq X]
31variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
33variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
35/-- The generator map into the completed Fox semidirect target attached to a basis-value map
36`φ : X -> H`. -/
37def freeProCZCCompletedFoxSemidirectGenerator (φ : X → H) :
38 X → ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
39 fun x =>
40 { left := Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
41 right := φ x }
43omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
44 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
45/-- The generator map has the expected left coordinate. -/
46@[simp]
48 (φ : X → H) (x : X) :
49 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x).left =
50 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :=
51 rfl
53omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
54 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
55/-- The generator map has the expected right coordinate. -/
56@[simp]
58 (φ : X → H) (x : X) :
59 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x).right = φ x :=
60 rfl
62omit [TopologicalSpace X]
63 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
64/-- For a finite generator set, the completed Fox semidirect generator map automatically
65converges to `1`. -/
67 [Finite X] (φ : X → H) :
69 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
70 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) := by
71 exact FamilyConvergesToOne.of_finite_domain
72 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
73 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
75omit [TopologicalSpace X] in
76/-- The closed subgroup of the completed Fox semidirect target generated by the Fox graph
77generators. -/
78def freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (φ : X → H) :
79 ClosedSubgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
81 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
82 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
84omit [TopologicalSpace X] in
85/-- If the ambient completed Fox semidirect target is a pro-`C` group, then the closed target
86generated by the Fox graph generators is pro-`C` by closed-subgroup permanence. -/
88 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
89 [ProC.DeterminedByFiniteQuotients]
90 [ProCGroups.ProC.ProCGroup ProC
91 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
92 (φ : X → H) :
95 (ProC := ProC) φ : Subgroup
96 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
98 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (ProC := ProC) φ)
100omit [TopologicalSpace X] in
101/-- Pro-`C` predicate form of
104 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
105 [ProC.DeterminedByFiniteQuotients]
106 [ProCGroups.ProC.ProCGroup ProC
107 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
108 (φ : X → H) :
109 ProC
110 (G :=
112 (ProC := ProC) φ : Subgroup
113 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))) :=
117omit [TopologicalSpace X] in
118/-- The Fox graph generator map, with codomain restricted to the closed subgroup it generates. -/
119def freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (φ : X → H) :
120 X →
122 (ProC := ProC) φ : Subgroup
123 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
125 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
126 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
128omit [TopologicalSpace X] in
129@[simp]
131 (φ : X → H) (x : X) :
132 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ x :
133 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) =
134 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
135 rfl
137omit [TopologicalSpace X] in
138/-- Each Fox graph generator belongs to the closed subgroup generated by the Fox graph. -/
139@[simp]
141 (φ : X → H) (x : X) :
142 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x ∈
144 (ProC := ProC) φ : Subgroup
145 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
146 simpa using
147 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ x).2
149omit [TopologicalSpace X] in
150/-- The completed semidirect Fox graph of every abstract free-group word lies in the closed
151subgroup generated by the Fox graph generators. -/
153 (φ : X → H) (w : FreeGroup X) :
154 zcCompletedFoxSemidirectLift ProC.finiteQuotientClass (FreeGroup.lift φ) w ∈
156 (ProC := ProC) φ : Subgroup
157 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
158 induction w using FreeGroup.induction_on with
159 | C1 =>
161 | of x =>
162 have hpoint :
163 zcCompletedFoxSemidirectLift ProC.finiteQuotientClass
164 (FreeGroup.lift φ) (FreeGroup.of x) =
165 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
166 simp only [zcCompletedFoxSemidirectLift, FreeGroup.lift_apply_of, freeProCZCCompletedFoxSemidirectGenerator]
167 rw [hpoint]
168 exact
170 (ProC := ProC) φ x
171 | inv_of x hx =>
172 simpa [map_inv] using
174 (ProC := ProC) φ : Subgroup
175 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)).inv_mem hx
176 | mul u v hu hv =>
179 (ProC := ProC) φ : Subgroup
180 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)).mul_mem hu hv
182omit [TopologicalSpace X] in
183/-- Equivalently, the pair consisting of the completed free Fox derivative vector and the target
184word value belongs to the closed generated Fox graph. -/
186 (φ : X → H) (w : FreeGroup X) :
187 ({ left :=
188 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
189 right := FreeGroup.lift φ w } :
190 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) ∈
192 (ProC := ProC) φ : Subgroup
193 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
194 simpa [zcCompletedFoxSemidirectLift_eq] using
196 (ProC := ProC) φ w
198omit [TopologicalSpace X] in
199/-- If an abstract free-group word maps trivially to the target group, its completed Fox
200derivative vector gives a genuine cycle point `(D w, 1)` in the closed generated Fox graph. -/
202 (φ : X → H) {w : FreeGroup X} (hw : FreeGroup.lift φ w = 1) :
203 ({ left :=
204 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
205 right := (1 : H) } :
206 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) ∈
208 (ProC := ProC) φ : Subgroup
209 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
210 simpa [hw] using
212 (ProC := ProC) φ w
214omit [TopologicalSpace X] in
215/-- The algebraic kernel-word cycle points in the completed Fox semidirect product.
217These are the points `(D w, 1)` obtained from abstract free-group words whose target value is
218`1`. The remaining density step for the completed Fox cycles is formulated using the closure of
219this set. -/
220def freeProCZCCompletedFoxSemidirectKernelCycleSet (φ : X → H) :
221 Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
222 { y | ∃ w : FreeGroup X, FreeGroup.lift φ w = 1 ∧
223 y =
224 ({ left :=
225 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
226 (FreeGroup.lift φ) w,
227 right := (1 : H) } :
228 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) }
231omit [TopologicalSpace X] in
232/-- The completed Fox boundary-cycle set inside the completed Fox semidirect product.
234Its points are exactly the pairs `(v, 1)` whose coordinate vector is killed by the source-shaped
235completed Fox boundary. The remaining density step can be stated as saying that this boundary
236cycle set is contained in the closure of the algebraic kernel-word cycle set. -/
237def freeProCZCCompletedFoxSemidirectBoundaryCycleSet [Fintype X] (φ : X → H) :
238 Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
239 { y | y.right = 1 ∧
240 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) y.left = 0 }
242/-! ## Graph-word points
244Finite quotient stages naturally produce words whose image is trivial only after applying the
246`(D w, φ(w))`, not the kernel-word point `(D w, 1)`.
247-/
249omit [TopologicalSpace X]
250 [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
251 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
252/-- The genuine completed Fox graph point `(D w, φ(w))` attached to an abstract free-group word. -/
253def freeProCZCCompletedFoxSemidirectGraphWordPoint (φ : X → H) (w : FreeGroup X) :
254 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
255 { left :=
256 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w,
257 right := FreeGroup.lift φ w }
259omit [TopologicalSpace X]
260 [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
261 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
262@[simp]
264 (φ : X → H) (w : FreeGroup X) :
265 (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w).left =
266 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w :=
267 rfl
269omit [TopologicalSpace X]
270 [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
271 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
272@[simp]
274 (φ : X → H) (w : FreeGroup X) :
275 (freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w).right =
276 FreeGroup.lift φ w :=
277 rfl
279omit [TopologicalSpace X]
280 [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
281 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
282/-- The set of all completed Fox graph points attached to abstract free-group words. -/
283def freeProCZCCompletedFoxSemidirectGraphWordSet (φ : X → H) :
284 Set (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
285 { y | ∃ w : FreeGroup X,
286 y = freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w }
288omit [TopologicalSpace X]
289 [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
290 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
292 (φ : X → H)
293 (y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :
294 y ∈ freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ ↔
295 ∃ w : FreeGroup X,
296 y = freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w := by
297 rfl
299omit [TopologicalSpace X] in
300/-- Every completed graph-word point lies in the closed subgroup generated by the Fox graph
301generators. -/
303 (φ : X → H) (w : FreeGroup X) :
304 freeProCZCCompletedFoxSemidirectGraphWordPoint (ProC := ProC) φ w ∈
306 (ProC := ProC) φ : Subgroup
307 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
308 simpa [freeProCZCCompletedFoxSemidirectGraphWordPoint] using
310 (ProC := ProC) φ w
312omit [TopologicalSpace X] in
313/-- The graph-word set lies in the closed subgroup generated by the Fox graph generators. -/
315 (φ : X → H) :
316 freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ ⊆
318 (ProC := ProC) φ : Subgroup
319 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
320 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
321 rintro y ⟨w, rfl⟩
323 (ProC := ProC) φ w
325omit [TopologicalSpace X] in
326/-- The closure of the graph-word set remains in the closed generated Fox graph target. -/
328 (φ : X → H) :
329 closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ) ⊆
331 (ProC := ProC) φ : Subgroup
332 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
333 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
334 closure_minimal
336 (ProC := ProC) φ)
337 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (ProC := ProC) φ).isClosed'
339omit [TopologicalSpace X] in
340/-- Graph-word density places every completed boundary cycle in the closed generated Fox graph
341target. -/
343 [Fintype X] (φ : X → H)
344 (hdensity :
345 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
346 closure (freeProCZCCompletedFoxSemidirectGraphWordSet (ProC := ProC) φ)) :
347 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
349 (ProC := ProC) φ : Subgroup
350 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
351 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
352 exact subset_trans hdensity
354 (ProC := ProC) φ)
356omit [TopologicalSpace X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
357/-- A kernel word has zero completed Fox boundary.
359This is the completed Fox fundamental formula applied before taking closures: if
360`w` maps to `1`, then the Euler boundary of its Fox derivative vector is zero. -/
362 [Fintype X] (φ : X → H) {w : FreeGroup X}
363 (hw : FreeGroup.lift φ w = 1) :
364 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ)
365 (zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass (FreeGroup.lift φ) w) = 0 := by
368 (C := ProC.finiteQuotientClass) (ψ := FreeGroup.lift φ) hw
370omit [TopologicalSpace X] in
371omit [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
372/-- Every algebraic kernel-word cycle point is an actual completed Fox boundary cycle. -/
374 [Fintype X] (φ : X → H) :
375 freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ ⊆
376 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ := by
377 intro y hy
378 rcases hy with ⟨w, hw, rfl⟩
379 constructor
380 · rfl
382 (ProC := ProC) φ hw
384omit [TopologicalSpace X] in
385/-- The boundary-cycle points form an honest subgroup of the completed Fox semidirect product.
387Algebraically this is the additive kernel of the source-shaped completed Fox boundary, embedded
388as the right-trivial subgroup `(v, 1)`. -/
390 [Fintype X] (φ : X → H) :
391 Subgroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) where
392 carrier := freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ
393 one_mem' := by
394 constructor
395 · rfl
397 mul_mem' := by
398 intro a b ha hb
399 rcases ha with ⟨ha_right, ha_boundary⟩
400 rcases hb with ⟨hb_right, hb_boundary⟩
401 constructor
402 · simp only [ZCCompletedFoxSemidirect.mul_right, ha_right, hb_right, mul_one]
403 · calc
404 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) (a * b).left
405 = zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ)
406 (a.left + b.left) := by
408 _ = zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) a.left +
409 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) b.left := by
411 _ = 0 := by
412 simp only [ha_boundary, hb_boundary, add_zero]
413 inv_mem' := by
414 intro a ha
415 rcases ha with ⟨ha_right, ha_boundary⟩
416 constructor
417 · simp only [ZCCompletedFoxSemidirect.inv_right, ha_right, inv_one]
418 · calc
419 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) a⁻¹.left
420 = zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) (-a.left) := by
422 _ = -zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) a.left := by
423 rw [map_neg]
424 _ = 0 := by
425 simp only [ha_boundary, neg_zero]
427omit [TopologicalSpace X] [DecidableEq X] [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
428@[simp]
430 [Fintype X] (φ : X → H) :
432 (ProC := ProC) φ : Subgroup
433 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
434 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) =
435 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ :=
436 rfl
438omit [TopologicalSpace X] [DecidableEq X] [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
439/-- The completed Fox boundary-cycle set is closed whenever the two semidirect projections and the
440source-shaped completed Fox boundary are continuous.
442This is the topological half of the density frontier: algebraic kernel-word cycles stay inside
443actual boundary cycles after taking closure. -/
445 [Fintype X] [T1Space H]
446 [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
447 [T1Space (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
448 (φ : X → H)
449 (hleft :
450 Continuous
451 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.left))
452 (hright :
453 Continuous
454 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.right))
455 (hboundary :
456 Continuous
457 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ))) :
458 IsClosed (freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ) := by
459 have hright_closed :
460 IsClosed
461 ((fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.right) ⁻¹'
462 ({1} : Set H)) :=
463 isClosed_singleton.preimage hright
464 have hboundary_closed :
465 IsClosed
466 ((fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H =>
467 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) y.left) ⁻¹'
468 ({0} : Set (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))) :=
469 isClosed_singleton.preimage (hboundary.comp hleft)
470 simpa [freeProCZCCompletedFoxSemidirectBoundaryCycleSet] using
471 hright_closed.inter hboundary_closed
473omit [TopologicalSpace X] in
474omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
475/-- Closure of algebraic kernel-word cycle points remains inside the actual completed Fox
476boundary-cycle set, assuming the displayed boundary-cycle set is topologically closed. -/
478 [Fintype X] [T1Space H]
479 [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
480 [T1Space (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
481 (φ : X → H)
482 (hleft :
483 Continuous
484 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.left))
485 (hright :
486 Continuous
487 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.right))
488 (hboundary :
489 Continuous
490 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ))) :
491 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) ⊆
492 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ := by
493 exact
494 closure_minimal
496 (ProC := ProC) φ)
498 (ProC := ProC) φ hleft hright hboundary)
500omit [TopologicalSpace X] in
501omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
502/-- With the continuity inputs in place, the remaining density statement is equivalently the
503claim that the closure of algebraic kernel-word cycle points is exactly the boundary-cycle set. -/
505 [Fintype X] [T1Space H]
506 [TopologicalSpace (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
507 [T1Space (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)]
508 (φ : X → H)
509 (hleft :
510 Continuous
511 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.left))
512 (hright :
513 Continuous
514 (fun y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => y.right))
515 (hboundary :
516 Continuous
517 (zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ))) :
518 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) =
519 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ↔
520 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
521 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) := by
522 constructor
523 · intro h y hy
524 simpa [h] using hy
525 · intro hdensity
526 ext y
527 constructor
528 · intro hy
529 exact
531 (ProC := ProC) φ hleft hright hboundary hy
532 · intro hy
533 exact hdensity hy
535omit [TopologicalSpace X] in
536/-- Every algebraic kernel-word cycle point lies in the closed generated Fox graph target. -/
538 (φ : X → H) :
539 freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ ⊆
541 (ProC := ProC) φ : Subgroup
542 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
543 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
544 intro y hy
545 rcases hy with ⟨w, hw, rfl⟩
546 exact
548 (ProC := ProC) φ hw
550omit [TopologicalSpace X] in
551/-- The closure of algebraic kernel-word cycle points is still contained in the closed generated
552Fox graph target. -/
554 (φ : X → H) :
555 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ) ⊆
557 (ProC := ProC) φ : Subgroup
558 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
559 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
560 exact
561 closure_minimal
563 (ProC := ProC) φ)
564 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget (ProC := ProC) φ).isClosed'
566omit [TopologicalSpace X] in
567/-- If the boundary-cycle set is dense in the algebraic kernel-word closure, then every completed
568Fox boundary cycle belongs to the closed subgroup generated by the Fox graph. -/
570 [Fintype X] (φ : X → H)
571 (hdensity :
572 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
573 closure (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)) :
574 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
576 (ProC := ProC) φ : Subgroup
577 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
578 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
579 intro y hy
580 exact
582 (ProC := ProC) φ (hdensity hy)
584omit [TopologicalSpace X] in
585/-- Pointwise form of the closure step for algebraic kernel-word cycle points. -/
587 (φ : X → H)
588 {y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
589 (hy :
590 y ∈ closure
591 (freeProCZCCompletedFoxSemidirectKernelCycleSet (ProC := ProC) φ)) :
592 y ∈
594 (ProC := ProC) φ : Subgroup
595 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
597 (ProC := ProC) φ hy
599omit [TopologicalSpace X] in
600/-- The restricted Fox graph generators topologically generate their closed generated target. -/
602 (φ : X → H) :
604 (G :=
606 (ProC := ProC) φ : Subgroup
607 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
608 (Set.range
609 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :=
611 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
612 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
614omit [TopologicalSpace X] in
615/-- For a finite generator set, the restricted Fox graph generators converge to `1`. -/
617 [Finite X] (φ : X → H) :
619 (G :=
621 (ProC := ProC) φ : Subgroup
622 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
623 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ) := by
624 exact FamilyConvergesToOne.of_finite_domain
625 (G :=
627 (ProC := ProC) φ : Subgroup
628 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
629 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)
631omit [TopologicalSpace X] in
632/-- The completed Fox semidirect lift into the closed target generated by the graph generators.
634This is the converging-set version needed when the graph generators do not generate the whole
635semidirect product. -/
637 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
638 (φ : X → H)
639 (htarget :
640 ProC (G :=
642 (ProC := ProC) φ : Subgroup
643 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
644 (hφconv :
646 (G :=
648 (ProC := ProC) φ : Subgroup
649 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
650 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
651 F →*
653 (ProC := ProC) φ : Subgroup
654 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
655 hι.lift htarget
656 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)
657 hφconv
659 (ProC := ProC) φ)
661omit [TopologicalSpace X] in
662/-- Continuous homomorphism form of the closed-generated semidirect lift. -/
664 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
665 (φ : X → H)
666 (htarget :
667 ProC (G :=
669 (ProC := ProC) φ : Subgroup
670 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
671 (hφconv :
673 (G :=
675 (ProC := ProC) φ : Subgroup
676 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
677 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
678 F →ₜ*
680 (ProC := ProC) φ : Subgroup
681 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
682 hι.liftHom htarget
683 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)
684 hφconv
686 (ProC := ProC) φ)
688omit [TopologicalSpace X] in
689@[simp]
691 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
692 (φ : X → H)
693 (htarget :
694 ProC (G :=
696 (ProC := ProC) φ : Subgroup
697 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
698 (hφconv :
700 (G :=
702 (ProC := ProC) φ : Subgroup
703 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
704 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
706 (ProC := ProC) hι φ htarget hφconv).toMonoidHom =
708 (ProC := ProC) hι φ htarget hφconv :=
709 rfl
711omit [TopologicalSpace X] in
712@[simp 900]
714 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
715 (φ : X → H)
716 (htarget :
717 ProC (G :=
719 (ProC := ProC) φ : Subgroup
720 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
721 (hφconv :
723 (G :=
725 (ProC := ProC) φ : Subgroup
726 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
727 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
728 (x : X) :
730 (ProC := ProC) hι φ htarget hφconv (ι x) =
731 freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ x :=
732 (hι.lift_spec htarget
733 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)
734 hφconv
736 (ProC := ProC) φ)).2 x
738omit [TopologicalSpace X] in
739/-- The closed-generated semidirect lift is surjective onto the closed target generated by the
740Fox graph generators.
742This is the honest replacement for the generally false assertion that the Fox graph generators
743fill the whole completed semidirect product: the universal map from the free pro-`C` group is
744onto exactly the closed subgroup generated by those graph generators. -/
746 [CompactSpace F]
747 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
748 (φ : X → H)
749 [T2Space
751 (ProC := ProC) φ : Subgroup
752 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))]
753 (htarget :
754 ProC (G :=
756 (ProC := ProC) φ : Subgroup
757 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
758 (hφconv :
760 (G :=
762 (ProC := ProC) φ : Subgroup
763 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
764 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
765 Function.Surjective
767 (ProC := ProC) hι φ htarget hφconv) := by
768 refine
771 (ProC := ProC) hι φ htarget hφconv)
773 (ProC := ProC) φ) ?_
774 rintro y ⟨x, rfl⟩
775 refine ⟨ι x, ?_⟩
776 change
778 (ProC := ProC) hι φ htarget hφconv (ι x) =
779 freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ x
781 (ProC := ProC) hι φ htarget hφconv x
783omit [TopologicalSpace X] in
784/-- The closed-generated lift, viewed in the full completed Fox semidirect product. -/
786 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
787 (φ : X → H)
788 (htarget :
789 ProC (G :=
791 (ProC := ProC) φ : Subgroup
792 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
793 (hφconv :
795 (G :=
797 (ProC := ProC) φ : Subgroup
798 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
799 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
800 F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
802 (ProC := ProC) φ : Subgroup
803 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)).subtype.comp
805 (ProC := ProC) hι φ htarget hφconv)
807omit [TopologicalSpace X] in
808/-- Elementwise form of the semidirect lift theorem, stated in the ambient completed Fox semidirect
809product. Every element of the closed Fox graph target has a preimage under the free pro-`C`
810semidirect lift. -/
812 [CompactSpace F]
813 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
814 (φ : X → H)
815 [T2Space
817 (ProC := ProC) φ : Subgroup
818 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))]
819 (htarget :
820 ProC (G :=
822 (ProC := ProC) φ : Subgroup
823 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
824 (hφconv :
826 (G :=
828 (ProC := ProC) φ : Subgroup
829 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
830 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
831 {y : ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H}
832 (hy : y ∈
834 (ProC := ProC) φ : Subgroup
835 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))) :
836 ∃ g : F,
838 (ProC := ProC) hι φ htarget hφconv g = y := by
839 let yclosed :
841 (ProC := ProC) φ : Subgroup
842 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) :=
843 ⟨y, hy⟩
844 rcases
846 (ProC := ProC) hι φ htarget hφconv yclosed with
847 ⟨g, hg⟩
848 refine ⟨g, ?_⟩
849 simpa [freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated, yclosed] using
850 congrArg Subtype.val hg
852omit [TopologicalSpace X] in
853@[simp]
855 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
856 (φ : X → H)
857 (htarget :
858 ProC (G :=
860 (ProC := ProC) φ : Subgroup
861 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
862 (hφconv :
864 (G :=
866 (ProC := ProC) φ : Subgroup
867 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
868 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
869 (x : X) :
871 (ProC := ProC) hι φ htarget hφconv (ι x) =
872 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
873 simp only [freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated, MonoidHom.coe_comp, Subgroup.coe_subtype,
874 Function.comp_apply, freeProCZCCompletedFoxSemidirectLiftToClosedGenerated_generator,
877omit [TopologicalSpace X] in
878/-- The right component of the closed-generated semidirect lift. -/
880 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
881 (φ : X → H)
882 (htarget :
883 ProC (G :=
885 (ProC := ProC) φ : Subgroup
886 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
887 (hφconv :
889 (G :=
891 (ProC := ProC) φ : Subgroup
892 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
893 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
894 F →* H :=
895 (ZCCompletedFoxSemidirect.rightMonoidHom ProC.finiteQuotientClass X H).comp
897 (ProC := ProC) hι φ htarget hφconv)
899omit [TopologicalSpace X] in
900@[simp]
902 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
903 (φ : X → H)
904 (htarget :
905 ProC (G :=
907 (ProC := ProC) φ : Subgroup
908 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
909 (hφconv :
911 (G :=
913 (ProC := ProC) φ : Subgroup
914 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
915 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
916 (x : X) :
918 (ProC := ProC) hι φ htarget hφconv (ι x) = φ x := by
919 simp only [freeProCZCCompletedFoxRightHomViaClosedGenerated, MonoidHom.coe_comp, Function.comp_apply,
920 freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator, ZCCompletedFoxSemidirect.rightMonoidHom_apply,
923omit [TopologicalSpace X] in
924/-- The derivative-vector component of the closed-generated semidirect lift. -/
926 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
927 (φ : X → H)
928 (htarget :
929 ProC (G :=
931 (ProC := ProC) φ : Subgroup
932 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
933 (hφconv :
935 (G :=
937 (ProC := ProC) φ : Subgroup
938 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
939 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
940 (g : F) :
941 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
943 (ProC := ProC) hι φ htarget hφconv g).left
945omit [TopologicalSpace X] in
946@[simp]
948 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
949 (φ : X → H)
950 (htarget :
951 ProC (G :=
953 (ProC := ProC) φ : Subgroup
954 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
955 (hφconv :
957 (G :=
959 (ProC := ProC) φ : Subgroup
960 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
961 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
962 (x : X) :
964 (ProC := ProC) hι φ htarget hφconv (ι x) =
965 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
967 freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated_generator, freeProCZCCompletedFoxSemidirectGenerator_left]
969omit [TopologicalSpace X] in
970/-- The closed-generated derivative vector is crossed with respect to its right component. -/
972 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
973 (φ : X → H)
974 (htarget :
975 ProC (G :=
977 (ProC := ProC) φ : Subgroup
978 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
979 (hφconv :
981 (G :=
983 (ProC := ProC) φ : Subgroup
984 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
985 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
987 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
989 (ProC := ProC) hι φ htarget hφconv))
991 (ProC := ProC) hι φ htarget hφconv) := by
992 intro g h
993 have hmul := congrArg ZCCompletedFoxSemidirect.left
996 (ProC := ProC) hι φ htarget hφconv) g h)
997 change
999 (ProC := ProC) hι φ htarget hφconv (g * h)).left =
1001 (ProC := ProC) hι φ htarget hφconv g).left +
1002 zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
1004 (ProC := ProC) hι φ htarget hφconv) g •
1006 (ProC := ProC) hι φ htarget hφconv h).left
1007 rw [hmul]
1008 simp only [ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHomViaClosedGenerated,
1009 zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp, Function.comp_apply,
1010 ZCCompletedFoxSemidirect.rightMonoidHom_apply]
1012/-- The continuous completed Fox semidirect lift from a free pro-`C` source. -/
1014 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1015 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1016 (φ : X → H)
1017 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1018 F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
1019 hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ
1021/-- The continuous homomorphism form of the completed Fox semidirect lift from a free pro-`C`
1022source. -/
1024 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1025 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1026 (φ : X → H)
1027 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1028 F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
1029 hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ
1031/-- Forgetting continuity from the continuous semidirect lift gives the underlying semidirect
1032lift. -/
1033@[simp]
1035 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1036 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1037 (φ : X → H)
1038 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1040 (ProC := ProC) hι htarget φ hφ).toMonoidHom =
1042 (ProC := ProC) hι htarget φ hφ :=
1043 rfl
1045/-- The free pro-`C` semidirect lift is continuous. -/
1047 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1048 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1049 (φ : X → H)
1050 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1051 Continuous (freeProCZCCompletedFoxSemidirectLift
1052 (ProC := ProC) hι htarget φ hφ) :=
1054 (ProC := ProC) hι htarget φ hφ).continuous_toFun
1056/-- The free pro-`C` semidirect lift has the prescribed completed Fox generator values. -/
1057@[simp]
1059 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1060 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1061 (φ : X → H)
1062 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1063 (x : X) :
1065 (ProC := ProC) hι htarget φ hφ (ι x) =
1066 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
1067 (hι.lift_spec htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ).2 x
1069/-- The continuous semidirect lift has the prescribed completed Fox generator values. -/
1070@[simp]
1072 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1073 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1074 (φ : X → H)
1075 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1076 (x : X) :
1078 (ProC := ProC) hι htarget φ hφ (ι x) =
1079 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
1080 hι.liftHom_apply htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ x
1082omit [TopologicalSpace X] in
1083/-- The completed Fox semidirect lift from a converging-set free pro-`C` source. The generator
1084map into the semidirect target is required to converge to `1` and topologically generate the
1085target, matching the `IsFreeProCGroupOnConvergingSet` universal property. -/
1087 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1088 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1089 (φ : X → H)
1090 (hφconv :
1092 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1093 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1094 (hφgen :
1096 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1097 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
1098 F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
1099 hι.lift htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
1100 hφconv hφgen
1102omit [TopologicalSpace X] in
1103/-- Continuous homomorphism form of the converging-set completed Fox semidirect lift. -/
1105 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1106 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1107 (φ : X → H)
1108 (hφconv :
1110 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1111 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1112 (hφgen :
1114 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1115 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
1116 F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
1117 hι.liftHom htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
1118 hφconv hφgen
1120omit [TopologicalSpace X] in
1121/-- Forgetting continuity from the converging-set semidirect lift homomorphism gives the
1122unbundled lift. -/
1123@[simp]
1125 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1126 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1127 (φ : X → H)
1128 (hφconv :
1130 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1131 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1132 (hφgen :
1134 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1135 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
1137 (ProC := ProC) hι htarget φ hφconv hφgen).toMonoidHom =
1139 (ProC := ProC) hι htarget φ hφconv hφgen :=
1140 rfl
1142omit [TopologicalSpace X] in
1143/-- The converging-set semidirect lift is continuous. -/
1145 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1146 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1147 (φ : X → H)
1148 (hφconv :
1150 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1151 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1152 (hφgen :
1154 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1155 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
1157 (ProC := ProC) hι htarget φ hφconv hφgen) :=
1159 (ProC := ProC) hι htarget φ hφconv hφgen).continuous_toFun
1161omit [TopologicalSpace X] in
1162/-- The converging-set semidirect lift has the prescribed generator values. -/
1163@[simp]
1165 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1166 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1167 (φ : X → H)
1168 (hφconv :
1170 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1171 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1172 (hφgen :
1174 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1175 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
1176 (x : X) :
1178 (ProC := ProC) hι htarget φ hφconv hφgen (ι x) =
1179 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
1180 (hι.lift_spec htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
1181 hφconv hφgen).2 x
1183omit [TopologicalSpace X] in
1184/-- The converging-set semidirect lift is surjective once its prescribed generator values
1185topologically generate the semidirect target. -/
1187 [CompactSpace F]
1188 [T2Space (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
1189 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1190 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1191 (φ : X → H)
1192 (hφconv :
1194 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1195 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1196 (hφgen :
1198 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1199 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
1200 Function.Surjective
1202 (ProC := ProC) hι htarget φ hφconv hφgen) := by
1203 refine
1206 (ProC := ProC) hι htarget φ hφconv hφgen)
1207 hφgen ?_
1208 rintro y ⟨x, rfl⟩
1209 refine ⟨ι x, ?_⟩
1210 change
1212 (ProC := ProC) hι htarget φ hφconv hφgen (ι x) =
1213 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x
1215 (ProC := ProC) hι htarget φ hφconv hφgen x
1217omit [TopologicalSpace X] in
1218/-- The right component of the converging-set semidirect lift. -/
1220 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1221 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1222 (φ : X → H)
1223 (hφconv :
1225 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1226 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1227 (hφgen :
1229 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1230 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
1231 F →* H :=
1232 (ZCCompletedFoxSemidirect.rightMonoidHom ProC.finiteQuotientClass X H).comp
1234 (ProC := ProC) hι htarget φ hφconv hφgen)
1236omit [TopologicalSpace X] in
1237/-- The derivative-vector component of the converging-set semidirect lift. -/
1239 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1240 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1241 (φ : X → H)
1242 (hφconv :
1244 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1245 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1246 (hφgen :
1248 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1249 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
1250 (g : F) :
1251 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
1253 (ProC := ProC) hι htarget φ hφconv hφgen g).left
1255omit [TopologicalSpace X] in
1256@[simp]
1258 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1259 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1260 (φ : X → H)
1261 (hφconv :
1263 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1264 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1265 (hφgen :
1267 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1268 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
1269 (x : X) :
1271 (ProC := ProC) hι htarget φ hφconv hφgen (ι x) = φ x := by
1272 simp only [freeProCZCCompletedFoxRightHomOfConvergingSet, MonoidHom.coe_comp, Function.comp_apply,
1273 freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator, ZCCompletedFoxSemidirect.rightMonoidHom_apply,
1276omit [TopologicalSpace X] in
1277@[simp]
1279 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1280 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1281 (φ : X → H)
1282 (hφconv :
1284 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1285 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1286 (hφgen :
1288 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1289 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
1290 (x : X) :
1292 (ProC := ProC) hι htarget φ hφconv hφgen (ι x) =
1293 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
1295 freeProCZCCompletedFoxSemidirectLiftOfConvergingSet_generator, freeProCZCCompletedFoxSemidirectGenerator_left]
1297omit [TopologicalSpace X] in
1298/-- The converging-set derivative vector is a crossed differential with respect to its right
1299component. -/
1301 {ι : X → F} (hι : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
1302 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1303 (φ : X → H)
1304 (hφconv :
1306 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1307 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1308 (hφgen :
1310 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
1311 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
1313 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
1315 (ProC := ProC) hι htarget φ hφconv hφgen))
1317 (ProC := ProC) hι htarget φ hφconv hφgen) := by
1318 intro g h
1319 change
1321 (ProC := ProC) hι htarget φ hφconv hφgen (g * h)).left =
1323 (ProC := ProC) hι htarget φ hφconv hφgen g).left +
1324 zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
1326 (ProC := ProC) hι htarget φ hφconv hφgen) g •
1328 (ProC := ProC) hι htarget φ hφconv hφgen h).left
1329 simp only [map_mul, ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHomOfConvergingSet,
1330 ZCCompletedFoxSemidirect.rightMonoidHom, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_comp, MonoidHom.coe_mk,
1331 OneHom.coe_mk, Function.comp_apply]
1333/-- The categorical completed Fox semidirect lift from a free pro-`C` source, bundled as a
1336 [ProCGroups.ProC.ProCGroup ProC F]
1337 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
1338 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1339 (φ : X → H)
1340 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1341 ProCGrp.of ProC F ⟶
1342 ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
1343 hι.liftMorphism
1344 (ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1345 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ
1347/-- The underlying continuous homomorphism of the categorical completed Fox semidirect lift is
1348the free pro-`C` continuous homomorphism supplied by `liftHom`. -/
1349@[simp]
1351 [ProCGroups.ProC.ProCGroup ProC F]
1352 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
1353 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1354 (φ : X → H)
1355 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1357 (ProC := ProC) hι φ hφ).hom =
1359 (ProC := ProC) hι
1360 (inferInstanceAs
1361 (ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
1362 φ hφ :=
1363 rfl
1365/-- The underlying homomorphism of the categorical completed Fox semidirect lift is the
1366unbundled completed Fox semidirect lift. -/
1367@[simp]
1369 [ProCGroups.ProC.ProCGroup ProC F]
1370 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
1371 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1372 (φ : X → H)
1373 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1375 (ProC := ProC) hι φ hφ).hom.toMonoidHom =
1377 (ProC := ProC) hι
1378 (inferInstanceAs
1379 (ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
1380 φ hφ :=
1381 rfl
1383/-- The categorical completed Fox semidirect lift has the prescribed generator values. -/
1384@[simp]
1386 [ProCGroups.ProC.ProCGroup ProC F]
1387 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
1388 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1389 (φ : X → H)
1390 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1391 (x : X) :
1393 (ProC := ProC) hι φ hφ (ι x) =
1394 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
1395 hι.liftMorphism_apply
1396 (ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1397 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ x
1399/-- The left component of the categorical completed Fox semidirect lift has the standard Fox
1400coordinate on each generator. -/
1401@[simp]
1403 [ProCGroups.ProC.ProCGroup ProC F]
1404 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
1405 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1406 (φ : X → H)
1407 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1408 (x : X) :
1410 (ProC := ProC) hι φ hφ (ι x)).left =
1411 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
1413 rfl
1415/-- The right component of the categorical completed Fox semidirect lift has the prescribed
1417@[simp]
1419 [ProCGroups.ProC.ProCGroup ProC F]
1420 [ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
1421 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1422 (φ : X → H)
1423 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1424 (x : X) :
1426 (ProC := ProC) hι φ hφ (ι x)).right = φ x := by
1428 rfl
1430/-- The left component of the free pro-`C` semidirect lift has the standard Fox coordinate on
1431each generator. -/
1432@[simp]
1434 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1435 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1436 (φ : X → H)
1437 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1438 (x : X) :
1440 (ProC := ProC) hι htarget φ hφ (ι x)).left =
1441 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
1443 rfl
1445/-- The left component of the continuous free pro-`C` semidirect lift has the standard Fox
1446coordinate on each generator. -/
1447@[simp]
1449 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1450 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1451 (φ : X → H)
1452 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1453 (x : X) :
1455 (ProC := ProC) hι htarget φ hφ (ι x)).left =
1456 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
1458 rfl
1460/-- The right component of the free pro-`C` semidirect lift has the prescribed generator value. -/
1461@[simp]
1463 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1464 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1465 (φ : X → H)
1466 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1467 (x : X) :
1469 (ProC := ProC) hι htarget φ hφ (ι x)).right = φ x := by
1471 rfl
1473/-- The right component of the continuous free pro-`C` semidirect lift has the prescribed
1475@[simp]
1477 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1478 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1479 (φ : X → H)
1480 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1481 (x : X) :
1483 (ProC := ProC) hι htarget φ hφ (ι x)).right = φ x := by
1485 rfl
1487/-- The target-group component of the continuous completed Fox semidirect lift. -/
1489 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1490 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1491 (φ : X → H)
1492 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1493 F →* H where
1494 toFun g := (freeProCZCCompletedFoxSemidirectLift
1495 (ProC := ProC) hι htarget φ hφ g).right
1496 map_one' := by
1498 map_mul' g h := by
1501/-- The right component of the continuous completed Fox semidirect lift is the associated
1502homomorphism. -/
1503@[simp]
1505 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1506 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1507 (φ : X → H)
1508 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1509 (g : F) :
1510 freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ g =
1512 (ProC := ProC) hι htarget φ hφ g).right :=
1513 rfl
1515/-- The target-group component has the prescribed generator values. -/
1516@[simp]
1518 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1519 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1520 (φ : X → H)
1521 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1522 (x : X) :
1523 freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ (ι x) = φ x := by
1527/-- The completed Fox derivative vector obtained as the left component of the continuous
1528free pro-`C` semidirect lift. -/
1530 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1531 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1532 (φ : X → H)
1533 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1534 (g : F) :
1535 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
1537 (ProC := ProC) hι htarget φ hφ g).left
1539/-- The free pro-`C` completed Fox derivative vector has the standard coordinate value on
1540generators. -/
1541@[simp]
1543 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1544 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1545 (φ : X → H)
1546 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
1547 (x : X) :
1549 (ProC := ProC) hι htarget φ hφ (ι x) =
1550 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
1554/-- The free pro-`C` completed Fox derivative vector is crossed with respect to the target-group
1555component of the continuous semidirect lift. -/
1557 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
1558 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
1559 (φ : X → H)
1560 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
1562 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
1563 (freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ))
1565 (ProC := ProC) hι htarget φ hφ) := by
1566 intro g h
1567 have hmul := congrArg ZCCompletedFoxSemidirect.left
1569 (ProC := ProC) hι htarget φ hφ) g h)
1571 (ProC := ProC) hι htarget φ hφ (g * h)).left =
1573 (ProC := ProC) hι htarget φ hφ g).left +
1574 zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
1575 (freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ) g •
1577 (ProC := ProC) hι htarget φ hφ h).left
1578 rw [hmul]
1579 simp only [ZCCompletedFoxSemidirect.mul_left, freeProCZCCompletedFoxRightHom,
1580 zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_mk, OneHom.coe_mk]
1583end
1585end FoxDifferential