FoxDifferential/Completed/FreeProC/Uniqueness/SemidirectHom.lean
1import FoxDifferential.Completed.FreeProC.SemidirectLift
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FreeProC/Uniqueness/SemidirectHom.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free pro-C completed Fox calculus
14Free pro-C sources are treated through completed Fox derivatives, stage projections, density arguments, and semidirect lift formulas.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.FreeProC
22universe u
25variable {ProC : ProCGroups.ProC.ProCGroupPredicate}
26variable {X F H : Type u}
27variable [TopologicalSpace X]
28variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
29variable [DecidableEq X]
30variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
31variable [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
32variable [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
34/-- A completed crossed differential and its coefficient homomorphism combine into a semidirect
35homomorphism. -/
37 (ψ : F →* H) (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
38 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta) :
39 F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H where
40 toFun g := { left := delta g, right := ψ g }
41 map_one' := by
42 apply ZCCompletedFoxSemidirect.ext
43 · simpa using IsCrossedDifferential.one hdelta
45 map_mul' g h := by
46 apply ZCCompletedFoxSemidirect.ext
47 · simpa using hdelta g h
50omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] [DecidableEq X]
51 [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
52 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
53/-- The semidirect homomorphism attached to a crossed differential has `delta` as its left
54component. -/
55@[simp]
57 (ψ : F →* H) (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
58 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
59 (g : F) :
61 (X := X) ψ delta hdelta g).left = delta g :=
62 rfl
64omit [TopologicalSpace X] [TopologicalSpace F] [IsTopologicalGroup F] [DecidableEq X]
65 [TopologicalSpace (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
66 [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
67/-- The semidirect homomorphism attached to a crossed differential has `ψ` as its right
68component. -/
69@[simp]
71 (ψ : F →* H) (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
72 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
73 (g : F) :
75 (X := X) ψ delta hdelta g).right = ψ g :=
76 rfl
78omit [IsTopologicalGroup (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)] in
79/-- If a crossed-differential semidirect homomorphism is continuous and has the standard
82 {ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
83 (ψ : F →* H) (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
84 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
85 (hcontinuous :
87 (X := X) ψ delta hdelta))
88 (hbasis :
89 ∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
90 Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) (fun x : X => ψ (ι x))) := by
91 have hgenerator :
92 (fun x : X =>
94 (X := X) ψ delta hdelta (ι x)) =
95 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) (fun x : X => ψ (ι x)) := by
96 funext x
97 apply ZCCompletedFoxSemidirect.ext
98 · exact hbasis x
99 · rfl
100 rw [← hgenerator]
101 exact hcontinuous.comp hι.continuous_ι
104end
106end FoxDifferential