FoxDifferential/Completed/Continuous/Topology.lean
1import FoxDifferential.Completed.FreeProC.SemidirectKernelBasis
2import FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Continuous/Topology.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Continuous crossed differentials
15Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
16-/
17namespace FoxDifferential
19noncomputable section
21open ProCGroups.InverseSystems
22open ProCGroups.Completion
23open scoped BigOperators
25universe u v
27/-- The finite quotients of the all-finite pro-`C` predicate are exactly finite groups. -/
30 ProCGroups.ProC.allFiniteProC.finiteQuotientClass) :=
31 ⟨by
32 intro G _ hG
35section BoundaryMapContinuity
37variable {R : Type u} [Ring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousMul R]
38variable {X : Type v} [Fintype X]
40/-- A finite Fox boundary map is continuous over any topological ring. -/
41theorem continuous_foxBoundaryMap (generatorBoundary : X → R) :
42 Continuous (foxBoundaryMap generatorBoundary) := by
43 change Continuous (fun v : X → R => ∑ x : X, v x * generatorBoundary x)
44 exact continuous_finset_sum _ fun x _ => (continuous_apply x).mul continuous_const
46end BoundaryMapContinuity
48section CompletedGroupAlgebraTopology
50variable (C : ProCGroups.FiniteGroupClass.{u})
51variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
52variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
54/-- The discrete topology on a finite pro-`C` stage of `Z_C[[G]]`. -/
56 (i : ZCCompletedGroupAlgebraIndex C G) :
57 TopologicalSpace (ZCCompletedGroupAlgebraStage C G i) :=
58 ⊥
61 (i : ZCCompletedGroupAlgebraIndex C G) :
62 DiscreteTopology (ZCCompletedGroupAlgebraStage C G i) :=
63 ⟨rfl⟩
66 (i : ZCCompletedGroupAlgebraIndex C G) :
67 CompactSpace (ZCCompletedGroupAlgebraStage C G i) := by
68 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
69 letI : Finite (ZCCompletedGroupAlgebraStage C G i) :=
71 (n := i.1.modulus) (G := G) C
72 (Fact.out (p := ProCGroups.FiniteGroupClass.FiniteOnly C)) i.2
73 letI : Fintype (ZCCompletedGroupAlgebraStage C G i) := Fintype.ofFinite _
74 infer_instance
77 (i : ZCCompletedGroupAlgebraIndex C G) :
78 T2Space (ZCCompletedGroupAlgebraStage C G i) :=
79 inferInstance
82 (i : ZCCompletedGroupAlgebraIndex C G) :
83 TotallyDisconnectedSpace (ZCCompletedGroupAlgebraStage C G i) :=
84 inferInstance
86/-- The pro-`C` completed group algebra is compact in its inverse-limit topology. -/
87instance instCompactSpaceZCCompletedGroupAlgebra :
88 CompactSpace (ZCCompletedGroupAlgebra C G) := by
89 let S := zcCompletedGroupAlgebraSystem C G
90 change CompactSpace S.inverseLimit
91 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
92 inferInstance
93 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, CompactSpace (S.X i) := fun i => by
94 dsimp [S, zcCompletedGroupAlgebraSystem]
95 infer_instance
96 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
97 dsimp [S, zcCompletedGroupAlgebraSystem]
98 infer_instance
99 infer_instance
101/-- The pro-`C` completed group algebra is Hausdorff in its inverse-limit topology. -/
102instance instT2SpaceZCCompletedGroupAlgebra :
103 T2Space (ZCCompletedGroupAlgebra C G) := by
104 let S := zcCompletedGroupAlgebraSystem C G
105 change T2Space S.inverseLimit
106 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
107 inferInstance
108 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
109 dsimp [S, zcCompletedGroupAlgebraSystem]
110 infer_instance
111 exact S.t2Space_inverseLimit
113omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
114/-- A finite stage projection from `Z_C[[G]]` is continuous. -/
116 (i : ZCCompletedGroupAlgebraIndex C G) :
117 Continuous (zcCompletedGroupAlgebraProjection C G i) :=
118 (continuous_apply i).comp continuous_subtype_val
120omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
121/-- A finite stage projection from `Z_C[[G]]`, regarded as a ring homomorphism, is continuous. -/
123 (i : ZCCompletedGroupAlgebraIndex C G) :
124 Continuous (zcCompletedGroupAlgebraProjectionRingHom C G i) :=
127/-- The pro-`C` completed group algebra is totally disconnected in its inverse-limit
128topology. -/
130 TotallyDisconnectedSpace (ZCCompletedGroupAlgebra C G) := by
131 let S := zcCompletedGroupAlgebraSystem C G
132 change TotallyDisconnectedSpace S.inverseLimit
133 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
134 inferInstance
135 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TotallyDisconnectedSpace (S.X i) := fun i => by
136 dsimp [S, zcCompletedGroupAlgebraSystem]
137 infer_instance
138 exact S.totallyDisconnectedSpace_inverseLimit
140/-- Addition on the pro-`C` completed group algebra is continuous. -/
141instance instContinuousAddZCCompletedGroupAlgebra :
142 ContinuousAdd (ZCCompletedGroupAlgebra C G) where
143 continuous_add := by
144 have hval : Continuous (fun p : ZCCompletedGroupAlgebra C G ×
145 ZCCompletedGroupAlgebra C G =>
146 ((p.1 + p.2 : ZCCompletedGroupAlgebra C G) :
147 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
148 exact continuous_pi fun i =>
149 (continuous_of_discreteTopology :
150 Continuous (fun q : ZCCompletedGroupAlgebraStage C G i ×
151 ZCCompletedGroupAlgebraStage C G i => q.1 + q.2)).comp
152 (((continuous_apply i).comp (continuous_subtype_val.comp continuous_fst)).prodMk
153 ((continuous_apply i).comp (continuous_subtype_val.comp continuous_snd)))
154 simpa [Subtype.eta] using
155 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
156 (fun p => (p.1 + p.2 : ZCCompletedGroupAlgebra C G).property))
158/-- Negation on the pro-`C` completed group algebra is continuous. -/
159instance instContinuousNegZCCompletedGroupAlgebra :
160 ContinuousNeg (ZCCompletedGroupAlgebra C G) where
161 continuous_neg := by
162 change Continuous (fun x : ZCCompletedGroupAlgebra C G => -x)
163 have hval : Continuous (fun x : ZCCompletedGroupAlgebra C G =>
164 ((-x : ZCCompletedGroupAlgebra C G) :
165 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
166 exact continuous_pi fun i =>
167 (continuous_of_discreteTopology :
168 Continuous (fun y : ZCCompletedGroupAlgebraStage C G i => -y)).comp
169 ((continuous_apply i).comp continuous_subtype_val)
170 simpa [Subtype.eta] using
171 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
172 (fun x => (-x : ZCCompletedGroupAlgebra C G).property))
174/-- The additive group structure on the pro-`C` completed group algebra is topological. -/
176 IsTopologicalAddGroup (ZCCompletedGroupAlgebra C G) where
177 continuous_add := continuous_add
178 continuous_neg := continuous_neg
180/-- Multiplication on the pro-`C` completed group algebra is continuous. -/
181instance instContinuousMulZCCompletedGroupAlgebra :
182 ContinuousMul (ZCCompletedGroupAlgebra C G) where
183 continuous_mul := by
184 have hval : Continuous (fun p : ZCCompletedGroupAlgebra C G ×
185 ZCCompletedGroupAlgebra C G =>
186 ((p.1 * p.2 : ZCCompletedGroupAlgebra C G) :
187 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
188 exact continuous_pi fun i =>
189 (continuous_of_discreteTopology :
190 Continuous (fun q : ZCCompletedGroupAlgebraStage C G i ×
191 ZCCompletedGroupAlgebraStage C G i => q.1 * q.2)).comp
192 (((continuous_apply i).comp (continuous_subtype_val.comp continuous_fst)).prodMk
193 ((continuous_apply i).comp (continuous_subtype_val.comp continuous_snd)))
194 simpa [Subtype.eta] using
195 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
196 (fun p => (p.1 * p.2 : ZCCompletedGroupAlgebra C G).property))
198/-- The completed group algebra is a topological ring in its inverse-limit topology. -/
200 IsTopologicalRing (ZCCompletedGroupAlgebra C G) where
201 continuous_add := continuous_add
202 continuous_mul := continuous_mul
203 continuous_neg := continuous_neg
205/-- Scalar multiplication of `Z_C[[G]]` on itself is continuous. -/
207 ContinuousSMul (ZCCompletedGroupAlgebra C G) (ZCCompletedGroupAlgebra C G) :=
208 ContinuousMul.to_continuousSMul
210omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
211/-- The scalar action map on the completed group algebra is continuous. -/
213 Continuous (fun p : ZCCompletedGroupAlgebra C G × ZCCompletedGroupAlgebra C G =>
214 p.1 • p.2) :=
215 continuous_smul
217omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
218/-- The completed group-like map `G -> Z_C[[G]]` is continuous. -/
219theorem continuous_zcGroupLike : Continuous (zcGroupLike C G) := by
220 have hval : Continuous (fun g : G =>
221 ((zcGroupLike C G g : ZCCompletedGroupAlgebra C G) :
222 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
223 refine continuous_pi fun i => ?_
224 letI : DiscreteTopology (CompletedGroupAlgebraQuotientInClass G C i.2) :=
225 QuotientGroup.discreteTopology
226 (ProCGroups.openNormalSubgroup_isOpen (G := G)
227 ((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G))
228 exact (continuous_of_discreteTopology :
229 Continuous (fun q : CompletedGroupAlgebraQuotientInClass G C i.2 =>
230 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
231 (CompletedGroupAlgebraQuotientInClass G C i.2) q)).comp
232 (continuous_quotient_mk' : Continuous (fun g : G =>
233 QuotientGroup.mk' (((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G) g))
234 simpa [Subtype.eta] using
235 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
236 (fun g => (zcGroupLike C G g : ZCCompletedGroupAlgebra C G).property))
238omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
239/-- The completed augmentation `Z_C[[G]] -> Z_C` is continuous in the inverse-limit topology. -/
242 Continuous (zcCompletedGroupAlgebraAugmentation C G) := by
243 have hval : Continuous (fun x : ZCCompletedGroupAlgebra C G =>
244 (zcCompletedGroupAlgebraAugmentation C G x :
245 (i : ProCIntegerIndex C) → ProCIntegerStage C i)) := by
246 refine continuous_pi fun i => ?_
247 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
248 let U := zcCompletedGroupAlgebraTopIndex C G
249 letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass i.modulus G C U) := ⊥
250 letI : DiscreteTopology (ModNCompletedGroupAlgebraStageInClass i.modulus G C U) := ⟨rfl⟩
251 exact
252 (continuous_of_discreteTopology :
253 Continuous (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus G C U)).comp
254 ((continuous_apply (i, U)).comp continuous_subtype_val)
255 simpa [zcCompletedGroupAlgebraAugmentation, Subtype.eta] using
256 (Continuous.subtype_mk (p := ProCIntegerCompatible C) hval
257 (fun x => (zcCompletedGroupAlgebraAugmentation C G x).property))
259omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
260/-- The completed augmentation ideal is closed in `Z_C[[G]]`. -/
263 IsClosed
265 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
266 change IsClosed ((zcCompletedGroupAlgebraAugmentation C G) ⁻¹' ({0} : Set (ZCCoeff C)))
267 exact isClosed_singleton.preimage
268 (continuous_zcCompletedGroupAlgebraAugmentation (C := C) (G := G))
270/-- The completed augmentation ideal is compact as a closed subspace of `Z_C[[G]]`. -/
273 CompactSpace (ZCCompletedGroupAlgebraAugmentationIdeal C G) := by
274 exact
276 (C := C) (G := G)).isClosedEmbedding_subtypeVal.compactSpace
278/-- The completed augmentation ideal is Hausdorff. -/
281 T2Space (ZCCompletedGroupAlgebraAugmentationIdeal C G) :=
282 inferInstance
284variable {A : Type v} [Group A] [TopologicalSpace A]
286omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
287/-- The completed group-algebra boundary `a ↦ [ψ a] - 1` is continuous whenever `ψ` is
288continuous. -/
290 (ψ : A →* G) (hψ : Continuous ψ) :
291 Continuous (zcCompletedGroupAlgebraBoundary C ψ) := by
292 simpa [zcCompletedGroupAlgebraBoundary] using
293 ((continuous_zcGroupLike (C := C) (G := G)).comp hψ).sub continuous_const
295variable {X : Type v} [Fintype X] [DecidableEq X]
297omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
298/-- The completed `Z_C[[G]]` Fox boundary/Euler map is continuous. -/
299theorem continuous_zcFreeGroupFoxBoundary (ψ : FreeGroup X →* G) :
300 Continuous (zcFreeGroupFoxBoundary C ψ) := by
301 classical
303 exact continuous_foxBoundaryMap _
305end CompletedGroupAlgebraTopology
307section CompletedSourceBoundary
309variable (C : ProCGroups.FiniteGroupClass.{u})
310variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
311variable {X H : Type u} [Fintype X]
312variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
314/-- Source-shaped completed Fox boundary map for a finite generating set. It evaluates a vector
316def freeProCZCCompletedFoxBoundary (φ : X → H) :
317 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
318 ZCCompletedGroupAlgebra C H :=
319 foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1)
322omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
323/-- The source-shaped completed Fox boundary map is the expected finite Euler sum. -/
325 (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
326 freeProCZCCompletedFoxBoundary C φ v =
327 ∑ x : X, v x * (zcGroupLike C H (φ x) - 1) :=
328 rfl
330variable [DecidableEq X]
333omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
334/-- The source-shaped completed Fox boundary map sends the standard basis vector at `x` to
335`[φ x] - 1`. -/
336@[simp]
338 (φ : X → H) (x : X) :
340 (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) =
341 zcGroupLike C H (φ x) - 1 := by
342 simp only [freeProCZCCompletedFoxBoundary, foxBoundaryMap_single]
344omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
345/-- The source-shaped completed Fox boundary map is continuous for finite generating sets. -/
346theorem continuous_freeProCZCCompletedFoxBoundary (φ : X → H) :
347 Continuous (freeProCZCCompletedFoxBoundary C φ) :=
350omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
351/-- The source-shaped completed Fox boundary has image equal to the submodule generated by the
352augmentation generators `[φ x] - 1`. -/
354 (φ : X → H) :
355 (freeProCZCCompletedFoxBoundary C φ).range =
356 Submodule.span (ZCCompletedGroupAlgebra C H)
357 (Set.range fun x : X => zcGroupLike C H (φ x) - 1) := by
358 apply le_antisymm
359 · rintro y ⟨v, rfl⟩
361 exact Submodule.sum_mem _ fun x _ =>
362 Submodule.smul_mem _ (v x)
363 (Submodule.subset_span (Set.mem_range_self x))
364 · refine Submodule.span_le.2 ?_
365 rintro y ⟨x, rfl⟩
366 exact ⟨Pi.single x (1 : ZCCompletedGroupAlgebra C H), by simp only [freeProCZCCompletedFoxBoundary_single]⟩
368omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
369/-- If the chosen finite source hits every element of `H`, the source-shaped completed Fox
372 (φ : X → H) (hφ : Function.Surjective φ) :
373 (freeProCZCCompletedFoxBoundary C φ).range =
375 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
378 congr 1
379 ext y
380 constructor
381 · rintro ⟨x, rfl⟩
382 exact ⟨φ x, rfl⟩
383 · rintro ⟨h, rfl⟩
384 rcases hφ h with ⟨x, rfl⟩
385 exact ⟨x, rfl⟩
387end CompletedSourceBoundary
389section SemidirectTopology
391variable (C : ProCGroups.FiniteGroupClass.{v})
392variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
393variable (X : Type u) [DecidableEq X]
394variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
396/-- The standard topology on `Z_C[[H]]^X ⋊ H`, induced from the product of coordinates and `H`.
397-/
399 TopologicalSpace (ZCCompletedFoxSemidirect C X H) :=
400 TopologicalSpace.induced
401 (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) inferInstance
403/-- The completed Fox semidirect target is homeomorphic to its product of components. -/
405 ZCCompletedFoxSemidirect C X H ≃ₜ (ZCFreeFoxCoordinates C (X := X) (H := H) × H) where
406 toEquiv :=
407 { toFun := fun a => (a.left, a.right)
408 invFun := fun p => { left := p.1, right := p.2 }
409 left_inv := by
410 intro a
411 cases a
412 rfl
413 right_inv := by
414 intro p
415 cases p
416 rfl }
417 continuous_toFun := continuous_induced_dom
418 continuous_invFun := by
419 rw [continuous_induced_rng]
420 exact continuous_id
422omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
423/-- The component-pair map from the semidirect target is continuous. -/
425 Continuous (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) :=
426 continuous_induced_dom
428omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
429/-- The Fox-coordinate projection from the semidirect target is continuous. -/
431 Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.left) :=
432 continuous_fst.comp (continuous_zcCompletedFoxSemidirect_toProd C X H)
434omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
435/-- The group projection from the semidirect target is continuous. -/
437 Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.right) :=
438 continuous_snd.comp (continuous_zcCompletedFoxSemidirect_toProd C X H)
440/-- Compactness of the completed Fox semidirect target when the group component is compact. -/
441instance instCompactSpaceZCCompletedFoxSemidirect [CompactSpace H] :
442 CompactSpace (ZCCompletedFoxSemidirect C X H) := by
443 exact (zcCompletedFoxSemidirectHomeomorphProd C X H).symm.compactSpace
445/-- Hausdorffness of the completed Fox semidirect target when the group component is Hausdorff. -/
446instance instT2SpaceZCCompletedFoxSemidirect [T2Space H] :
447 T2Space (ZCCompletedFoxSemidirect C X H) := by
448 exact (zcCompletedFoxSemidirectHomeomorphProd C X H).symm.t2Space
450/-- Total disconnectedness of the completed Fox semidirect target when the group component is
451totally disconnected. -/
452instance instTotallyDisconnectedSpaceZCCompletedFoxSemidirect [TotallyDisconnectedSpace H] :
453 TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H) := by
454 exact (zcCompletedFoxSemidirectHomeomorphProd C X H).symm.totallyDisconnectedSpace
456/-- The completed Fox semidirect target is a topological group with its standard product
457topology. -/
459 IsTopologicalGroup (ZCCompletedFoxSemidirect C X H) where
460 continuous_mul := by
461 letI : ContinuousMul H := (inferInstanceAs (IsTopologicalGroup H)).toContinuousMul
462 rw [continuous_induced_rng]
463 have hleft : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
464 ZCCompletedFoxSemidirect C X H => (p.1 * p.2).left) := by
465 refine continuous_pi fun x => ?_
466 have hleftA : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
467 ZCCompletedFoxSemidirect C X H => p.1.left x) :=
468 (continuous_apply x).comp
469 ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_fst)
470 have hrightA : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
471 ZCCompletedFoxSemidirect C X H => p.2.left x) :=
472 (continuous_apply x).comp
473 ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_snd)
474 have hgroup : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
475 ZCCompletedFoxSemidirect C X H => zcGroupLike C H p.1.right) :=
476 (continuous_zcGroupLike (C := C) (G := H)).comp
477 ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_fst)
478 change Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
479 ZCCompletedFoxSemidirect C X H =>
480 p.1.left x + zcGroupLike C H p.1.right * p.2.left x)
481 exact hleftA.add (hgroup.mul hrightA)
482 have hright : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
483 ZCCompletedFoxSemidirect C X H => (p.1 * p.2).right) := by
484 exact ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_fst).mul
485 ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_snd)
486 exact hleft.prodMk hright
487 continuous_inv := by
488 letI : ContinuousInv H := (inferInstanceAs (IsTopologicalGroup H)).toContinuousInv
489 rw [continuous_induced_rng]
490 have hleft : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a⁻¹.left) := by
491 refine continuous_pi fun x => ?_
492 have hleftA : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.left x) :=
493 (continuous_apply x).comp (continuous_zcCompletedFoxSemidirect_left C X H)
494 have hgroup : Continuous (fun a : ZCCompletedFoxSemidirect C X H =>
495 zcGroupLike C H a.right⁻¹) :=
496 (continuous_zcGroupLike (C := C) (G := H)).comp
497 ((continuous_zcCompletedFoxSemidirect_right C X H).inv)
498 change Continuous (fun a : ZCCompletedFoxSemidirect C X H =>
499 -(zcGroupLike C H a.right⁻¹ * a.left x))
501 have hright : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a⁻¹.right) := by
502 exact (continuous_zcCompletedFoxSemidirect_right C X H).inv
503 exact hleft.prodMk hright
505omit [DecidableEq X] in
506/-- The completed Fox semidirect target is profinite when the group component is profinite. -/
508 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] :
509 ProCGroups.IsProfiniteGroup (ZCCompletedFoxSemidirect C X H) := by
510 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
512/-- The completed Fox semidirect target is an all-finite pro-`C` group when the group component is
513profinite. -/
515 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] :
517 (ZCCompletedFoxSemidirect C X H) :=
521omit [DecidableEq X] in
522/-- The completed Fox semidirect target is an all-finite pro-`C` group when the group component is
523profinite. This theorem form is convenient when an explicit target proof is needed. -/
525 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] :
526 ProCGroups.ProC.allFiniteProC (G := ZCCompletedFoxSemidirect C X H) :=
527 (inferInstanceAs
529 (ZCCompletedFoxSemidirect C X H))).isProC
531end SemidirectTopology
533section CompletedGroupAlgebraProC
535variable (C : ProCGroups.FiniteGroupClass.{u})
536variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
538/-- One finite stage `(Z/nZ)[H/U]`, written multiplicatively from its additive group, belongs
542 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
543 (hProd : ProCGroups.FiniteGroupClass.FiniteProductClosed C)
544 (i : ProCIntegerIndex C) (U : CompletedGroupAlgebraIndexInClass H C) :
545 C (Multiplicative (ModNCompletedGroupAlgebraStageInClass i.modulus H C U)) := by
546 classical
547 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
548 let Q := CompletedGroupAlgebraQuotientInClass H C U
549 letI : Finite Q := ProCGroups.FiniteGroupClass.finite (C := C) (OrderDual.ofDual U).2
550 letI : Fintype Q := Fintype.ofFinite Q
551 let e :
552 Multiplicative (ModNCompletedGroupAlgebraStageInClass i.modulus H C U) ≃*
553 (Q → ULift.{u} (Multiplicative (ModNCompletedCoeff i.modulus))) :=
554 { toFun := fun a q =>
555 ULift.up (Multiplicative.ofAdd ((Finsupp.equivFunOnFinite a.toAdd) q))
556 invFun := fun f =>
557 Multiplicative.ofAdd
558 (Finsupp.equivFunOnFinite.symm fun q => (f q).down.toAdd)
559 left_inv := by
560 intro a
561 apply Multiplicative.ext
562 exact Finsupp.equivFunOnFinite.left_inv a.toAdd
563 right_inv := by
564 intro f
565 funext q
566 have hcoeff :
567 (Finsupp.equivFunOnFinite
568 (Finsupp.equivFunOnFinite.symm fun q => (f q).down.toAdd)) q =
569 (f q).down.toAdd := by
570 exact congrFun
571 (Finsupp.equivFunOnFinite.right_inv
572 (fun q => (f q).down.toAdd)) q
573 apply ULift.ext
574 apply Multiplicative.ext
575 exact hcoeff
576 map_mul' := by
577 intro a b
578 funext q
579 apply ULift.ext
580 apply Multiplicative.ext
581 rfl }
582 have hPi :
583 C (Q → ULift.{u} (Multiplicative (ModNCompletedCoeff i.modulus))) := by
584 exact hProd (ι := Q)
585 (G := fun _ => ULift.{u} (Multiplicative (ModNCompletedCoeff i.modulus)))
586 (fun _ => by
587 simpa [ModNCompletedCoeff, ProCIntegerStage] using i.cyclic_mem)
588 exact hIso ⟨e.symm⟩ hPi
590/-- The group-valued inverse system underlying the additive group of `Z_C[[H]]`, written
591multiplicatively. -/
593 ProCGroups.InverseSystems.InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
594 X := fun i => Multiplicative (ZCCompletedGroupAlgebraStage C H i)
595 topologicalSpace := fun _ => ⊥
596 map := fun {i j} hij =>
597 (zcCompletedGroupAlgebraTransition C H hij).toAddMonoidHom.toMultiplicative
598 continuous_map := by
599 intro i j hij
600 exact continuous_of_discreteTopology
601 map_id := by
602 intro i
603 funext x
604 apply Multiplicative.ext
605 change zcCompletedGroupAlgebraTransition C H (le_rfl : i ≤ i) x.toAdd = x.toAdd
606 simp only [zcCompletedGroupAlgebraTransition_id, RingHom.id_apply]
607 map_comp := by
608 intro i j k hij hjk
609 funext x
610 apply Multiplicative.ext
611 change
612 zcCompletedGroupAlgebraTransition C H hij
613 (zcCompletedGroupAlgebraTransition C H hjk x.toAdd) =
614 zcCompletedGroupAlgebraTransition C H (hij.trans hjk) x.toAdd
615 exact congrArg (fun f : ZCCompletedGroupAlgebraStage C H k →+*
616 ZCCompletedGroupAlgebraStage C H i => f x.toAdd)
617 (zcCompletedGroupAlgebraTransition_comp C H hij hjk)
620 (i : ZCCompletedGroupAlgebraIndex C H) :
621 Group ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i) := by
623 infer_instance
626 (i : ZCCompletedGroupAlgebraIndex C H) :
627 IsTopologicalGroup ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i) := by
629 infer_instance
631/-- The multiplicative additive stages of `Z_C[[H]]` form a group-valued inverse system. -/
634 (zcCompletedGroupAlgebraMultiplicativeSystem C H) where
636 intro i j hij
637 simp only [zcCompletedGroupAlgebraMultiplicativeSystem, RingHom.toAddMonoidHom_eq_coe,
638 AddMonoidHom.coe_toMultiplicative, AddMonoidHom.coe_coe, Function.comp_apply, toAdd_one, map_zero, ofAdd_zero]
640 intro i j hij x y
641 simp only [zcCompletedGroupAlgebraMultiplicativeSystem, RingHom.toAddMonoidHom_eq_coe,
642 AddMonoidHom.coe_toMultiplicative, AddMonoidHom.coe_coe, Function.comp_apply, toAdd_mul, map_add, ofAdd_add]
643 map_inv := by
644 intro i j hij x
645 simp only [zcCompletedGroupAlgebraMultiplicativeSystem, RingHom.toAddMonoidHom_eq_coe,
646 AddMonoidHom.coe_toMultiplicative, AddMonoidHom.coe_coe, Function.comp_apply, toAdd_inv, map_neg, ofAdd_neg]
648/-- The multiplicative inverse limit of the finite completed group-algebra stages is the
649additive group underlying `Z_C[[H]]`, written multiplicatively. -/
651 (zcCompletedGroupAlgebraMultiplicativeSystem C H).inverseLimit ≃ₜ*
652 Multiplicative (ZCCompletedGroupAlgebra C H) := by
653 let S := zcCompletedGroupAlgebraMultiplicativeSystem C H
654 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, Group (S.X i) := fun i => by
655 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
656 infer_instance
657 letI : ProCGroups.InverseSystems.IsGroupSystem S := by
658 dsimp [S]
659 infer_instance
660 refine
661 { toMulEquiv := ?_
662 continuous_toFun := ?_
663 continuous_invFun := ?_ }
664 · refine
665 { toFun := fun x =>
666 Multiplicative.ofAdd
667 (⟨fun i => (S.projection i x).toAdd, by
668 intro i j hij
669 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij)⟩ :
671 invFun := fun x =>
672 (⟨fun i =>
673 Multiplicative.ofAdd
674 (zcCompletedGroupAlgebraProjection C H i x.toAdd), by
675 intro i j hij
676 apply Multiplicative.ext
677 exact x.toAdd.2 i j hij⟩ :
678 S.inverseLimit)
679 left_inv := by
680 intro x
681 apply S.ext
682 intro i
683 rfl
684 right_inv := by
685 intro x
686 apply Multiplicative.ext
687 ext i
688 rfl
689 map_mul' := by
690 intro x y
691 apply Multiplicative.ext
692 ext i
693 rfl }
694 · refine continuous_ofAdd.comp ?_
695 have hambient : Continuous fun x : S.inverseLimit =>
696 (fun i : ZCCompletedGroupAlgebraIndex C H => (S.projection i x).toAdd :
697 ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i) := by
698 exact continuous_pi fun i => continuous_toAdd.comp (S.continuous_projection i)
699 exact Continuous.subtype_mk hambient (fun x => by
700 intro i j hij
701 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij))
702 · have hambient : Continuous fun x : Multiplicative (ZCCompletedGroupAlgebra C H) =>
703 (fun i : ZCCompletedGroupAlgebraIndex C H =>
704 Multiplicative.ofAdd (zcCompletedGroupAlgebraProjection C H i x.toAdd) :
705 ∀ i : ZCCompletedGroupAlgebraIndex C H, S.X i) := by
706 exact continuous_pi fun i =>
707 continuous_ofAdd.comp
708 ((continuous_apply i).comp (continuous_subtype_val.comp continuous_toAdd))
709 exact Continuous.subtype_mk hambient (fun x => by
710 intro i j hij
711 apply Multiplicative.ext
712 exact x.toAdd.2 i j hij)
714omit [IsTopologicalGroup H] in
715/-- The two-parameter completed group-algebra index is directed when `C` is a formation. -/
717 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
718 Directed (· ≤ ·)
719 (id : ZCCompletedGroupAlgebraIndex C H → ZCCompletedGroupAlgebraIndex C H) := by
720 intro i j
721 rcases ProCIntegerIndex.directed_of_formation (C := C) hForm i.1 j.1 with
722 ⟨kcoeff, hki_coeff, hkj_coeff⟩
724 (C := C) (G := H) hForm i.2 j.2 with
725 ⟨kquot, hki_quot, hkj_quot⟩
726 exact ⟨(kcoeff, kquot), ⟨hki_coeff, hki_quot⟩, ⟨hkj_coeff, hkj_quot⟩⟩
728/-- The additive group underlying `Z_C[[H]]`, written multiplicatively, is pro-`C`. -/
730 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
731 ProCGroups.ProC.IsProCGroup C (Multiplicative (ZCCompletedGroupAlgebra C H)) := by
732 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly C) :=
735 hForm.containsTrivialQuotients
736 letI : Nonempty (ProCIntegerIndex C) :=
737 ⟨ProCIntegerIndex.terminal hForm.containsTrivialQuotients⟩
738 letI : Nonempty (CompletedGroupAlgebraIndexInClass H C) :=
739 ⟨_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass (G := H) C⟩
740 letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) := inferInstance
741 let S := zcCompletedGroupAlgebraMultiplicativeSystem C H
742 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, Group (S.X i) := fun i => by
743 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
744 infer_instance
745 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, IsTopologicalGroup (S.X i) := fun i => by
746 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
747 infer_instance
748 letI : ProCGroups.InverseSystems.IsGroupSystem S := by
749 dsimp [S]
750 infer_instance
751 have hS : ProCGroups.ProC.IsProCGroup C S.inverseLimit := by
752 exact ProCGroups.ProC.inverseLimit (S := S)
753 hForm.isomClosed hForm.quotientClosed
755 (fun i => by
756 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
757 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
758 letI : Finite (ZCCompletedGroupAlgebraStage C H i) :=
760 (n := i.1.modulus) (G := H) C
762 letI : Finite (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) :=
763 @Finite.of_equiv _ _ (inferInstance : Finite (ZCCompletedGroupAlgebraStage C H i))
764 Multiplicative.toAdd
765 letI : DiscreteTopology (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) := ⟨rfl⟩
766 exact ProCGroups.ProC.IsProCGroup.of_finite_discrete (C := C)
767 (G := Multiplicative (ZCCompletedGroupAlgebraStage C H i))
768 hForm.quotientClosed
770 C H hForm.isomClosed hForm.finiteProductClosed i.1 i.2))
771 exact ProCGroups.ProC.IsProCGroup.ofContinuousMulEquiv (C := C)
772 hForm.isomClosed hForm.quotientClosed hS
775variable (X : Type u)
777/-- Coordinatewise, the multiplicative version of an additive function group is the product of
778the multiplicative coordinate groups. -/
780 (A : Type u) [AddCommGroup A] [TopologicalSpace A] :
781 Multiplicative (X → A) ≃ₜ* (X → Multiplicative A) where
782 toMulEquiv :=
783 { toFun := fun f x => Multiplicative.ofAdd (f.toAdd x)
784 invFun := fun f => Multiplicative.ofAdd fun x => (f x).toAdd
785 left_inv := by
786 intro f
787 rfl
788 right_inv := by
789 intro f
790 rfl
791 map_mul' := by
792 intro f g
793 rfl }
794 continuous_toFun := by
795 exact continuous_pi fun x =>
796 continuous_ofAdd.comp ((continuous_apply x).comp continuous_toAdd)
797 continuous_invFun := by
798 exact continuous_ofAdd.comp
799 (continuous_pi fun x => continuous_toAdd.comp (continuous_apply x))
801/-- The additive Fox-coordinate group `Z_C[[H]]^X`, written multiplicatively, is pro-`C`. -/
803 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
804 ProCGroups.ProC.IsProCGroup C
805 (Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H))) := by
806 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly C) :=
808 have hPi :
809 ProCGroups.ProC.IsProCGroup C
810 (X → Multiplicative (ZCCompletedGroupAlgebra C H)) :=
812 (C := C) (α := X)
813 (β := fun _ => Multiplicative (ZCCompletedGroupAlgebra C H))
814 hForm
816 (C := C) (H := H) hForm)
817 exact ProCGroups.ProC.IsProCGroup.ofContinuousMulEquiv (C := C)
818 hForm.isomClosed hForm.quotientClosed hPi
819 (multiplicativePiContinuousMulEquiv (X := X)
820 (A := ZCCompletedGroupAlgebra C H)).symm
822end CompletedGroupAlgebraProC
824section SemidirectProC
826variable (C : ProCGroups.FiniteGroupClass.{u})
827variable (X H : Type u) [DecidableEq X]
828variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
830/-- The kernel of the right projection `Z_C[[H]]^X ⋊ H -> H` is the additive coordinate group,
831written multiplicatively. -/
834 Subgroup (ZCCompletedFoxSemidirect C X H)) ≃ₜ*
835 Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H)) where
836 toMulEquiv :=
837 { toFun := fun a => Multiplicative.ofAdd a.1.left
838 invFun := fun v =>
839 ⟨{ left := v.toAdd, right := 1 }, by
840 simp only [ZCCompletedFoxSemidirect.rightMonoidHom, MonoidHom.mem_ker, MonoidHom.coe_mk, OneHom.coe_mk]⟩
841 left_inv := by
842 intro a
843 apply Subtype.ext
844 apply ZCCompletedFoxSemidirect.ext
845 · rfl
846 · change (1 : H) = a.1.right
847 exact a.2.symm
848 right_inv := by
849 intro v
850 rfl
851 map_mul' := by
852 intro a b
853 apply Multiplicative.ext
854 have ha : a.1.right = 1 := by
855 exact a.2
856 simp only [Subgroup.coe_mul, ZCCompletedFoxSemidirect.mul_left, ha, map_one, one_smul, ofAdd_add, toAdd_mul,
857 toAdd_ofAdd]}
858 continuous_toFun := by
859 exact continuous_ofAdd.comp
860 ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_subtype_val)
861 continuous_invFun := by
862 refine Continuous.subtype_mk ?_ (fun v => by
863 simp only [ZCCompletedFoxSemidirect.rightMonoidHom, MonoidHom.mem_ker, MonoidHom.coe_mk, OneHom.coe_mk])
864 rw [continuous_induced_rng]
865 exact continuous_toAdd.prodMk continuous_const
867omit [DecidableEq X] in
868/-- The right-projection kernel in the completed Fox semidirect product is pro-`C`. -/
870 (hForm : ProCGroups.FiniteGroupClass.Formation C) :
871 ProCGroups.ProC.IsProCGroup C
873 Subgroup (ZCCompletedFoxSemidirect C X H)) := by
874 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly C) :=
876 have hcoords :
877 ProCGroups.ProC.IsProCGroup C
878 (Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H))) :=
879 isProCGroup_multiplicative_zcFreeFoxCoordinates (C := C) (X := X) (H := H) hForm
880 exact ProCGroups.ProC.IsProCGroup.ofContinuousMulEquiv (C := C)
881 hForm.isomClosed hForm.quotientClosed hcoords
882 (zcCompletedFoxSemidirectRightKernelEquivCoordinates C X H).symm
884omit [DecidableEq X] in
885/-- The completed Fox semidirect target `Z_C[[H]]^X ⋊ H` is pro-`C` when `H` is pro-`C`. -/
887 (hMel : ProCGroups.FiniteGroupClass.MelnikovFormation C)
888 (hH : ProCGroups.ProC.IsProCGroup C H) :
889 ProCGroups.ProC.IsProCGroup C (ZCCompletedFoxSemidirect C X H) := by
890 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly C) :=
892 letI : CompactSpace H := ProCGroups.ProC.IsProCGroup.compactSpace hH
893 letI : T2Space H := ProCGroups.ProC.IsProCGroup.t2Space hH
894 letI : TotallyDisconnectedSpace H :=
895 ProCGroups.ProC.IsProCGroup.totallyDisconnectedSpace hH
896 let E := ZCCompletedFoxSemidirect C X H
897 let f : E →ₜ* H :=
898 { toMonoidHom := ZCCompletedFoxSemidirect.rightMonoidHom C X H
899 continuous_toFun := continuous_zcCompletedFoxSemidirect_right C X H }
900 let K : Subgroup E := f.toMonoidHom.ker
901 have hE : ProCGroups.IsProfiniteGroup E :=
903 have hK : ProCGroups.ProC.IsProCGroup C K := by
904 dsimp [K, f, E]
906 (C := C) (X := X) (H := H) hMel.formation
907 have hQ : ProCGroups.ProC.IsProCGroup C (E ⧸ K) := by
908 letI : CompactSpace E := ProCGroups.IsProfiniteGroup.compactSpace hE
909 letI : T2Space E := ProCGroups.IsProfiniteGroup.t2Space hE
910 have hf_surj : Function.Surjective f := by
911 intro h
912 exact ⟨{ left := 0, right := h }, rfl⟩
913 let eQuotRange : (E ⧸ K) ≃ₜ* f.toMonoidHom.range := by
914 simpa [K] using ContinuousMonoidHom.quotientKerContinuousMulEquivRange f
915 let eRangeH : f.toMonoidHom.range ≃ₜ* H :=
916 { toMulEquiv :=
917 { toFun := fun x => x.1
918 invFun := fun h => ⟨h, hf_surj h⟩
919 left_inv := by
920 intro x
921 exact Subtype.ext rfl
922 right_inv := by
923 intro h
924 rfl
925 map_mul' := by
926 intro x y
927 rfl }
928 continuous_toFun := continuous_subtype_val
929 continuous_invFun := Continuous.subtype_mk continuous_id (fun h => hf_surj h) }
930 exact ProCGroups.ProC.IsProCGroup.ofContinuousMulEquiv (C := C)
931 hMel.formation.isomClosed hMel.formation.quotientClosed hH
932 (eRangeH.symm.trans eQuotRange.symm)
933 exact ProCGroups.ProC.IsProCGroup.extension (C := C)
934 hMel.formation.isomClosed hMel.formation.quotientClosed hMel.extensionClosed
935 hE K hK hQ
937omit [DecidableEq X] in
938/-- Bundled `ProCGroup` form for the completed Fox semidirect target. -/
940 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
941 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.DeterminedByFiniteQuotients]
942 [ProCGroups.ProC.ProCGroup ProC H] :
944 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H) :=
946 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
948 (C := ProC.finiteQuotientClass) (X := X) (H := H)
949 ProC.finiteQuotientMelnikovFormation
950 (inferInstanceAs (ProCGroups.ProC.ProCGroup ProC H)).isProCGroup)
952end SemidirectProC
954section ClosedGeneratedSemidirectTopology
956variable (X H : Type u) [DecidableEq X]
957variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
959/-- The closed target generated by the Fox graph generators is an all-finite pro-`C` group when
960the ambient completed Fox semidirect target is profinite. -/
962 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] (φ : X → H) :
964 (G :=
966 (ProC := ProCGroups.ProC.allFiniteProC) φ : Subgroup
968 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H))) := by
970 (ProCGroups.IsProfiniteGroup.of_closedSubgroup
971 (G := ZCCompletedFoxSemidirect
972 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
974 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
976 (ProC := ProCGroups.ProC.allFiniteProC) φ))).isProC
978end ClosedGeneratedSemidirectTopology
980end
982end FoxDifferential