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

Source: ProCGroups.FoxDifferential.Completed.Continuous.Topology

1import ProCGroups.FoxDifferential.Completed.FreeProC.SemidirectKernelBasis
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
4/-!
5# Fox differential: completed — continuous — topology
7The principal declarations in this module are:
9- `freeProCZCCompletedFoxBoundary`
10 Source-shaped completed Fox boundary map for a finite generating set. It evaluates a vector of
11 completed Fox coefficients against the generator boundaries \([\varphi(x)]-1\).
12- `zcCompletedFoxSemidirectHomeomorphProd`
13 The completed Fox semidirect target is homeomorphic to its product of components.
14- `continuous_foxBoundaryMap`
15 A finite Fox boundary map is continuous over any topological ring.
16- `continuous_zcCompletedGroupAlgebraProjection`
17 A finite stage projection from \(\mathbb{Z}_C\llbracket G\rrbracket\) is continuous.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
26open scoped BigOperators
28universe u v
30section BoundaryMapContinuity
32variable {R : Type u} [Ring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousMul R]
33variable {X : Type v} [Fintype X]
35/-- A finite Fox boundary map is continuous over any topological ring. -/
36theorem continuous_foxBoundaryMap (generatorBoundary : X → R) :
37 Continuous (foxBoundaryMap generatorBoundary) := by
38 change Continuous (fun v : X → R => ∑ x : X, v x * generatorBoundary x)
39 exact continuous_finsetSum _ fun x _ => (continuous_apply x).mul continuous_const
41end BoundaryMapContinuity
43section CompletedGroupAlgebraTopology
45variable (C : ProCGroups.FiniteGroupClass.{u})
46variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
48/-- Each finite-stage \(\mathbb{Z}_C\)-completed group algebra carries its finite-stage topology. -/
49instance instTopologicalSpaceZCCompletedGroupAlgebraStage
50 (i : ZCCompletedGroupAlgebraIndex C G) :
51 TopologicalSpace (ZCCompletedGroupAlgebraStage C G i) :=
52 ⊥
54/-- Each finite-stage \(\mathbb{Z}_C\)-completed group algebra carries the discrete topology. -/
55instance instDiscreteTopologyZCCompletedGroupAlgebraStage
56 (i : ZCCompletedGroupAlgebraIndex C G) :
57 DiscreteTopology (ZCCompletedGroupAlgebraStage C G i) :=
58 ⟨rfl⟩
60/-- Each finite-stage \(\mathbb{Z}_C\)-completed group algebra is compact. -/
61instance instCompactSpaceZCCompletedGroupAlgebraStage
62 (i : ZCCompletedGroupAlgebraIndex C G) :
63 CompactSpace (ZCCompletedGroupAlgebraStage C G i) := by
64 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
65 letI : Finite (ZCCompletedGroupAlgebraStage C G i) :=
66 finite_modNCompletedGroupAlgebraStageInClass
67 (n := i.1.modulus) (G := G) C
68 i.2
69 letI : Fintype (ZCCompletedGroupAlgebraStage C G i) := Fintype.ofFinite _
70 infer_instance
72/-- Each finite-stage \(\mathbb{Z}_C\)-completed group algebra is a \(T_2\) space. -/
73instance instT2SpaceZCCompletedGroupAlgebraStage
74 (i : ZCCompletedGroupAlgebraIndex C G) :
75 T2Space (ZCCompletedGroupAlgebraStage C G i) :=
76 inferInstance
78/-- Each finite-stage \(\mathbb{Z}_C\)-completed group algebra is totally disconnected. -/
79instance instTotallyDisconnectedSpaceZCCompletedGroupAlgebraStage
80 (i : ZCCompletedGroupAlgebraIndex C G) :
81 TotallyDisconnectedSpace (ZCCompletedGroupAlgebraStage C G i) :=
82 inferInstance
84/-- The completed \(\mathbb{Z}_C\)-group algebra is compact. -/
85instance instCompactSpaceZCCompletedGroupAlgebra :
86 CompactSpace (ZCCompletedGroupAlgebra C G) := by
87 let S := zcCompletedGroupAlgebraSystem C G
88 change CompactSpace S.inverseLimit
89 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
90 inferInstance
91 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, CompactSpace (S.X i) := fun i => by
92 dsimp [S, zcCompletedGroupAlgebraSystem]
93 change @CompactSpace (ZCCompletedGroupAlgebraStage C G i) ⊥
94 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
95 letI : Finite (ZCCompletedGroupAlgebraStage C G i) :=
96 finite_modNCompletedGroupAlgebraStageInClass
97 (n := i.1.modulus) (G := G) C i.2
98 exact Finite.compactSpace
99 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
100 dsimp [S, zcCompletedGroupAlgebraSystem]
101 change @T2Space (ZCCompletedGroupAlgebraStage C G i) ⊥
102 exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩
103 infer_instance
105/-- The completed \(\mathbb{Z}_C\)-group algebra is a \(T_2\) space. -/
106instance instT2SpaceZCCompletedGroupAlgebra :
107 T2Space (ZCCompletedGroupAlgebra C G) := by
108 let S := zcCompletedGroupAlgebraSystem C G
109 change T2Space S.inverseLimit
110 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
111 inferInstance
112 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, T2Space (S.X i) := fun i => by
113 dsimp [S, zcCompletedGroupAlgebraSystem]
114 change @T2Space (ZCCompletedGroupAlgebraStage C G i) ⊥
115 exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩
116 exact S.t2Space_inverseLimit
118/-- A finite stage projection from \(\mathbb{Z}_C\llbracket G\rrbracket\) is continuous. -/
119theorem continuous_zcCompletedGroupAlgebraProjection
120 (i : ZCCompletedGroupAlgebraIndex C G) :
121 Continuous (zcCompletedGroupAlgebraProjection C G i) :=
122 (continuous_apply i).comp continuous_subtype_val
124/--
125A finite stage projection from \(\mathbb{Z}_C\llbracket G\rrbracket\), regarded as a ring
126homomorphism, is continuous.
127-/
128theorem continuous_zcCompletedGroupAlgebraProjectionRingHom
129 (i : ZCCompletedGroupAlgebraIndex C G) :
130 Continuous (zcCompletedGroupAlgebraProjectionRingHom C G i) :=
131 continuous_zcCompletedGroupAlgebraProjection C G i
133/-- The completed \(\mathbb{Z}_C\)-group algebra is totally disconnected. -/
134instance instTotallyDisconnectedSpaceZCCompletedGroupAlgebra :
135 TotallyDisconnectedSpace (ZCCompletedGroupAlgebra C G) := by
136 let S := zcCompletedGroupAlgebraSystem C G
137 change TotallyDisconnectedSpace S.inverseLimit
138 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TopologicalSpace (S.X i) := fun _ =>
139 inferInstance
140 letI : ∀ i : ZCCompletedGroupAlgebraIndex C G, TotallyDisconnectedSpace (S.X i) := fun i => by
141 dsimp [S, zcCompletedGroupAlgebraSystem]
142 change @TotallyDisconnectedSpace (ZCCompletedGroupAlgebraStage C G i) ⊥
143 exact @TotallySeparatedSpace.totallyDisconnectedSpace _ ⊥
144 (@TotallySeparatedSpace.of_discrete _ ⊥ ⟨rfl⟩)
145 exact S.totallyDisconnectedSpace_inverseLimit
147/--
148Addition on \(\mathbb{Z}_C\llbracket H\rrbracket\) is continuous for the inverse-limit topology.
149-/
150instance instContinuousAddZCCompletedGroupAlgebra :
151 ContinuousAdd (ZCCompletedGroupAlgebra C G) where
152 continuous_add := by
153 have hval : Continuous (fun p : ZCCompletedGroupAlgebra C G ×
154 ZCCompletedGroupAlgebra C G =>
155 ((p.1 + p.2 : ZCCompletedGroupAlgebra C G) :
156 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
157 exact continuous_pi fun i =>
158 (continuous_of_discreteTopology :
159 Continuous (fun q : ZCCompletedGroupAlgebraStage C G i ×
160 ZCCompletedGroupAlgebraStage C G i => q.1 + q.2)).comp
161 (((continuous_apply i).comp (continuous_subtype_val.comp continuous_fst)).prodMk
162 ((continuous_apply i).comp (continuous_subtype_val.comp continuous_snd)))
163 convert
164 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
165 (fun p => (p.1 + p.2 : ZCCompletedGroupAlgebra C G).property)) using 1
167/-- Negation on the completed group algebra is continuous for the inverse-limit topology. -/
168instance instContinuousNegZCCompletedGroupAlgebra :
169 ContinuousNeg (ZCCompletedGroupAlgebra C G) where
170 continuous_neg := by
171 change Continuous (fun x : ZCCompletedGroupAlgebra C G => -x)
172 have hval : Continuous (fun x : ZCCompletedGroupAlgebra C G =>
173 ((-x : ZCCompletedGroupAlgebra C G) :
174 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
175 exact continuous_pi fun i =>
176 (continuous_of_discreteTopology :
177 Continuous (fun y : ZCCompletedGroupAlgebraStage C G i => -y)).comp
178 ((continuous_apply i).comp continuous_subtype_val)
179 convert
180 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
181 (fun x => (-x : ZCCompletedGroupAlgebra C G).property)) using 1
183/-- The completed group algebra has addition defined coordinatewise on compatible families. -/
184instance instIsTopologicalAddGroupZCCompletedGroupAlgebra :
185 IsTopologicalAddGroup (ZCCompletedGroupAlgebra C G) where
186 continuous_add := continuous_add
187 continuous_neg := continuous_neg
189/-- Multiplication on the completed group algebra is continuous for the inverse-limit topology. -/
190instance instContinuousMulZCCompletedGroupAlgebra :
191 ContinuousMul (ZCCompletedGroupAlgebra C G) where
192 continuous_mul := by
193 have hval : Continuous (fun p : ZCCompletedGroupAlgebra C G ×
194 ZCCompletedGroupAlgebra C G =>
195 ((p.1 * p.2 : ZCCompletedGroupAlgebra C G) :
196 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
197 exact continuous_pi fun i =>
198 (continuous_of_discreteTopology :
199 Continuous (fun q : ZCCompletedGroupAlgebraStage C G i ×
200 ZCCompletedGroupAlgebraStage C G i => q.1 * q.2)).comp
201 (((continuous_apply i).comp (continuous_subtype_val.comp continuous_fst)).prodMk
202 ((continuous_apply i).comp (continuous_subtype_val.comp continuous_snd)))
203 convert
204 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
205 (fun p => (p.1 * p.2 : ZCCompletedGroupAlgebra C G).property)) using 1
207/-- The completed group algebra inherits a ring structure from the compatible finite-stage rings. -/
208instance instIsTopologicalRingZCCompletedGroupAlgebra :
209 IsTopologicalRing (ZCCompletedGroupAlgebra C G) where
210 continuous_add := continuous_add
211 continuous_mul := continuous_mul
212 continuous_neg := continuous_neg
214/-- Scalar multiplication is continuous for the relevant inverse-limit topology. -/
215instance instContinuousSMulZCCompletedGroupAlgebraSelf :
216 ContinuousSMul (ZCCompletedGroupAlgebra C G) (ZCCompletedGroupAlgebra C G) :=
217 ContinuousMul.to_continuousSMul
219/-- The scalar action map on the completed group algebra is continuous. -/
220theorem continuous_zcCompletedGroupAlgebra_smul :
221 Continuous (fun p : ZCCompletedGroupAlgebra C G × ZCCompletedGroupAlgebra C G =>
222 p.1 • p.2) :=
223 continuous_smul
225/-- The completed group-like map \(G \to \mathbb{Z}_C\llbracket G\rrbracket\) is continuous. -/
226theorem continuous_zcGroupLike : Continuous (zcGroupLike C G) := by
227 have hval : Continuous (fun g : G =>
228 ((zcGroupLike C G g : ZCCompletedGroupAlgebra C G) :
229 (i : ZCCompletedGroupAlgebraIndex C G) → ZCCompletedGroupAlgebraStage C G i)) := by
230 refine continuous_pi fun i => ?_
231 letI : DiscreteTopology (CompletedGroupAlgebraQuotientInClass G C i.2) :=
232 QuotientGroup.discreteTopology
234 ((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G))
235 exact (continuous_of_discreteTopology :
236 Continuous (fun q : CompletedGroupAlgebraQuotientInClass G C i.2 =>
237 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
238 (CompletedGroupAlgebraQuotientInClass G C i.2) q)).comp
239 (continuous_quotient_mk' : Continuous (fun g : G =>
240 QuotientGroup.mk' (((OrderDual.ofDual i.2).1 : OpenNormalSubgroup G) : Subgroup G) g))
241 simpa [Subtype.eta] using
242 (Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C G) hval
243 (fun g => (zcGroupLike C G g : ZCCompletedGroupAlgebra C G).property))
245/--
246The completed augmentation \(\mathbb{Z}_C\llbracket G\rrbracket \to \mathbb{Z}_C\) is continuous
247in the inverse-limit topology.
248-/
249theorem continuous_zcCompletedGroupAlgebraAugmentation
251 Continuous (zcCompletedGroupAlgebraAugmentation C G) := by
252 have hval : Continuous (fun x : ZCCompletedGroupAlgebra C G =>
253 (zcCompletedGroupAlgebraAugmentation C G x :
254 (i : ProCIntegerIndex C) → ProCIntegerStage C i)) := by
255 refine continuous_pi fun i => ?_
256 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
257 let U := zcCompletedGroupAlgebraTopIndex C G
258 letI : TopologicalSpace (ModNCompletedGroupAlgebraStageInClass i.modulus G C U) := ⊥
259 letI : DiscreteTopology (ModNCompletedGroupAlgebraStageInClass i.modulus G C U) := ⟨rfl⟩
260 exact
261 (continuous_of_discreteTopology :
262 Continuous (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus G C U)).comp
263 ((continuous_apply (i, U)).comp continuous_subtype_val)
264 simpa [zcCompletedGroupAlgebraAugmentation, Subtype.eta] using
265 (Continuous.subtype_mk (p := ProCIntegerCompatible C) hval
266 (fun x => (zcCompletedGroupAlgebraAugmentation C G x).property))
268/-- The completed augmentation ideal is closed in \(\mathbb{Z}_C\llbracket G\rrbracket\). -/
269theorem isClosed_zcCompletedGroupAlgebraAugmentationIdeal
271 IsClosed
272 ((zcCompletedGroupAlgebraAugmentationIdeal C G :
273 Ideal (ZCCompletedGroupAlgebra C G)) : Set (ZCCompletedGroupAlgebra C G)) := by
274 change IsClosed ((zcCompletedGroupAlgebraAugmentation C G) ⁻¹' ({0} : Set (ZCCoeff C)))
275 exact isClosed_singleton.preimage
276 (continuous_zcCompletedGroupAlgebraAugmentation (C := C) (G := G))
278/-- The completed \(\mathbb{Z}_C\)-group algebra augmentation ideal is compact. -/
279instance instCompactSpaceZCCompletedGroupAlgebraAugmentationIdeal
281 CompactSpace (ZCCompletedGroupAlgebraAugmentationIdeal C G) := by
282 exact
283 (isClosed_zcCompletedGroupAlgebraAugmentationIdeal
284 (C := C) (G := G)).isClosedEmbedding_subtypeVal.compactSpace
286/-- The completed \(\mathbb{Z}_C\)-group algebra augmentation ideal is a \(T_2\) space. -/
287instance instT2SpaceZCCompletedGroupAlgebraAugmentationIdeal
289 T2Space (ZCCompletedGroupAlgebraAugmentationIdeal C G) :=
290 inferInstance
292variable {A : Type v} [Group A] [TopologicalSpace A]
294/--
295The completed group-algebra boundary \(a \mapsto [\psi(a)] - 1\) is continuous whenever \(\psi\)
296is continuous.
297-/
298theorem continuous_zcCompletedGroupAlgebraBoundary
299 (ψ : A →* G) (hψ : Continuous ψ) :
300 Continuous (zcCompletedGroupAlgebraBoundary C ψ) := by
301 convert
302 ((continuous_zcGroupLike (C := C) (G := G)).comp hψ).sub continuous_const using 1 <;>
303 rfl
305variable {X : Type v} [Fintype X] [DecidableEq X]
307omit [DecidableEq X] in
308/-- The completed \(\mathbb{Z}_C\llbracket G\rrbracket\) Fox boundary/Euler map is continuous. -/
309theorem continuous_zcFreeGroupFoxBoundary (ψ : FreeGroup X →* G) :
310 Continuous (zcFreeGroupFoxBoundary C ψ) := by
311 classical
312 rw [zcFreeGroupFoxBoundary_eq_foxBoundaryMap]
313 exact continuous_foxBoundaryMap _
315end CompletedGroupAlgebraTopology
317section CompletedSourceBoundary
319variable (C : ProCGroups.FiniteGroupClass.{u})
320variable {X H : Type u} [Fintype X]
321variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
323/--
324Source-shaped completed Fox boundary map for a finite generating set. It evaluates a vector of
325completed Fox coefficients against the generator boundaries \([\varphi(x)]-1\).
326-/
327def freeProCZCCompletedFoxBoundary (φ : X → H) :
328 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
329 ZCCompletedGroupAlgebra C H :=
330 foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1)
333/--
334The boundary map is evaluated on the canonical generators and then extended linearly to the
335completed coordinate module.
336-/
337theorem freeProCZCCompletedFoxBoundary_apply
338 (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
339 freeProCZCCompletedFoxBoundary C φ v =
340 ∑ x : X, v x * (zcGroupLike C H (φ x) - 1) :=
341 rfl
343variable [DecidableEq X]
346/--
347The source-shaped completed Fox boundary map sends the standard basis vector at \(x\) to
348\([\varphi(x)]-1\).
349-/
350@[simp]
351theorem freeProCZCCompletedFoxBoundary_single
352 (φ : X → H) (x : X) :
353 freeProCZCCompletedFoxBoundary C φ
354 (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) =
355 zcGroupLike C H (φ x) - 1 := by
356 simp only [freeProCZCCompletedFoxBoundary, foxBoundaryMap_single]
358omit [DecidableEq X] in
359/-- The source-shaped completed Fox boundary map is continuous for finite generating sets. -/
360theorem continuous_freeProCZCCompletedFoxBoundary (φ : X → H) :
361 Continuous (freeProCZCCompletedFoxBoundary C φ) :=
362 continuous_foxBoundaryMap _
364omit [DecidableEq X] in
365/--
366The source-shaped completed Fox boundary has image equal to the submodule generated by the
367augmentation generators \([\varphi(x)]-1\).
368-/
369theorem freeProCZCCompletedFoxBoundary_range
370 (φ : X → H) :
371 (freeProCZCCompletedFoxBoundary C φ).range =
372 Submodule.span (ZCCompletedGroupAlgebra C H)
373 (Set.range fun x : X => zcGroupLike C H (φ x) - 1) := by
374 classical
375 apply le_antisymm
376 · rintro y ⟨v, rfl⟩
377 rw [freeProCZCCompletedFoxBoundary_apply]
378 exact Submodule.sum_mem _ fun x _ =>
379 Submodule.smul_mem _ (v x)
380 (Submodule.subset_span (Set.mem_range_self x))
381 · refine Submodule.span_le.2 ?_
382 rintro y ⟨x, rfl⟩
383 exact ⟨Pi.single x (1 : ZCCompletedGroupAlgebra C H), by simp only
384 [freeProCZCCompletedFoxBoundary_single]⟩
386omit [DecidableEq X] in
387/--
388If the chosen finite source hits every element of H, the source-shaped completed Fox boundary
389has image equal to the algebraic standard-generator ideal.
390-/
391theorem freeProCZCCompletedFoxBoundary_range_eq_standardAugmentationIdeal_of_surjective
392 (φ : X → H) (hφ : Function.Surjective φ) :
393 (freeProCZCCompletedFoxBoundary C φ).range =
394 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
395 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
396 rw [freeProCZCCompletedFoxBoundary_range,
397 zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span]
398 congr 1
399 ext y
400 constructor
401 · rintro ⟨x, rfl⟩
402 exact ⟨φ x, rfl⟩
403 · rintro ⟨h, rfl⟩
404 rcases hφ h with ⟨x, rfl⟩
405 exact ⟨x, rfl⟩
407end CompletedSourceBoundary
409section SemidirectTopology
411variable (C : ProCGroups.FiniteGroupClass.{v})
412variable (X : Type u) [DecidableEq X]
413variable (H : Type v) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
415/-- The completed Fox semidirect product carries the inverse-limit topological space structure. -/
416instance instTopologicalSpaceZCCompletedFoxSemidirect :
417 TopologicalSpace (ZCCompletedFoxSemidirect C X H) :=
418 TopologicalSpace.induced
419 (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) inferInstance
421/-- The completed Fox semidirect target is homeomorphic to its product of components. -/
422def zcCompletedFoxSemidirectHomeomorphProd :
423 ZCCompletedFoxSemidirect C X H ≃ₜ (ZCFreeFoxCoordinates C (X := X) (H := H) × H) where
424 toEquiv :=
425 { toFun := fun a => (a.left, a.right)
426 invFun := fun p => { left := p.1, right := p.2 }
427 left_inv := by
428 intro a
429 cases a
430 rfl
431 right_inv := by
432 intro p
433 cases p
434 rfl }
435 continuous_toFun := continuous_induced_dom
436 continuous_invFun := by
437 rw [continuous_induced_rng]
438 exact continuous_id
440omit [DecidableEq X] in
441/-- The component-pair map from the semidirect target is continuous. -/
442theorem continuous_zcCompletedFoxSemidirect_toProd :
443 Continuous (fun a : ZCCompletedFoxSemidirect C X H => (a.left, a.right)) :=
444 continuous_induced_dom
446omit [DecidableEq X] in
447/-- The Fox-coordinate projection from the semidirect target is continuous. -/
448theorem continuous_zcCompletedFoxSemidirect_left :
449 Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.left) :=
450 continuous_fst.comp (continuous_zcCompletedFoxSemidirect_toProd C X H)
452omit [DecidableEq X] in
453/-- The group projection from the semidirect target is continuous. -/
454theorem continuous_zcCompletedFoxSemidirect_right :
455 Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.right) :=
456 continuous_snd.comp (continuous_zcCompletedFoxSemidirect_toProd C X H)
458/-- The completed Fox semidirect product is compact as an inverse limit of finite stages. -/
459instance instCompactSpaceZCCompletedFoxSemidirect [CompactSpace H] :
460 CompactSpace (ZCCompletedFoxSemidirect C X H) := by
461 exact (zcCompletedFoxSemidirectHomeomorphProd C X H).symm.compactSpace
463/-- The completed Fox semidirect product is Hausdorff for the inverse-limit topology. -/
464instance instT2SpaceZCCompletedFoxSemidirect [T2Space H] :
465 T2Space (ZCCompletedFoxSemidirect C X H) := by
466 exact (zcCompletedFoxSemidirectHomeomorphProd C X H).symm.t2Space
468/--
469The completed Fox semidirect product is totally disconnected as an inverse limit of finite
470discrete stages.
471-/
472instance instTotallyDisconnectedSpaceZCCompletedFoxSemidirect [TotallyDisconnectedSpace H] :
473 TotallyDisconnectedSpace (ZCCompletedFoxSemidirect C X H) := by
474 exact (zcCompletedFoxSemidirectHomeomorphProd C X H).symm.totallyDisconnectedSpace
476/-- The completed Fox semidirect product is a topological group for the inverse-limit topology. -/
477instance instIsTopologicalGroupZCCompletedFoxSemidirect :
478 IsTopologicalGroup (ZCCompletedFoxSemidirect C X H) where
479 continuous_mul := by
480 rw [continuous_induced_rng]
481 have hleft : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
482 ZCCompletedFoxSemidirect C X H => (p.1 * p.2).left) := by
483 refine continuous_pi fun x => ?_
484 have hleftA : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
485 ZCCompletedFoxSemidirect C X H => p.1.left x) :=
486 (continuous_apply x).comp
487 ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_fst)
488 have hrightA : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
489 ZCCompletedFoxSemidirect C X H => p.2.left x) :=
490 (continuous_apply x).comp
491 ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_snd)
492 have hgroup : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
493 ZCCompletedFoxSemidirect C X H => zcGroupLike C H p.1.right) :=
494 (continuous_zcGroupLike (C := C) (G := H)).comp
495 ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_fst)
496 change Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
497 ZCCompletedFoxSemidirect C X H =>
498 p.1.left x + zcGroupLike C H p.1.right * p.2.left x)
499 exact hleftA.add (hgroup.mul hrightA)
500 have hright : Continuous (fun p : ZCCompletedFoxSemidirect C X H ×
501 ZCCompletedFoxSemidirect C X H => (p.1 * p.2).right) := by
502 exact ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_fst).mul
503 ((continuous_zcCompletedFoxSemidirect_right C X H).comp continuous_snd)
504 exact hleft.prodMk hright
505 continuous_inv := by
506 rw [continuous_induced_rng]
507 have hleft : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a⁻¹.left) := by
508 refine continuous_pi fun x => ?_
509 have hleftA : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a.left x) :=
510 (continuous_apply x).comp (continuous_zcCompletedFoxSemidirect_left C X H)
511 have hgroup : Continuous (fun a : ZCCompletedFoxSemidirect C X H =>
512 zcGroupLike C H a.right⁻¹) :=
513 (continuous_zcGroupLike (C := C) (G := H)).comp
514 ((continuous_zcCompletedFoxSemidirect_right C X H).inv)
515 change Continuous (fun a : ZCCompletedFoxSemidirect C X H =>
516 -(zcGroupLike C H a.right⁻¹ * a.left x))
517 exact (hgroup.mul hleftA).neg
518 have hright : Continuous (fun a : ZCCompletedFoxSemidirect C X H => a⁻¹.right) := by
519 exact (continuous_zcCompletedFoxSemidirect_right C X H).inv
520 exact hleft.prodMk hright
522end SemidirectTopology
524section CompletedGroupAlgebraProC
526variable (C : ProCGroups.FiniteGroupClass.{u})
527variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
529/--
530One finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\), viewed multiplicatively through its additive
531group, belongs to \(C\).
532-/
533theorem finiteGroupClass_multiplicative_modNCompletedGroupAlgebraStageInClass_mem
536 (i : ProCIntegerIndex C) (U : CompletedGroupAlgebraIndexInClass H C) :
537 C (Multiplicative (ModNCompletedGroupAlgebraStageInClass i.modulus H C U)) := by
538 classical
539 letI : Fact (0 < i.modulus) := ⟨i.positive⟩
540 let Q := CompletedGroupAlgebraQuotientInClass H C U
541 letI : Finite Q := ProCGroups.FiniteGroupClass.finite (C := C) (OrderDual.ofDual U).2
542 letI : Fintype Q := Fintype.ofFinite Q
543 let e :
544 Multiplicative (ModNCompletedGroupAlgebraStageInClass i.modulus H C U) ≃*
545 (Q → ULift.{u} (Multiplicative (ModNCompletedCoeff i.modulus))) :=
546 { toFun := fun a q =>
547 ULift.up (Multiplicative.ofAdd ((Finsupp.equivFunOnFinite a.toAdd.coeff) q))
548 invFun := fun f =>
549 Multiplicative.ofAdd
550 (MonoidAlgebra.ofCoeff
551 (Finsupp.equivFunOnFinite.symm fun q => (f q).down.toAdd))
552 left_inv := by
553 intro a
554 apply Multiplicative.ext
555 apply MonoidAlgebra.coeff_injective
556 exact Finsupp.equivFunOnFinite.left_inv a.toAdd.coeff
557 right_inv := by
558 intro f
559 funext q
560 have hcoeff :
561 (Finsupp.equivFunOnFinite
562 (Finsupp.equivFunOnFinite.symm fun q => (f q).down.toAdd)) q =
563 (f q).down.toAdd := by
564 exact congrFun
565 (Finsupp.equivFunOnFinite.right_inv
566 (fun q => (f q).down.toAdd)) q
567 apply ULift.ext
568 apply Multiplicative.ext
569 exact hcoeff
570 map_mul' := by
571 intro a b
572 funext q
573 apply ULift.ext
574 apply Multiplicative.ext
575 rfl }
576 have hPi :
577 C (Q → ULift.{u} (Multiplicative (ModNCompletedCoeff i.modulus))) := by
578 exact hProd (ι := Q)
579 (G := fun _ => ULift.{u} (Multiplicative (ModNCompletedCoeff i.modulus)))
580 (fun _ => by
581 apply C.mem_of_memAcrossUniverses
582 apply (C.memAcrossUniverses_ulift_iff
583 (Multiplicative (ModNCompletedCoeff i.modulus))).2
584 simpa [ModNCompletedCoeff, ProCIntegerStage] using i.cyclic_mem)
585 exact hIso ⟨e.symm⟩ hPi
587/--
588The group-valued inverse system underlying the additive group of \(\mathbb{Z}_C\llbracket
589H\rrbracket\), written multiplicatively.
590-/
591def zcCompletedGroupAlgebraMultiplicativeSystem :
592 ProCGroups.InverseSystems.InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
593 X := fun i => Multiplicative (ZCCompletedGroupAlgebraStage C H i)
594 topologicalSpace := fun _ => ⊥
595 map := fun {i j} hij =>
596 (zcCompletedGroupAlgebraTransition C H hij).toAddMonoidHom.toMultiplicative
597 continuous_map := by
598 intro i j hij
599 exact continuous_bot
600 map_id := by
601 intro i
602 funext x
603 apply Multiplicative.ext
604 change zcCompletedGroupAlgebraTransition C H (le_rfl : i ≤ i) x.toAdd = x.toAdd
605 simp only [zcCompletedGroupAlgebraTransition_id, RingHom.id_apply]
606 map_comp := by
607 intro i j k hij hjk
608 funext x
609 apply Multiplicative.ext
610 change
611 zcCompletedGroupAlgebraTransition C H hij
612 (zcCompletedGroupAlgebraTransition C H hjk x.toAdd) =
613 zcCompletedGroupAlgebraTransition C H (hij.trans hjk) x.toAdd
614 exact congrArg (fun f : ZCCompletedGroupAlgebraStage C H k →+*
615 ZCCompletedGroupAlgebraStage C H i => f x.toAdd)
616 (zcCompletedGroupAlgebraTransition_comp C H hij hjk)
618/-- Each stage of the multiplicative system carries the discrete topology selected by the system. -/
619instance instDiscreteTopologyZCCompletedGroupAlgebraMultiplicativeSystemStage
620 (i : ZCCompletedGroupAlgebraIndex C H) :
621 DiscreteTopology ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i) :=
622 ⟨rfl⟩
624/-- Each stage of the multiplicative system is finite. -/
625instance instFiniteZCCompletedGroupAlgebraMultiplicativeSystemStage
626 (i : ZCCompletedGroupAlgebraIndex C H) :
627 Finite ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i) := by
628 dsimp [zcCompletedGroupAlgebraMultiplicativeSystem]
629 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
630 letI : Finite (ZCCompletedGroupAlgebraStage C H i) :=
631 finite_modNCompletedGroupAlgebraStageInClass
632 (n := i.1.modulus) (G := H) C i.2
633 exact @Finite.of_equiv _ _ (inferInstance : Finite (ZCCompletedGroupAlgebraStage C H i))
634 Multiplicative.toAdd
636/-- Each finite-stage group algebra in the multiplicative system carries its group structure. -/
637instance instGroupZCCompletedGroupAlgebraMultiplicativeSystemStage
638 (i : ZCCompletedGroupAlgebraIndex C H) :
639 Group ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i) := by
640 dsimp [zcCompletedGroupAlgebraMultiplicativeSystem]
641 infer_instance
643/-- Each finite-stage group algebra in the multiplicative system is a topological group. -/
644instance instIsTopologicalGroupZCCompletedGroupAlgebraMultiplicativeSystemStage
645 (i : ZCCompletedGroupAlgebraIndex C H) :
646 IsTopologicalGroup ((zcCompletedGroupAlgebraMultiplicativeSystem C H).X i) := by
647 exact
648 { continuous_mul := continuous_of_discreteTopology
649 continuous_inv := continuous_of_discreteTopology }
651/-- The multiplicative finite-stage group-algebra system is group-valued. -/
652instance instIsGroupSystemZCCompletedGroupAlgebraMultiplicativeSystem :
654 (zcCompletedGroupAlgebraMultiplicativeSystem C H) where
655 map_one := by
656 intro i j hij
657 apply Multiplicative.ext
658 change zcCompletedGroupAlgebraTransition C H hij 0 = 0
659 exact map_zero _
660 map_mul := by
661 intro i j hij x y
662 change Multiplicative (ZCCompletedGroupAlgebraStage C H j) at x y
663 apply Multiplicative.ext
664 change zcCompletedGroupAlgebraTransition C H hij (x.toAdd + y.toAdd) =
665 zcCompletedGroupAlgebraTransition C H hij x.toAdd +
666 zcCompletedGroupAlgebraTransition C H hij y.toAdd
667 exact map_add _ _ _
668 map_inv := by
669 intro i j hij x
670 change Multiplicative (ZCCompletedGroupAlgebraStage C H j) at x
671 apply Multiplicative.ext
672 change zcCompletedGroupAlgebraTransition C H hij (-x.toAdd) =
673 -zcCompletedGroupAlgebraTransition C H hij x.toAdd
674 exact (zcCompletedGroupAlgebraTransition C H hij).map_neg x.toAdd
676/--
677The multiplicative inverse limit of the finite completed group-algebra stages is the additive
678group underlying \(\mathbb{Z}_C\llbracket H\rrbracket\), written multiplicatively.
679-/
680def zcCompletedGroupAlgebraMultiplicativeLimitEquiv :
681 (zcCompletedGroupAlgebraMultiplicativeSystem C H).inverseLimit ≃ₜ*
682 Multiplicative (ZCCompletedGroupAlgebra C H) := by
683 let S := zcCompletedGroupAlgebraMultiplicativeSystem C H
684 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, Group (S.X i) := fun i => by
685 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
686 infer_instance
688 dsimp [S]
689 infer_instance
690 refine
691 { toMulEquiv := ?_
692 continuous_toFun := ?_
693 continuous_invFun := ?_ }
694 · refine
695 { toFun := fun x =>
696 Multiplicative.ofAdd
697 (⟨fun i => (S.projection i x).toAdd, by
698 intro i j hij
699 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij)⟩ :
700 ZCCompletedGroupAlgebra C H)
701 invFun := fun x =>
702 (⟨fun i =>
703 Multiplicative.ofAdd
704 (zcCompletedGroupAlgebraProjection C H i x.toAdd), by
705 intro i j hij
706 apply Multiplicative.ext
707 exact x.toAdd.2 i j hij⟩ :
708 S.inverseLimit)
709 left_inv := by
710 intro x
711 apply S.ext
712 intro i
713 rfl
714 right_inv := by
715 intro x
716 apply Multiplicative.ext
717 ext i
718 rfl
719 map_mul' := by
720 intro x y
721 apply Multiplicative.ext
722 ext i
723 rfl }
724 · refine continuous_ofAdd.comp ?_
725 have hambient : Continuous fun x : S.inverseLimit =>
726 (fun i : ZCCompletedGroupAlgebraIndex C H => (S.projection i x).toAdd :
727 ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i) := by
728 exact continuous_pi fun i => continuous_toAdd.comp (S.continuous_projection i)
729 exact Continuous.subtype_mk hambient (fun x => by
730 intro i j hij
731 exact congrArg Multiplicative.toAdd (S.projection_compatible x i j hij))
732 · have hambient : Continuous fun x : Multiplicative (ZCCompletedGroupAlgebra C H) =>
733 (fun i : ZCCompletedGroupAlgebraIndex C H =>
734 Multiplicative.ofAdd (zcCompletedGroupAlgebraProjection C H i x.toAdd) :
735 ∀ i : ZCCompletedGroupAlgebraIndex C H, S.X i) := by
736 exact continuous_pi fun i =>
737 continuous_ofAdd.comp
738 ((continuous_apply i).comp (continuous_subtype_val.comp continuous_toAdd))
739 exact Continuous.subtype_mk hambient (fun x => by
740 intro i j hij
741 apply Multiplicative.ext
742 exact x.toAdd.2 i j hij)
744omit [IsTopologicalGroup H] in
745/-- The two-parameter completed group-algebra index is directed when \(C\) is a formation. -/
746theorem directed_zcCompletedGroupAlgebraIndex_of_formation
748 Directed (· ≤ ·)
749 (id : ZCCompletedGroupAlgebraIndex C H → ZCCompletedGroupAlgebraIndex C H) := by
750 intro i j
751 rcases ProCIntegerIndex.directed_of_formation (C := C) hForm i.1 j.1 with
752 ⟨kcoeff, hki_coeff, hkj_coeff⟩
754 (C := C) (G := H) hForm i.2 j.2 with
755 ⟨kquot, hki_quot, hkj_quot⟩
756 exact ⟨(kcoeff, kquot), ⟨hki_coeff, hki_quot⟩, ⟨hkj_coeff, hkj_quot⟩⟩
758/-- The additive group underlying \(\mathbb{Z}_C\llbracket H\rrbracket\), written multiplicatively,
759has an open-normal \(C\)-basis. -/
760theorem hasOpenNormalBasisInClass_multiplicative_zcCompletedGroupAlgebra
762 ProCGroups.ProC.HasOpenNormalBasisInClass C (Multiplicative (ZCCompletedGroupAlgebra C
763 H)) := by
765 hForm.containsTrivialQuotients
766 letI : Nonempty (ProCIntegerIndex C) :=
767 ⟨ProCIntegerIndex.terminal hForm.containsTrivialQuotients⟩
768 letI : Nonempty (CompletedGroupAlgebraIndexInClass H C) :=
769 ⟨_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndexInClass (G := H) C⟩
770 letI : Nonempty (ZCCompletedGroupAlgebraIndex C H) := inferInstance
771 let S := zcCompletedGroupAlgebraMultiplicativeSystem C H
772 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, Group (S.X i) := fun i => by
773 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
774 infer_instance
775 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, IsTopologicalGroup (S.X i) := fun i => by
776 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
777 exact instIsTopologicalGroupZCCompletedGroupAlgebraMultiplicativeSystemStage C H i
778 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, CompactSpace (S.X i) := fun i => by
779 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
780 letI : DiscreteTopology (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) := ⟨rfl⟩
781 letI : Finite (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) :=
782 instFiniteZCCompletedGroupAlgebraMultiplicativeSystemStage C H i
783 infer_instance
784 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, T2Space (S.X i) := fun i => by
785 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
786 change @T2Space (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) ⊥
787 exact @DiscreteTopology.toT2Space _ ⊥ ⟨rfl⟩
788 letI : ∀ i : ZCCompletedGroupAlgebraIndex C H, TotallyDisconnectedSpace (S.X i) := fun i => by
789 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
790 change @TotallyDisconnectedSpace
791 (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) ⊥
792 exact @TotallySeparatedSpace.totallyDisconnectedSpace _ ⊥
793 (@TotallySeparatedSpace.of_discrete _ ⊥ ⟨rfl⟩)
795 dsimp [S]
796 infer_instance
797 have hS : ProCGroups.ProC.HasOpenNormalBasisInClass C (S.inverseLimit) := by
799 hForm.isomClosed hForm.quotientClosed
800 (directed_zcCompletedGroupAlgebraIndex_of_formation C H hForm)
801 (fun i => by
802 dsimp [S, zcCompletedGroupAlgebraMultiplicativeSystem]
803 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
804 letI : Finite (ZCCompletedGroupAlgebraStage C H i) :=
805 finite_modNCompletedGroupAlgebraStageInClass
806 (n := i.1.modulus) (G := H) C
807 i.2
808 letI : Finite (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) :=
809 @Finite.of_equiv _ _ (inferInstance : Finite (ZCCompletedGroupAlgebraStage C H i))
810 Multiplicative.toAdd
811 letI : DiscreteTopology (Multiplicative (ZCCompletedGroupAlgebraStage C H i)) := ⟨rfl⟩
813 (G := Multiplicative (ZCCompletedGroupAlgebraStage C H i))
814 hForm.quotientClosed
815 (finiteGroupClass_multiplicative_modNCompletedGroupAlgebraStageInClass_mem
816 C H hForm.isomClosed hForm.finiteProductClosed i.1 i.2))
818 (zcCompletedGroupAlgebraMultiplicativeLimitEquiv C H)
820variable (X : Type u)
822/--
823Coordinatewise, the multiplicative version of an additive function group is the product of the
824multiplicative coordinate groups.
825-/
826def multiplicativePiContinuousMulEquiv
827 (A : Type u) [AddCommGroup A] [TopologicalSpace A] :
828 Multiplicative (X → A) ≃ₜ* (X → Multiplicative A) where
829 toMulEquiv :=
830 { toFun := fun f x => Multiplicative.ofAdd (f.toAdd x)
831 invFun := fun f => Multiplicative.ofAdd fun x => (f x).toAdd
832 left_inv := by
833 intro f
834 rfl
835 right_inv := by
836 intro f
837 rfl
838 map_mul' := by
839 intro f g
840 rfl }
841 continuous_toFun := by
842 exact continuous_pi fun x =>
843 continuous_ofAdd.comp ((continuous_apply x).comp continuous_toAdd)
844 continuous_invFun := by
845 exact continuous_ofAdd.comp
846 (continuous_pi fun x => continuous_toAdd.comp (continuous_apply x))
848/-- The additive Fox-coordinate group \(\mathbb{Z}_C\llbracket H\rrbracket^{X}\), written
849multiplicatively, has an open-normal \(C\)-basis. -/
850theorem hasOpenNormalBasisInClass_multiplicative_zcFreeFoxCoordinates
852 (Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H))) := by
853 letI : T2Space (Multiplicative (ZCCompletedGroupAlgebra C H)) := by
854 change T2Space (ZCCompletedGroupAlgebra C H)
855 infer_instance
856 letI : TotallyDisconnectedSpace
857 (Multiplicative (ZCCompletedGroupAlgebra C H)) := by
858 change TotallyDisconnectedSpace (ZCCompletedGroupAlgebra C H)
859 infer_instance
861 (X → Multiplicative (ZCCompletedGroupAlgebra C H)) :=
863 (C := C) (α := X)
864 (β := fun _ => Multiplicative (ZCCompletedGroupAlgebra C H))
865 hForm
866 (fun _ => hasOpenNormalBasisInClass_multiplicative_zcCompletedGroupAlgebra
867 (C := C) (H := H) hForm)
869 (multiplicativePiContinuousMulEquiv (X := X)
870 (A := ZCCompletedGroupAlgebra C H)).symm
872end CompletedGroupAlgebraProC
874section SemidirectProC
876variable (C : ProCGroups.FiniteGroupClass.{u})
877variable (X H : Type u) [DecidableEq X]
878variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
880/--
881The kernel of the right projection \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H \to H\) is
882the additive coordinate group, written multiplicatively.
883-/
884def zcCompletedFoxSemidirectRightKernelEquivCoordinates :
885 ((ZCCompletedFoxSemidirect.rightMonoidHom C X H).ker :
886 Subgroup (ZCCompletedFoxSemidirect C X H)) ≃ₜ*
887 Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H)) where
888 toMulEquiv :=
889 { toFun := fun a => Multiplicative.ofAdd a.1.left
890 invFun := fun v =>
891 ⟨{ left := v.toAdd, right := 1 }, by
892 simp only [ZCCompletedFoxSemidirect.rightMonoidHom, MonoidHom.mem_ker,
893 MonoidHom.coe_mk, OneHom.coe_mk]⟩
894 left_inv := by
895 intro a
896 apply Subtype.ext
897 apply ZCCompletedFoxSemidirect.ext
898 · rfl
899 · change (1 : H) = a.1.right
900 exact a.2.symm
901 right_inv := by
902 intro v
903 rfl
904 map_mul' := by
905 intro a b
906 apply Multiplicative.ext
907 have ha : a.1.right = 1 := by
908 exact a.2
909 simp only [Subgroup.coe_mul, ZCCompletedFoxSemidirect.mul_left, ha, map_one, one_smul,
910 ofAdd_add, toAdd_mul,
911 toAdd_ofAdd]}
912 continuous_toFun := by
913 exact continuous_ofAdd.comp
914 ((continuous_zcCompletedFoxSemidirect_left C X H).comp continuous_subtype_val)
915 continuous_invFun := by
916 refine Continuous.subtype_mk ?_ (fun v => by
917 simp only [ZCCompletedFoxSemidirect.rightMonoidHom, MonoidHom.mem_ker, MonoidHom.coe_mk,
918 OneHom.coe_mk])
919 rw [continuous_induced_rng]
920 exact continuous_toAdd.prodMk continuous_const
922omit [DecidableEq X] in
923/-- The right-projection kernel in the completed Fox semidirect product has an open-normal
924\(C\)-basis. -/
925theorem hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_rightKernel
927 ((ZCCompletedFoxSemidirect.rightMonoidHom C X H).ker :
928 Subgroup (ZCCompletedFoxSemidirect C X H)) := by
930 (Multiplicative (ZCFreeFoxCoordinates C (X := X) (H := H))) :=
931 hasOpenNormalBasisInClass_multiplicative_zcFreeFoxCoordinates (C := C) (X := X) (H := H) hForm
933 (zcCompletedFoxSemidirectRightKernelEquivCoordinates C X H).symm
935omit [DecidableEq X] in
936/-- The completed Fox semidirect target
937\(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\) has an open-normal \(C\)-basis when \(H\)
938does. -/
939theorem hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_of_hasOpenNormalBasisInClass
940 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
943 ProCGroups.ProC.HasOpenNormalBasisInClass C (ZCCompletedFoxSemidirect C X H) := by
944 let E := ZCCompletedFoxSemidirect C X H
945 let f : E →ₜ* H :=
946 { toMonoidHom := ZCCompletedFoxSemidirect.rightMonoidHom C X H
947 continuous_toFun := continuous_zcCompletedFoxSemidirect_right C X H }
948 let K : Subgroup E := f.toMonoidHom.ker
950 dsimp [K, f, E]
951 exact hasOpenNormalBasisInClass_zcCompletedFoxSemidirect_rightKernel
952 (C := C) (X := X) (H := H) hMel.formation
954 have hf_surj : Function.Surjective f := by
955 intro h
956 exact ⟨{ left := 0, right := h }, rfl⟩
957 let eQuotRange : (E ⧸ K) ≃ₜ* f.toMonoidHom.range := by
959 let eRangeH : f.toMonoidHom.range ≃ₜ* H :=
960 { toMulEquiv :=
961 { toFun := fun x => x.1
962 invFun := fun h => ⟨h, hf_surj h⟩
963 left_inv := by
964 intro x
965 exact Subtype.ext rfl
966 right_inv := by
967 intro h
968 rfl
969 map_mul' := by
970 intro x y
971 rfl }
972 continuous_toFun := continuous_subtype_val
973 continuous_invFun := Continuous.subtype_mk continuous_id (fun h => hf_surj h) }
975 (eRangeH.symm.trans eQuotRange.symm)
977 hMel.formation.isomClosed hMel.formation.quotientClosed hMel.extensionClosed
980end SemidirectProC
982end
984end FoxDifferential