Source: ProCGroups.FoxDifferential.Completed.Continuous.TopologicalGeneration
1import ProCGroups.FoxDifferential.Completed.Continuous.Topology
2import ProCGroups.ProC.Kernels
4/-!
5# Continuous Fox formulas from topological generators
7Continuous crossed homomorphisms into Hausdorff targets are determined by their values on a
8topologically generating set. This module applies that principle to bundled completed Fox
9differentials: it constructs their kernel restrictions, compares the resulting kernel map with
10the topological abelianization, derives closed-commutator criteria, and proves the completed
11fundamental and Euler formulas from generator values.
13The free pro-\(C\) specializations are parameterized by the canonical finite-group class `C`;
14there is no predicate-to-class conversion or raw crossed-differential compatibility layer.
15-/
17namespace FoxDifferential
19noncomputable section
21open scoped BigOperators
22open ProCGroups.Generation
23open ProCGroups.ProC
25universe u v
27namespace CrossedHom
29variable {G A : Type*} [Group G] [AddCommGroup A]
30variable {action : G →* Multiplicative (AddAut A)}
32variable [TopologicalSpace G] [IsTopologicalGroup G]
33variable [TopologicalSpace A] [T2Space A]
35/--
36Continuous crossed differentials with the same coefficients are determined by a topological
37generating set.
38-/
39theorem eq_of_continuous_of_topologicallyGenerates
40 (delta epsilon : CrossedHom action)
41 (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
42 {s : Set G} (hsgen : TopologicallyGenerates (G := G) s)
43 (hs : Set.EqOn delta epsilon s) :
44 delta = epsilon := by
45 let K : Subgroup G :=
46 { carrier := {g | delta g = epsilon g}
47 one_mem' := by
48 change delta 1 = epsilon 1
49 rw [delta.map_one, epsilon.map_one]
50 mul_mem' := by
51 intro a b ha hb
52 change delta (a * b) = epsilon (a * b)
53 rw [delta.map_mul a b, epsilon.map_mul a b, ha, hb]
54 inv_mem' := by
55 intro a ha
56 change delta a⁻¹ = epsilon a⁻¹
57 rw [delta.map_inv a, epsilon.map_inv a, ha] }
58 have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
59 change IsClosed {g | delta g = epsilon g}
60 exact isClosed_eq hdelta_continuous hepsilon_continuous
61 have hsub : Subgroup.closure s ≤ K := by
62 rw [Subgroup.closure_le]
63 intro x hx
64 exact hs hx
65 have htop : (⊤ : Subgroup G) ≤ K := by
66 have hcl : (Subgroup.closure s).topologicalClosure ≤ K :=
67 Subgroup.topologicalClosure_minimal _ hsub hKclosed
68 rw [TopologicallyGenerates] at hsgen
69 simpa [hsgen] using hcl
70 apply CrossedHom.ext
71 intro g
72 simpa [K] using htop (show g ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])
74section FreeProC
76variable {C : ProCGroups.FiniteGroupClass.{u}}
77variable {X F : Type u}
78variable [TopologicalSpace X]
79variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
80variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
81variable {A : Type*} [AddCommGroup A]
82variable [TopologicalSpace A] [T2Space A]
84/--
85Continuous crossed differentials on a free pro-\(C\) source are determined by their values on
86the free pro-\(C\) generators.
87-/
88theorem eq_of_freeProC_of_continuous
89 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
90 {action : F →* Multiplicative (AddAut A)} (delta epsilon : CrossedHom action)
91 (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
92 (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
93 delta = epsilon := by
94 refine
95 eq_of_continuous_of_topologicallyGenerates
96 delta epsilon hdelta_continuous hepsilon_continuous hι.generates_range ?_
97 rintro _ ⟨x, rfl⟩
98 exact hbasis x
100end FreeProC
102end CrossedHom
104section UniversalKernelCriterion
106variable (C : ProCGroups.FiniteGroupClass.{u})
107variable {G H A : Type u}
108variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
109variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
110variable [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
112/--
113The completed Magnus-kernel criterion for the universal differential transfers to every crossed
114differential represented by it.
115-/
116theorem zcUniversalDifferential_kernel_le_closedCommutator_of_crossedDifferential
117 (ψ : G →ₜ* H)
118 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
119 (hkerD :
120 ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
121 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
122 ∀ n : ProfiniteKernelSubgroup ψ,
123 zcUniversalDifferential C ψ.toMonoidHom n.1 = 0 →
124 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ) := by
125 intro n hn
126 exact hkerD n
127 (crossedDifferential_eq_zero_of_zcUniversalDifferential_eq_zero
128 (C := C) ψ.toMonoidHom D hn)
130end UniversalKernelCriterion
132section KernelAbelianization
134variable (C : ProCGroups.FiniteGroupClass.{u})
135variable {G H A : Type u}
136variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
137variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
138variable [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [T1Space A]
139variable [Module (ZCCompletedGroupAlgebra C H) A]
141/-- The multiplicative target object is \(T_1\) for its finite-stage topology. -/
142instance instT1SpaceMultiplicativeTarget : T1Space (Multiplicative A) := by
143 change T1Space A
144 infer_instance
146/--
147The restriction of a completed crossed differential to the kernel of its coefficient
148homomorphism, multiplicatively valued in the additive target.
149-/
150def zcCrossedDifferentialKernelHom
151 (ψ : G →ₜ* H)
152 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A) :
153 ProfiniteKernelSubgroup ψ →* Multiplicative A where
154 toFun n := Multiplicative.ofAdd (D n.1)
155 map_one' := by
156 rw [Submonoid.coe_one]
157 exact congrArg Multiplicative.ofAdd (ScalarCrossedHom.map_one D)
158 map_mul' n m := by
159 apply Multiplicative.ext
160 change D ((n * m : ProfiniteKernelSubgroup ψ) : G) = D n.1 + D m.1
161 rw [Submonoid.coe_mul, ScalarCrossedHom.map_mul D n.1 m.1]
162 have hn : ψ n.1 = 1 := n.2
163 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedGroupAlgebraScalar_apply,
164 MonoidHom.coe_coe, hn,
165 map_one, one_smul]
167omit [IsTopologicalGroup G] [IsTopologicalAddGroup A] [T1Space A] in
168/--
169The crossed-differential kernel homomorphism is continuous for the topology determined by the
170completed Fox coordinates.
171-/
172theorem continuous_zcCrossedDifferentialKernelHom
173 (ψ : G →ₜ* H)
174 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
175 (hcont : Continuous D) :
176 Continuous (zcCrossedDifferentialKernelHom (C := C) ψ D) := by
177 change Continuous fun n : ProfiniteKernelSubgroup ψ => Multiplicative.ofAdd (D n.1)
178 exact continuous_ofAdd.comp (hcont.comp continuous_subtype_val)
180/--
181A continuous crossed differential on G descends along the completed kernel abelianization of its
182coefficient homomorphism. This is the natural target of the completed relation-module map.
183-/
184def zcCrossedDifferentialProfiniteKernelAbelianizationHom
185 (ψ : G →ₜ* H)
186 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
187 (hcont : Continuous D) :
188 ProfiniteKernelAbelianization ψ →* Multiplicative A :=
190 { toMonoidHom := zcCrossedDifferentialKernelHom (C := C) ψ D
191 continuous_toFun :=
192 continuous_zcCrossedDifferentialKernelHom (C := C) ψ D hcont }).toMonoidHom
194/-- Additive form of \(\mathrm{zcCrossedDifferentialProfiniteKernelAbelianizationHom}\). -/
195def zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
196 (ψ : G →ₜ* H)
197 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
198 (hcont : Continuous D) :
199 ProfiniteKernelAbelianizationAdd ψ →+ A :=
200 (zcCrossedDifferentialProfiniteKernelAbelianizationHom
201 (C := C) ψ D hcont).toAdditiveLeft
203omit [IsTopologicalAddGroup A] in
204/--
205The completed crossed differential induces an additive monoid homomorphism from the topological
206kernel abelianization.
207-/
208@[simp]
209theorem zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_mk
210 (ψ : G →ₜ* H)
211 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
212 (hcont : Continuous D) (n : ProfiniteKernelSubgroup ψ) :
213 zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
214 (C := C) ψ D hcont
215 (Additive.ofMul (QuotientGroup.mk' (Subgroup.closedCommutator _) n)) =
216 D n.1 := by
217 have h :=
219 ({ toMonoidHom := zcCrossedDifferentialKernelHom (C := C) ψ D
220 continuous_toFun :=
221 continuous_zcCrossedDifferentialKernelHom (C := C) ψ D hcont } :
222 ProfiniteKernelSubgroup ψ →ₜ* Multiplicative A) n
223 have h' := congrArg (fun a : Multiplicative A => a.toAdd) h
224 convert h' using 1 <;> rfl
226omit [IsTopologicalAddGroup A] in
227/--
228A continuous completed crossed differential kills the closed commutator subgroup of the kernel
229of its coefficient homomorphism.
230-/
231theorem zcCrossedDifferential_eq_zero_of_mem_closedCommutator
232 (ψ : G →ₜ* H)
233 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
234 (hcont : Continuous D) {n : ProfiniteKernelSubgroup ψ}
235 (hn : n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
236 D n.1 = 0 := by
237 let F :=
238 zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
239 (C := C) ψ D hcont
240 have hnq :
241 QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n = 1 :=
242 (QuotientGroup.eq_one_iff
243 (N := Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n).2 hn
244 have h :=
245 congrArg (fun q : ProfiniteKernelAbelianization ψ => F (Additive.ofMul q)) hnq
246 rw [← zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_mk
247 (C := C) ψ D hcont n]
248 simpa [F] using h
250omit [IsTopologicalAddGroup A] in
251/--
252The induced map from the topological kernel abelianization is injective when the kernel of the
253crossed differential is contained in the closed commutator subgroup.
254-/
255theorem zcCrossedDiffProfiniteKernelAbelianizationAddMonoidHom_inj_of_kernel_le_closedCommutator
256 (ψ : G →ₜ* H)
257 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
258 (hcont : Continuous D)
259 (hker :
260 ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
261 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) :
262 Function.Injective
263 (zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
264 (C := C) ψ D hcont) := by
265 intro x y hxy
266 suffices x - y = 0 by exact sub_eq_zero.mp this
267 let F :=
268 zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
269 (C := C) ψ D hcont
270 have hmap : F (x - y) = 0 := by
271 rw [map_sub, hxy, sub_self]
272 have hzero_of_map_zero :
273 ∀ z : ProfiniteKernelAbelianizationAdd ψ, F z = 0 → z = 0 := by
274 intro z hz
275 apply Additive.toMul.injective
276 change (Additive.toMul z : ProfiniteKernelAbelianization ψ) = 1
277 revert hz
278 change
279 (fun q : ProfiniteKernelAbelianization ψ =>
280 F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
281 refine QuotientGroup.induction_on (Additive.toMul z) ?_
282 intro n hn
283 change QuotientGroup.mk' (Subgroup.closedCommutator _) n = 1
284 exact (QuotientGroup.eq_one_iff
285 (N := Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n).2
286 (hker n (by
287 rw [← zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_mk
288 (C := C) ψ D hcont n]
289 simpa [F] using hn))
290 exact hzero_of_map_zero (x - y) hmap
292omit [IsTopologicalAddGroup A] in
293/--
294Injectivity of the induced map on the topological kernel abelianization is equivalent to the
295continuous Magnus-kernel criterion.
296-/
297theorem zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom_injective_iff
298 {ψ : G →ₜ* H}
299 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ.toMonoidHom) A)
300 (hcont : Continuous D) :
301 Function.Injective
302 (zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
303 (C := C) ψ D hcont) ↔
304 ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
305 n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ) := by
306 constructor
307 · intro hinj n hn
308 let F :=
309 zcCrossedDifferentialProfiniteKernelAbelianizationAddMonoidHom
310 (C := C) ψ D hcont
311 have hzero :
312 F (Additive.ofMul
313 (QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n)) =
314 F 0 := by
315 simpa [F, hn]
316 have hclass :
317 Additive.ofMul
318 (QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n) =
319 0 := hinj hzero
320 have hmk :
321 QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n = 1 := by
322 simpa using congrArg Additive.toMul hclass
323 exact (QuotientGroup.eq_one_iff
324 (N := Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n).1 hmk
325 · intro hker
326 exact
327 zcCrossedDiffProfiniteKernelAbelianizationAddMonoidHom_inj_of_kernel_le_closedCommutator
328 (C := C) ψ D hcont hker
330end KernelAbelianization
332section CompletedFundamentalFormula
334variable (C : ProCGroups.FiniteGroupClass.{u})
335variable {X : Type u} [Fintype X] [DecidableEq X]
336variable {G H : Type u}
337variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
338variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
340/--
341Source-shaped completed Fox boundary formula from continuity and topological generation. This is
342the abstract form of the completed Fox fundamental formula: no free pro-\(C\) universal property
343is needed once the source generators topologically generate the source.
344-/
345theorem freeProCZCBoundary_of_topologicalGeneration
346 {ι : X → G}
347 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
348 (ψ : G →* H)
349 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
350 (ZCFreeFoxCoordinates C (X := X) (H := H)))
351 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
352 (hbasis :
353 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
354 (g : G) :
355 freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta g) =
356 zcCompletedGroupAlgebraBoundary C ψ g := by
357 let beta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
358 (ZCCompletedGroupAlgebra C H) :=
359 delta.mapLinear
360 (freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)))
361 have hbeta_continuous : Continuous beta :=
362 (continuous_freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))).comp hdelta_continuous
363 have hboundary_continuous : Continuous (zcCompletedGroupAlgebraBoundary C ψ) :=
364 continuous_zcCompletedGroupAlgebraBoundary (C := C) (G := H) ψ hψ_continuous
365 have hEqOn :
366 Set.EqOn beta (zcCompletedGroupAlgebraBoundary C ψ) (Set.range ι) := by
367 intro y hy
368 rcases hy with ⟨x, rfl⟩
369 change
370 freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta (ι x)) =
371 zcGroupLike C H (ψ (ι x)) - 1
372 rw [hbasis x, freeProCZCCompletedFoxBoundary_single]
373 have hEq :=
374 CrossedHom.eq_of_continuous_of_topologicallyGenerates
375 beta (zcCompletedGroupAlgebraBoundary C ψ)
376 hbeta_continuous hboundary_continuous hgen hEqOn
377 exact congrArg
378 (fun d : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
379 (ZCCompletedGroupAlgebra C H) => d g) hEq
381omit [DecidableEq X] [TopologicalSpace G]
382 [IsTopologicalGroup G] in
383/--
384Exactness at the finite completed Fox-coordinate term from a surjective semidirect graph. The
385hypothesis says that the crossed-differential graph g \(\mapsto\) (delta g, \(\psi(g)\)) fills
386\(\mathbb{Z}_C\llbracket H\rrbracket^{X}\) \(\rtimes\) H. Then every vector killed by the
387source-shaped Fox boundary is the derivative of an element of \(\ker \psi\).
388-/
389theorem exact_zcCrossedDiffKernelAddMonoidHom_freeProCZCCompletedFoxBoundary_of_surj_semi
390 (φ : X → H)
391 (ψ : G →* H)
392 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
393 (ZCFreeFoxCoordinates C (X := X) (H := H)))
394 (hboundary :
395 ∀ g : G,
396 freeProCZCCompletedFoxBoundary C φ (delta g) =
397 zcCompletedGroupAlgebraBoundary C ψ g)
398 (hgraph :
399 Function.Surjective
400 (fun g : G =>
401 ({ left := delta g, right := ψ g } :
402 ZCCompletedFoxSemidirect C X H))) :
403 Function.Exact
404 (ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom
405 delta ψ.ker
406 (zcCompletedGroupAlgebraScalar_subtype_ker (C := C) (ψ := ψ)))
407 (freeProCZCCompletedFoxBoundary C φ) := by
408 intro v
409 constructor
410 · intro hv
411 rcases hgraph
412 ({ left := v, right := 1 } :
413 ZCCompletedFoxSemidirect C X H) with
414 ⟨g, hg⟩
415 have hdelta_g : delta g = v := congrArg ZCCompletedFoxSemidirect.left hg
416 have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
417 refine ⟨Additive.ofMul (⟨g, hψ_g⟩ : ψ.ker), ?_⟩
418 simp only [ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom_apply, hdelta_g]
419 · rintro ⟨n, hn⟩
420 rw [← hn]
421 change
422 freeProCZCCompletedFoxBoundary C φ
423 (delta (((Additive.toMul n : ψ.ker) : G))) = 0
424 rw [hboundary (((Additive.toMul n : ψ.ker) : G))]
425 exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
426 (C := C) (ψ := ψ) (g := ((Additive.toMul n : ψ.ker) : G))
427 (Additive.toMul n).2
429omit [DecidableEq X] [TopologicalSpace G]
430 [IsTopologicalGroup G] in
431/--
432If a completed semidirect Fox lift onto \(\mathbb{Z}_C\llbracket H\rrbracket^{X} \rtimes H\) is
433actually surjective, then every generator boundary \([\varphi(x)]-1\) must vanish. This is a
434useful diagnostic obstruction: the graph generators of a free source cannot generally
435topologically generate the whole semidirect product.
436-/
437theorem zcCompletedFoxSemidirect_surjective_forces_generator_boundary_zero
438 (φ : X → H)
439 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
440 (hboundary :
441 ∀ g : G,
442 freeProCZCCompletedFoxBoundary C φ (delta g) =
443 zcCompletedGroupAlgebraBoundary C ψ g)
444 (hgraph :
445 Function.Surjective
446 (fun g : G =>
447 ({ left := delta g, right := ψ g } :
448 ZCCompletedFoxSemidirect C X H))) (x : X) :
449 zcGroupLike C H (φ x) - 1 = 0 := by
450 classical
451 rcases hgraph
452 ({ left := Pi.single x (1 : ZCCompletedGroupAlgebra C H), right := 1 } :
453 ZCCompletedFoxSemidirect C X H) with
454 ⟨g, hg⟩
455 have hdelta_g : delta g = Pi.single x (1 : ZCCompletedGroupAlgebra C H) :=
456 congrArg ZCCompletedFoxSemidirect.left hg
457 have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
458 calc
459 zcGroupLike C H (φ x) - 1 =
460 freeProCZCCompletedFoxBoundary C φ
461 (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) := by
462 rw [freeProCZCCompletedFoxBoundary_single]
463 _ = freeProCZCCompletedFoxBoundary C φ (delta g) := by rw [hdelta_g]
464 _ = zcCompletedGroupAlgebraBoundary C ψ g := hboundary g
465 _ = 0 := zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker C ψ hψ_g
467/--
468Exactness at the finite completed Fox-coordinate term, with the boundary identity supplied by
469continuity and topological generation of the source generators.
470-/
471theorem exact_zcKernelAdd_freeProCZCFoxBoundary_of_topGen
472 {ι : X → G}
473 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
474 (ψ : G →* H)
475 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
476 (ZCFreeFoxCoordinates C (X := X) (H := H)))
477 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
478 (hbasis :
479 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
480 (hgraph :
481 Function.Surjective
482 (fun g : G =>
483 ({ left := delta g, right := ψ g } :
484 ZCCompletedFoxSemidirect C X H))) :
485 Function.Exact
486 (ScalarCrossedHom.restrictTrivialSubgroupAddMonoidHom
487 delta ψ.ker
488 (zcCompletedGroupAlgebraScalar_subtype_ker (C := C) (ψ := ψ)))
489 (freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))) := by
490 exact
491 exact_zcCrossedDiffKernelAddMonoidHom_freeProCZCCompletedFoxBoundary_of_surj_semi
492 (C := C) (X := X) (G := G) (H := H)
493 (fun x : X => ψ (ι x)) ψ delta
494 (freeProCZCBoundary_of_topologicalGeneration
495 (C := C) (X := X) (G := G) (H := H)
496 hgen ψ delta hdelta_continuous hψ_continuous hbasis)
497 hgraph
499/-- Source-shaped completed Fox fundamental formula from continuity and topological generation. -/
500theorem freeProCZCFundamentalFormula_of_topologicalGeneration
501 {ι : X → G}
502 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
503 (ψ : G →* H)
504 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
505 (ZCFreeFoxCoordinates C (X := X) (H := H)))
506 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
507 (hbasis :
508 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
509 (g : G) :
510 zcCompletedGroupAlgebraBoundary C ψ g =
511 ∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1) := by
512 simpa [freeProCZCCompletedFoxBoundary_apply] using
513 (freeProCZCBoundary_of_topologicalGeneration
514 (X := X) (G := G) (H := H) C hgen ψ delta
515 hdelta_continuous hψ_continuous hbasis g).symm
517/--
518The finite-stage projection of the source-shaped completed Fox formula obtained from continuity
519and topological generation.
520-/
521theorem freeProCZCFundamentalFormula_stage_of_topologicalGeneration
522 {ι : X → G}
523 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
524 (ψ : G →* H)
525 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
526 (ZCFreeFoxCoordinates C (X := X) (H := H)))
527 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
528 (hbasis :
529 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
530 (j : ZCCompletedGroupAlgebraIndex C H) (g : G) :
531 zcCompletedGroupAlgebraProjection C H j
532 (zcCompletedGroupAlgebraBoundary C ψ g) =
533 zcCompletedGroupAlgebraProjection C H j
534 (∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1)) := by
535 exact congrArg (zcCompletedGroupAlgebraProjection C H j)
536 (freeProCZCFundamentalFormula_of_topologicalGeneration
537 (X := X) (G := G) (H := H) C hgen ψ delta
538 hdelta_continuous hψ_continuous hbasis g)
540/-- Explicit Euler-sum form from continuity and topological generation. -/
541theorem freeProCZCEulerFormula_of_topologicalGeneration
542 {ι : X → G}
543 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
544 (ψ : G →* H)
545 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
546 (ZCFreeFoxCoordinates C (X := X) (H := H)))
547 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
548 (hbasis :
549 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
550 (g : G) :
551 zcGroupLike C H (ψ g) - 1 =
552 ∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1) := by
553 convert
554 freeProCZCFundamentalFormula_of_topologicalGeneration
555 (X := X) (G := G) (H := H) C hgen ψ delta
556 hdelta_continuous hψ_continuous hbasis g using 1
557 rfl
559end CompletedFundamentalFormula
561section FreeProCCompletedExt
563variable {C : ProCGroups.FiniteGroupClass.{u}}
564variable {X F H : Type u}
565variable [TopologicalSpace X]
566variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
567variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
568variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
570/--
571Extensionality for continuous completed crossed differentials on a free pro-\(C\) source, using
572continuity of the coordinate-valued maps themselves.
573-/
574theorem freeProCZCCompletedCrossedDifferential_ext_of_continuous
575 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (C := C) ι)
576 (ψ : F →* H)
577 (delta epsilon :
578 ScalarCrossedHom
579 (zcCompletedGroupAlgebraScalar C ψ)
580 (ZCFreeFoxCoordinates C (X := X) (H := H)))
581 (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
582 (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
583 delta = epsilon := by
584 exact CrossedHom.eq_of_freeProC_of_continuous
585 (C := C) hι delta epsilon
586 hdelta_continuous hepsilon_continuous hbasis
588end FreeProCCompletedExt
590end
592end FoxDifferential