FoxDifferential/Completed/Continuous/Free/Rules.lean
1import FoxDifferential.Completed.Continuous.Free.Continuity
2import FoxDifferential.Completed.ProCIntegerCoefficients.Naturality
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Continuous/Free/Rules.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
23universe u
25variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
26variable {X F H : Type u}
27variable [TopologicalSpace X] [DecidableEq X]
28variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
29variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
31section FreeProCCompletedRules
33variable {ι : X → F}
34variable (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
35variable (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
36variable (φ : X → H)
37variable (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
39/-- The right component of the completed free pro-`C` Fox lift, bundled as a continuous
40homomorphism. -/
41def freeProCZCCompletedFoxRightHomContinuousMonoidHom : F →ₜ* H where
42 toMonoidHom := freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ
43 continuous_toFun :=
44 continuous_freeProCZCCompletedFoxRightHom (ProC := ProC) X H hι htarget φ hφ
46/-- The bundled right homomorphism has the expected underlying monoid homomorphism. -/
47@[simp]
50 (ProC := ProC) hι htarget φ hφ).toMonoidHom =
51 freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ :=
52 rfl
54/-- Evaluation of the bundled right homomorphism. -/
55@[simp]
56theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_apply (g : F) :
58 (ProC := ProC) hι htarget φ hφ g =
59 freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ g :=
60 rfl
62/-- The bundled right homomorphism has the prescribed generator values. -/
63@[simp]
64theorem freeProCZCCompletedFoxRightHomContinuousMonoidHom_generator (x : X) :
66 (ProC := ProC) hι htarget φ hφ (ι x) = φ x := by
67 exact freeProCZCCompletedFoxRightHom_generator (ProC := ProC) hι htarget φ hφ x
69/-- The completed free pro-`C` Fox derivative vector, bundled as a continuous map. It is a
70crossed differential, not a homomorphism. -/
72 ContinuousMap F (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) where
73 toFun := freeProCZCCompletedFoxDerivativeVector (ProC := ProC) hι htarget φ hφ
74 continuous_toFun :=
75 continuous_freeProCZCCompletedFoxDerivativeVector (ProC := ProC) X H hι htarget φ hφ
77/-- Evaluation of the bundled continuous completed Fox derivative vector. -/
78@[simp]
79theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_apply (g : F) :
81 (ProC := ProC) hι htarget φ hφ g =
82 freeProCZCCompletedFoxDerivativeVector (ProC := ProC) hι htarget φ hφ g :=
83 rfl
85/-- The bundled continuous completed Fox derivative vector has the prescribed generator values. -/
86@[simp]
87theorem freeProCZCCompletedFoxDerivativeVectorContinuousMap_generator (x : X) :
89 (ProC := ProC) hι htarget φ hφ (ι x) =
90 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
91 simp only [freeProCZCCompletedFoxDerivativeVectorContinuousMap, ContinuousMap.coe_mk,
94/-- The bundled continuous completed Fox derivative is a crossed differential. -/
97 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass
98 (freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ))
100 (ProC := ProC) hι htarget φ hφ) := by
102 (ProC := ProC) hι htarget φ hφ
104/-- Restricting the continuous completed Fox derivative to the abstract free group generated by
105the chosen free pro-`C` basis recovers the completed free-group Fox derivative. -/
107 (w : FreeGroup X) :
108 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
109 ((freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ).comp
110 (FreeGroup.lift ι)) w =
112 (ProC := ProC) hι htarget φ hφ ((FreeGroup.lift ι) w) := by
113 let ρ : F →* H :=
114 freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ
115 let D : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
116 freeProCZCCompletedFoxDerivativeVector (ProC := ProC) hι htarget φ hφ
117 let δ : FreeGroup X →
118 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
119 fun w => D ((FreeGroup.lift ι) w)
120 have hδ :
122 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι))) δ := by
123 intro u v
126 (ProC := ProC) hι htarget φ hφ ((FreeGroup.lift ι) u) ((FreeGroup.lift ι) v)
127 have hbasis :
128 ∀ x : X, δ (FreeGroup.of x) =
129 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
130 intro x
131 simp only [FreeGroup.lift_apply_of, freeProCZCCompletedFoxDerivativeVector_generator, δ, D]
132 have hδeq :
133 δ =
134 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
135 (ρ.comp (FreeGroup.lift ι)) :=
137 ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι)) δ hδ hbasis
138 exact congrFun hδeq w |>.symm
140/-- Source restriction and target naturality for the continuous completed Fox derivative. -/
142 (hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)
143 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
144 (η : H →ₜ* K) (w : FreeGroup X) :
145 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
146 (η.toMonoidHom.comp
147 ((freeProCZCCompletedFoxRightHom (ProC := ProC) hι htarget φ hφ).comp
148 (FreeGroup.lift ι))) w =
149 zcFreeFoxCoordinatesMap (X := X) ProC.finiteQuotientClass hC η
151 (ProC := ProC) hι htarget φ hφ ((FreeGroup.lift ι) w)) := by
154 (ProC := ProC) hι htarget φ hφ w]
156end FreeProCCompletedRules
158section FreeProCConvergingSetCompletedRules
160variable {ι : X → F}
161variable (hι :
162 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
163variable (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
164variable (φ : X → H)
165variable (hφconv :
166 ProCGroups.FreeProC.FamilyConvergesToOne
167 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
168 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
169variable (hφgen :
171 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
172 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
174omit [TopologicalSpace X] in
175/-- Restricting the converging-set continuous completed Fox derivative to the abstract free
176group generated by the chosen free pro-`C` basis recovers the completed free-group Fox
177derivative. -/
179 (w : FreeGroup X) :
180 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
182 (ProC := ProC) hι htarget φ hφconv hφgen).comp
183 (FreeGroup.lift ι)) w =
185 (ProC := ProC) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w) := by
186 let ρ : F →* H :=
188 (ProC := ProC) hι htarget φ hφconv hφgen
189 let D : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
191 (ProC := ProC) hι htarget φ hφconv hφgen
192 let δ : FreeGroup X →
193 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
194 fun w => D ((FreeGroup.lift ι) w)
195 have hδ :
197 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι))) δ := by
198 intro u v
201 (ProC := ProC) hι htarget φ hφconv hφgen
202 ((FreeGroup.lift ι) u) ((FreeGroup.lift ι) v)
203 have hbasis :
204 ∀ x : X, δ (FreeGroup.of x) =
205 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
206 intro x
207 simp only [FreeGroup.lift_apply_of, freeProCZCCompletedFoxDerivativeVectorOfConvergingSet_generator, δ, D]
208 have hδeq :
209 δ =
210 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
211 (ρ.comp (FreeGroup.lift ι)) :=
213 ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι)) δ hδ hbasis
214 exact congrFun hδeq w |>.symm
216omit [TopologicalSpace X] in
217/-- Source restriction and target naturality for the converging-set continuous completed Fox
218derivative. -/
220 (hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)
221 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
222 (η : H →ₜ* K) (w : FreeGroup X) :
223 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
224 (η.toMonoidHom.comp
226 (ProC := ProC) hι htarget φ hφconv hφgen).comp
227 (FreeGroup.lift ι))) w =
228 zcFreeFoxCoordinatesMap (X := X) ProC.finiteQuotientClass hC η
230 (ProC := ProC) hι htarget φ hφconv hφgen ((FreeGroup.lift ι) w)) := by
233 (ProC := ProC) hι htarget φ hφconv hφgen w]
235end FreeProCConvergingSetCompletedRules
237section FreeProCClosedGeneratedCompletedRules
239variable {ι : X → F}
240variable (hι :
241 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι)
242variable (φ : X → H)
243variable (htarget :
244 ProC (G :=
246 (ProC := ProC) φ : Subgroup
247 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
248variable (hφconv :
249 ProCGroups.FreeProC.FamilyConvergesToOne
250 (G :=
252 (ProC := ProC) φ : Subgroup
253 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
254 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
256omit [TopologicalSpace X] in
257/-- Restricting the closed-generated continuous completed Fox derivative to the abstract free
258group generated by the chosen free pro-`C` basis recovers the completed free-group Fox
259derivative. -/
261 (w : FreeGroup X) :
262 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
264 (ProC := ProC) hι φ htarget hφconv).comp
265 (FreeGroup.lift ι)) w =
267 (ProC := ProC) hι φ htarget hφconv ((FreeGroup.lift ι) w) := by
268 let ρ : F →* H :=
270 (ProC := ProC) hι φ htarget hφconv
271 let D : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
273 (ProC := ProC) hι φ htarget hφconv
274 let δ : FreeGroup X →
275 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
276 fun w => D ((FreeGroup.lift ι) w)
277 have hδ :
279 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι))) δ := by
280 intro u v
283 (ProC := ProC) hι φ htarget hφconv
284 ((FreeGroup.lift ι) u) ((FreeGroup.lift ι) v)
285 have hbasis :
286 ∀ x : X, δ (FreeGroup.of x) =
287 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
288 intro x
289 simp only [FreeGroup.lift_apply_of, freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator, δ, D]
290 have hδeq :
291 δ =
292 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
293 (ρ.comp (FreeGroup.lift ι)) :=
295 ProC.finiteQuotientClass (ρ.comp (FreeGroup.lift ι)) δ hδ hbasis
296 exact congrFun hδeq w |>.symm
298omit [TopologicalSpace X] in
299/-- Source restriction and target naturality for the closed-generated continuous completed Fox
300derivative. -/
302 (hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)
303 {K : Type u} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
304 (η : H →ₜ* K) (w : FreeGroup X) :
305 zcFreeGroupFoxDerivativeVector ProC.finiteQuotientClass
306 (η.toMonoidHom.comp
308 (ProC := ProC) hι φ htarget hφconv).comp
309 (FreeGroup.lift ι))) w =
310 zcFreeFoxCoordinatesMap (X := X) ProC.finiteQuotientClass hC η
312 (ProC := ProC) hι φ htarget hφconv ((FreeGroup.lift ι) w)) := by
315 (ProC := ProC) hι φ htarget hφconv w]
317end FreeProCClosedGeneratedCompletedRules
319end
321end FoxDifferential