Yamaguchi Lean 4 Library
FoxDifferential/Completed/Continuous/TopologicalGeneration.lean
FoxDifferential/Completed/Continuous/TopologicalGeneration/Source

FoxDifferential/Completed/Continuous/TopologicalGeneration.lean

1import FoxDifferential.Completed.Continuous.Topology
2import ProCGroups.ProC.Kernels
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Continuous/TopologicalGeneration.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 scoped BigOperators
22open ProCGroups.Generation
23open ProCGroups.ProC
25universe u v
29variable {R G A : Type*} [Semiring R] [Group G] [AddCommGroup A] [Module R A]
30variable {coeff : G →* R} {delta epsilon : G → A}
32variable [TopologicalSpace G] [IsTopologicalGroup G]
33variable [TopologicalSpace A] [T2Space A]
35/-- Continuous crossed differentials with the same coefficients are determined by a topological
36generating set. -/
38 (hdelta : IsCrossedDifferential coeff delta)
39 (hepsilon : IsCrossedDifferential coeff epsilon)
40 (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
41 {s : Set G} (hsgen : TopologicallyGenerates (G := G) s)
42 (hs : Set.EqOn delta epsilon s) :
43 delta = epsilon := by
44 let K : Subgroup G :=
45 { carrier := {g | delta g = epsilon g}
46 one_mem' := by
47 change delta 1 = epsilon 1
48 rw [hdelta.one, hepsilon.one]
49 mul_mem' := by
50 intro a b ha hb
51 change delta (a * b) = epsilon (a * b)
52 rw [hdelta.mul a b, hepsilon.mul a b, ha, hb]
53 inv_mem' := by
54 intro a ha
55 change delta a⁻¹ = epsilon a⁻¹
56 rw [hdelta.inv a, hepsilon.inv a, ha] }
57 have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
58 change IsClosed {g | delta g = epsilon g}
59 exact isClosed_eq hdelta_continuous hepsilon_continuous
60 have hsub : Subgroup.closure s ≤ K := by
61 rw [Subgroup.closure_le]
62 intro x hx
63 exact hs hx
64 have htop : (⊤ : Subgroup G) ≤ K := by
65 have hcl : (Subgroup.closure s).topologicalClosure ≤ K :=
66 Subgroup.topologicalClosure_minimal _ hsub hKclosed
68 simpa [hsgen] using hcl
69 funext g
70 simpa [K] using htop (show g ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])
72section FreeProC
74variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
75variable {X F : Type u}
76variable [TopologicalSpace X]
77variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
78variable {R A : Type*} [Semiring R] [AddCommGroup A] [Module R A]
79variable [TopologicalSpace A] [T2Space A]
81/-- Continuous crossed differentials on a free pro-`C` source are determined by their values on
82the free pro-`C` generators. -/
84 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
85 {coeff : F →* R} {delta epsilon : F → A}
86 (hdelta : IsCrossedDifferential coeff delta)
87 (hepsilon : IsCrossedDifferential coeff epsilon)
88 (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
89 (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
90 delta = epsilon := by
91 refine
93 hdelta hepsilon hdelta_continuous hepsilon_continuous hι.generates_range ?_
94 rintro _ ⟨x, rfl⟩
95 exact hbasis x
97end FreeProC
101section UniversalKernelCriterion
103variable (C : ProCGroups.FiniteGroupClass.{u})
104variable {G H A : Type u}
105variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
106variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
107variable [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
109/-- To prove the universal completed Magnus-kernel criterion, it is enough to prove it for any
110crossed differential represented by the completed universal differential. -/
112 (ψ : G →ₜ* H) (D : G → A)
114 (hkerD :
115 ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
118 zcUniversalDifferential C ψ.toMonoidHom n.1 = 0 →
120 intro n hn
121 exact hkerD n
123 (C := C) ψ.toMonoidHom D hD hn)
125end UniversalKernelCriterion
127section KernelAbelianization
129variable (C : ProCGroups.FiniteGroupClass.{u})
130variable {G H A : Type u}
131variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
132variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
133variable [AddCommGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] [T1Space A]
134variable [Module (ZCCompletedGroupAlgebra C H) A]
136instance instT1SpaceMultiplicativeTarget : T1Space (Multiplicative A) := by
137 change T1Space A
138 infer_instance
140/-- The restriction of a completed crossed differential to the kernel of its
141coefficient homomorphism, multiplicatively valued in the additive target. -/
143 (ψ : G →ₜ* H) (D : G → A)
145 ProfiniteKernelSubgroup ψ →* Multiplicative A where
146 toFun n := Multiplicative.ofAdd (D n.1)
147 map_one' := by
148 rw [Submonoid.coe_one]
149 exact congrArg Multiplicative.ofAdd (IsCrossedDifferential.one hD)
150 map_mul' n m := by
151 apply Multiplicative.ext
152 change D ((n * m : ProfiniteKernelSubgroup ψ) : G) = D n.1 + D m.1
153 rw [Submonoid.coe_mul, hD n.1 m.1]
154 have hn : ψ n.1 = 1 := n.2
155 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedGroupAlgebraScalar_apply, MonoidHom.coe_coe, hn,
156 map_one, one_smul]
158omit [IsTopologicalGroup G] [IsTopologicalAddGroup A] [T1Space A] in
160 (ψ : G →ₜ* H) (D : G → A)
162 (hcont : Continuous D) :
163 Continuous (zcCrossedDifferentialKernelHom (C := C) ψ D hD) := by
164 change Continuous fun n : ProfiniteKernelSubgroup ψ => Multiplicative.ofAdd (D n.1)
165 exact continuous_ofAdd.comp (hcont.comp continuous_subtype_val)
167/-- A continuous crossed differential on `G` descends along the completed kernel
168abelianization of its coefficient homomorphism. This is the natural target of
169the completed relation-module map. -/
171 (ψ : G →ₜ* H) (D : G → A)
173 (hcont : Continuous D) :
174 ProfiniteKernelAbelianization ψ →* Multiplicative A :=
176 { toMonoidHom := zcCrossedDifferentialKernelHom (C := C) ψ D hD
177 continuous_toFun :=
178 continuous_zcCrossedDifferentialKernelHom (C := C) ψ D hD hcont }).toMonoidHom
180/-- Additive form of `zcCrossedDifferentialProfiniteKernelAbelianizationHom`. -/
182 (ψ : G →ₜ* H) (D : G → A)
184 (hcont : Continuous D) :
187 (C := C) ψ D hD hcont).toAdditiveLeft
189omit [IsTopologicalAddGroup A] in
190@[simp]
192 (ψ : G →ₜ* H) (D : G → A)
194 (hcont : Continuous D) (n : ProfiniteKernelSubgroup ψ) :
196 (C := C) ψ D hD hcont
197 (Additive.ofMul (QuotientGroup.mk' (Subgroup.closedCommutator _) n)) =
198 D n.1 := by
199 have h :=
201 ({ toMonoidHom := zcCrossedDifferentialKernelHom (C := C) ψ D hD
202 continuous_toFun :=
204 ProfiniteKernelSubgroup ψ →ₜ* Multiplicative A) n
209 congrArg Multiplicative.toAdd h
211omit [IsTopologicalAddGroup A] in
212/-- A continuous completed crossed differential kills the closed commutator subgroup of the
213kernel of its coefficient homomorphism. -/
215 (ψ : G →ₜ* H) (D : G → A)
217 (hcont : Continuous D) {n : ProfiniteKernelSubgroup ψ}
219 D n.1 = 0 := by
220 let F :=
222 (C := C) ψ D hD hcont
223 have hnq :
224 QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n = 1 :=
225 (QuotientGroup.eq_one_iff
227 have h :=
228 congrArg (fun q : ProfiniteKernelAbelianization ψ => F (Additive.ofMul q)) hnq
229 simpa [F] using h
231omit [IsTopologicalAddGroup A] in
233 (ψ : G →ₜ* H) (D : G → A)
235 (hcont : Continuous D)
236 (hker :
237 ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
239 Function.Injective
241 (C := C) ψ D hD hcont) := by
242 intro x y hxy
243 suffices x - y = 0 by exact sub_eq_zero.mp this
244 let F :=
246 (C := C) ψ D hD hcont
247 have hmap : F (x - y) = 0 := by
248 rw [map_sub, hxy, sub_self]
249 have hzero_of_map_zero :
250 ∀ z : ProfiniteKernelAbelianizationAdd ψ, F z = 0 → z = 0 := by
251 intro z hz
252 apply Additive.toMul.injective
253 change (Additive.toMul z : ProfiniteKernelAbelianization ψ) = 1
254 revert hz
255 change
257 F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
258 refine QuotientGroup.induction_on (Additive.toMul z) ?_
259 intro n hn
260 change QuotientGroup.mk' (Subgroup.closedCommutator _) n = 1
261 exact (QuotientGroup.eq_one_iff
263 (hker n (by simpa [F] using hn))
264 exact hzero_of_map_zero (x - y) hmap
266omit [IsTopologicalAddGroup A] in
267/-- Injectivity of the induced map on the topological kernel abelianization is exactly the
268continuous Magnus-kernel criterion. -/
270 (ψ : G →ₜ* H) (D : G → A)
272 (hcont : Continuous D) :
273 Function.Injective
275 (C := C) ψ D hD hcont) ↔
276 ∀ n : ProfiniteKernelSubgroup ψ, D n.1 = 0 →
278 constructor
279 · intro hinj n hn
280 let F :=
282 (C := C) ψ D hD hcont
283 have hzero :
284 F (Additive.ofMul
285 (QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n)) =
286 F 0 := by
287 simpa [F, hn]
288 have hclass :
289 Additive.ofMul
291 0 := hinj hzero
292 have hmk :
293 QuotientGroup.mk' (Subgroup.closedCommutator (ProfiniteKernelSubgroup ψ)) n = 1 := by
294 simpa using congrArg Additive.toMul hclass
295 exact (QuotientGroup.eq_one_iff
297 · intro hker
298 exact
300 (C := C) ψ D hD hcont hker
302end KernelAbelianization
304section CompletedFundamentalFormula
306variable (C : ProCGroups.FiniteGroupClass.{u})
308variable {X : Type u} [Fintype X] [DecidableEq X]
309variable {G H : Type u}
310variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
311variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
314/-- Source-shaped completed Fox boundary formula from continuity and topological generation.
316This is the abstract form of the completed Fox fundamental formula: no free pro-`C` universal
317property is needed once the source generators topologically generate the source. -/
319 {ι : X → G}
320 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
321 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
323 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
324 (hbasis :
325 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
326 (g : G) :
327 freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta g) =
329 let beta : G → ZCCompletedGroupAlgebra C H :=
330 fun g => freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)) (delta g)
332 IsCrossedDifferential.map_linear hdelta
333 (freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x)))
334 have hboundary :
338 have hbeta_continuous : Continuous beta :=
339 (continuous_freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))).comp hdelta_continuous
340 have hboundary_continuous : Continuous (zcCompletedGroupAlgebraBoundary C ψ) :=
341 continuous_zcCompletedGroupAlgebraBoundary (C := C) (G := H) ψ hψ_continuous
342 have hEqOn :
343 Set.EqOn beta (zcCompletedGroupAlgebraBoundary C ψ) (Set.range ι) := by
344 intro y hy
345 rcases hy with ⟨x, rfl⟩
347 have hEq :=
348 IsCrossedDifferential.eq_of_continuous_of_topologicallyGenerates
349 hbeta hboundary hbeta_continuous hboundary_continuous hgen hEqOn
350 exact congrFun hEq g
352omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] [TopologicalSpace G]
353 [IsTopologicalGroup G] in
354/-- Exactness at the finite completed Fox-coordinate term from a surjective semidirect graph.
356The hypothesis says that the crossed-differential graph
357`g ↦ (delta g, ψ g)` fills `Z_C[[H]]^X ⋊ H`. Then every vector killed by the
358source-shaped Fox boundary is the derivative of an element of `ker ψ`. -/
360 (φ : X → H)
361 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
363 (hboundary :
364 ∀ g : G,
367 (hgraph :
368 Function.Surjective
369 (fun g : G =>
370 ({ left := delta g, right := ψ g } :
372 Function.Exact
375 intro v
376 constructor
377 · intro hv
378 rcases hgraph
379 ({ left := v, right := 1 } :
381 ⟨g, hg⟩
382 have hdelta_g : delta g = v := congrArg ZCCompletedFoxSemidirect.left hg
383 have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
384 refine ⟨Additive.ofMul (⟨g, hψ_g⟩ : ψ.ker), ?_⟩
386 · rintro ⟨n, hn⟩
387 rw [← hn]
388 change
390 (delta (((Additive.toMul n : ψ.ker) : G))) = 0
391 rw [hboundary (((Additive.toMul n : ψ.ker) : G))]
393 (C := C) (ψ := ψ) (g := ((Additive.toMul n : ψ.ker) : G))
394 (Additive.toMul n).2
396omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [TopologicalSpace G]
397 [IsTopologicalGroup G] in
398/-- If a completed semidirect Fox lift onto `Z_C[[H]]^X ⋊ H` is actually
399surjective, then every generator boundary `[φ x] - 1` must vanish.
401This is a useful diagnostic obstruction: the graph generators of a free source
402cannot generally topologically generate the whole semidirect product. -/
404 (φ : X → H)
405 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
406 (hboundary :
407 ∀ g : G,
410 (hgraph :
411 Function.Surjective
412 (fun g : G =>
413 ({ left := delta g, right := ψ g } :
414 ZCCompletedFoxSemidirect C X H))) (x : X) :
415 zcGroupLike C H (φ x) - 1 = 0 := by
416 rcases hgraph
417 ({ left := Pi.single x (1 : ZCCompletedGroupAlgebra C H), right := 1 } :
419 ⟨g, hg⟩
420 have hdelta_g : delta g = Pi.single x (1 : ZCCompletedGroupAlgebra C H) :=
421 congrArg ZCCompletedFoxSemidirect.left hg
422 have hψ_g : ψ g = 1 := congrArg ZCCompletedFoxSemidirect.right hg
423 calc
424 zcGroupLike C H (φ x) - 1 =
426 (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) := by
428 _ = freeProCZCCompletedFoxBoundary C φ (delta g) := by rw [hdelta_g]
429 _ = zcCompletedGroupAlgebraBoundary C ψ g := hboundary g
430 _ = 0 := by simp only [zcCompletedGroupAlgebraBoundary, hψ_g, map_one, sub_self]
433/-- Exactness at the finite completed Fox-coordinate term, with the boundary identity supplied by
434continuity and topological generation of the source generators. -/
436 {ι : X → G}
437 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
438 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
440 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
441 (hbasis :
442 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
443 (hgraph :
444 Function.Surjective
445 (fun g : G =>
446 ({ left := delta g, right := ψ g } :
448 Function.Exact
450 (freeProCZCCompletedFoxBoundary C (fun x : X => ψ (ι x))) := by
451 exact
453 (C := C) (X := X) (G := G) (H := H)
454 (fun x : X => ψ (ι x)) ψ delta hdelta
456 (C := C) (X := X) (G := G) (H := H)
457 hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis)
458 hgraph
461/-- Source-shaped completed Fox fundamental formula from continuity and topological generation. -/
463 {ι : X → G}
464 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
465 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
467 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
468 (hbasis :
469 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
470 (g : G) :
472 ∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1) := by
475 (X := X) (G := G) (H := H) C hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis g).symm
478/-- Finite-stage projection of the source-shaped completed Fox formula obtained from continuity
479and topological generation. -/
481 {ι : X → G}
482 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
483 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
485 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
486 (hbasis :
487 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
488 (j : ZCCompletedGroupAlgebraIndex C H) (g : G) :
492 (∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1)) := by
493 exact congrArg (zcCompletedGroupAlgebraProjection C H j)
495 (X := X) (G := G) (H := H) C hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis g)
498/-- Explicit Euler-sum form from continuity and topological generation. -/
500 {ι : X → G}
501 (hgen : TopologicallyGenerates (G := G) (Set.range ι))
502 (ψ : G →* H) (delta : G → ZCFreeFoxCoordinates C (X := X) (H := H))
504 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
505 (hbasis :
506 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H))
507 (g : G) :
508 zcGroupLike C H (ψ g) - 1 =
509 ∑ x : X, delta g x * (zcGroupLike C H (ψ (ι x)) - 1) := by
512 (X := X) (G := G) (H := H) C hgen ψ delta hdelta hdelta_continuous hψ_continuous hbasis g
514end CompletedFundamentalFormula
516section FreeProCCompletedExt
518variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
519variable {X F H : Type u}
520variable [TopologicalSpace X]
521variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
522variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
524/-- Extensionality for continuous completed crossed differentials on a free pro-`C` source,
525using continuity of the coordinate-valued maps themselves. -/
527 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
528 (ψ : F →* H)
529 (delta epsilon :
530 F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
531 (hdelta :
532 IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
533 (hepsilon :
534 IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) epsilon)
535 (hdelta_continuous : Continuous delta) (hepsilon_continuous : Continuous epsilon)
536 (hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
537 delta = epsilon := by
538 exact IsCrossedDifferential.eq_of_freeProC_of_continuous
539 (ProC := ProC) hι hdelta hepsilon hdelta_continuous hepsilon_continuous hbasis
541end FreeProCCompletedExt
543end
545end FoxDifferential