FoxDifferential/Completed/Continuous/Free/Continuity.lean
1import FoxDifferential.Completed.FreeProC.Uniqueness.Derivative
2import FoxDifferential.Completed.Continuous.Topology
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Continuous/Free/Continuity.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 ProCGroups.InverseSystems
22open scoped BigOperators
24universe u
27variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
28variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
29variable (X H : Type u) [DecidableEq X]
30variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
33/-- The completed Fox semidirect generator map is continuous when both component maps are
34continuous. -/
36 [TopologicalSpace X]
37 (φ : X → H)
38 (hleft : Continuous (fun x : X =>
39 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)))
40 (hφ : Continuous φ) :
41 Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) := by
42 rw [continuous_induced_rng]
43 exact hleft.prodMk hφ
45omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
46/-- The completed Fox semidirect generator map is continuous for a discrete generating space. -/
48 [TopologicalSpace X] [DiscreteTopology X] (φ : X → H) :
49 Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) :=
50 continuous_of_discreteTopology
52variable {F : Type u}
53variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
55omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
56 [DecidableEq X] [IsTopologicalGroup F] in
57/-- A crossed-differential graph into the completed Fox semidirect target is continuous when both
58its component maps are continuous. -/
60 (ψ : F →* H)
61 (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
62 (hdelta : IsCrossedDifferential
63 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
64 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ) :
66 (ProC := ProC) (X := X) (F := F) (H := H) ψ delta hdelta) := by
67 rw [continuous_induced_rng]
68 exact hdelta_continuous.prodMk hψ_continuous
70variable [TopologicalSpace X]
72omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
73/-- The target-group component of the free pro-`C` completed Fox semidirect lift is continuous. -/
75 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
76 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
77 (φ : X → H)
78 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
79 Continuous (freeProCZCCompletedFoxRightHom
80 (ProC := ProC) hι htarget φ hφ) := by
81 change Continuous (fun g : F =>
83 (ProC := ProC) hι htarget φ hφ g).right)
84 exact (continuous_zcCompletedFoxSemidirect_right ProC.finiteQuotientClass X H).comp
86 (ProC := ProC) hι htarget φ hφ)
88omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
89 [TopologicalSpace X] in
90/-- The right component of the converging-set completed Fox semidirect lift is continuous. -/
92 {ι : X → F}
93 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
94 (ProC := ProC) X F ι)
95 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
96 (φ : X → H)
97 (hφconv :
98 ProCGroups.FreeProC.FamilyConvergesToOne
99 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
100 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
101 (hφgen :
103 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
104 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
105 Continuous (freeProCZCCompletedFoxRightHomOfConvergingSet
106 (ProC := ProC) hι htarget φ hφconv hφgen) := by
107 change Continuous (fun g : F =>
109 (ProC := ProC) hι htarget φ hφconv hφgen g).right)
110 exact (continuous_zcCompletedFoxSemidirect_right ProC.finiteQuotientClass X H).comp
112 (ProC := ProC) hι htarget φ hφconv hφgen)
114omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
115 [TopologicalSpace X] in
116/-- The right component of the converging-set semidirect Fox lift is exactly the universal
119 {ι : X → F}
120 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
121 (ProC := ProC) X F ι)
122 (hH : ProC (G := H))
123 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
124 (φ : X → H)
125 (hφconv :
126 ProCGroups.FreeProC.FamilyConvergesToOne
127 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
128 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
129 (hφgen :
131 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
132 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
133 (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ)
134 (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
136 (ProC := ProC) hι htarget φ hφconv hφgen =
137 hι.lift hH φ hφHconv hφHgen := by
138 apply hι.lift_unique hH φ hφHconv hφHgen
140 (ProC := ProC) X H hι htarget φ hφconv hφgen
141 · intro x
144omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
145 [TopologicalSpace X] in
146/-- The closed-generated completed Fox semidirect lift is continuous as a map to the full
147semidirect target. -/
149 {ι : X → F}
150 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
151 (ProC := ProC) X F ι)
152 (φ : X → H)
153 (htarget :
154 ProC (G :=
156 (ProC := ProC) φ : Subgroup
157 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
158 (hφconv :
159 ProCGroups.FreeProC.FamilyConvergesToOne
160 (G :=
162 (ProC := ProC) φ : Subgroup
163 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
164 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
166 (ProC := ProC) hι φ htarget hφconv) := by
167 change Continuous (fun g : F =>
169 (ProC := ProC) hι φ htarget hφconv g :
170 ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
171 exact continuous_subtype_val.comp
173 (ProC := ProC) hι φ htarget hφconv).continuous_toFun
175omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
176 [TopologicalSpace X] in
177/-- The right component of the closed-generated completed Fox semidirect lift is continuous. -/
179 {ι : X → F}
180 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
181 (ProC := ProC) X F ι)
182 (φ : X → H)
183 (htarget :
184 ProC (G :=
186 (ProC := ProC) φ : Subgroup
187 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
188 (hφconv :
189 ProCGroups.FreeProC.FamilyConvergesToOne
190 (G :=
192 (ProC := ProC) φ : Subgroup
193 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
194 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
195 Continuous (freeProCZCCompletedFoxRightHomViaClosedGenerated
196 (ProC := ProC) hι φ htarget hφconv) := by
197 change Continuous (fun g : F =>
199 (ProC := ProC) hι φ htarget hφconv g).right)
200 exact (continuous_zcCompletedFoxSemidirect_right ProC.finiteQuotientClass X H).comp
202 (ProC := ProC) X H hι φ htarget hφconv)
204omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
205 [TopologicalSpace X] in
206/-- The right component of the closed-generated semidirect Fox lift is the universal
209 {ι : X → F}
210 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
211 (ProC := ProC) X F ι)
212 (hH : ProC (G := H))
213 (φ : X → H)
214 (htarget :
215 ProC (G :=
217 (ProC := ProC) φ : Subgroup
218 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
219 (hφconv :
220 ProCGroups.FreeProC.FamilyConvergesToOne
221 (G :=
223 (ProC := ProC) φ : Subgroup
224 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
225 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
226 (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ)
227 (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
229 (ProC := ProC) hι φ htarget hφconv =
230 hι.lift hH φ hφHconv hφHgen := by
231 apply hι.lift_unique hH φ hφHconv hφHgen
233 (ProC := ProC) X H hι φ htarget hφconv
234 · intro x
237omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
238 [TopologicalSpace X] in
239/-- The right component of the closed-generated semidirect Fox lift is any continuous
242This is the paper graph's target-coordinate verification: once the closed-generated lift has
244that right component with the intended continuous homomorphism. -/
246 {ι : X → F}
247 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
248 (ProC := ProC) X F ι)
249 (hH : ProC (G := H))
250 (φ : X → H)
251 (htarget :
252 ProC (G :=
254 (ProC := ProC) φ : Subgroup
255 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
256 (hφconv :
257 ProCGroups.FreeProC.FamilyConvergesToOne
258 (G :=
260 (ProC := ProC) φ : Subgroup
261 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
262 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
263 (hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ)
264 (hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
265 (ψ : F →ₜ* H)
266 (hψ_gen : ∀ x : X, ψ (ι x) = φ x) :
268 (ProC := ProC) hι φ htarget hφconv =
269 ψ.toMonoidHom := by
270 have hright_lift :
272 (ProC := ProC) hι φ htarget hφconv =
273 hι.lift hH φ hφHconv hφHgen :=
275 (ProC := ProC) X H hι hH φ htarget hφconv hφHconv hφHgen
276 have hψ_lift :
277 ψ.toMonoidHom = hι.lift hH φ hφHconv hφHgen := by
278 apply hι.lift_unique hH φ hφHconv hφHgen
279 · exact ψ.continuous_toFun
280 · exact hψ_gen
281 exact hright_lift.trans hψ_lift.symm
283omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
284 [TopologicalSpace X] in
285/-- The derivative-vector component of the closed-generated semidirect lift is continuous. -/
287 {ι : X → F}
288 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
289 (ProC := ProC) X F ι)
290 (φ : X → H)
291 (htarget :
292 ProC (G :=
294 (ProC := ProC) φ : Subgroup
295 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
296 (hφconv :
297 ProCGroups.FreeProC.FamilyConvergesToOne
298 (G :=
300 (ProC := ProC) φ : Subgroup
301 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
302 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
304 (ProC := ProC) hι φ htarget hφconv) := by
305 change Continuous (fun g : F =>
307 (ProC := ProC) hι φ htarget hφconv g).left)
308 exact (continuous_zcCompletedFoxSemidirect_left ProC.finiteQuotientClass X H).comp
310 (ProC := ProC) X H hι φ htarget hφconv)
312omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
313/-- The completed Fox derivative-vector component of the free pro-`C` semidirect lift is
314continuous. -/
316 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
317 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
318 (φ : X → H)
319 (hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
320 Continuous (freeProCZCCompletedFoxDerivativeVector
321 (ProC := ProC) hι htarget φ hφ) := by
322 change Continuous (fun g : F =>
324 (ProC := ProC) hι htarget φ hφ g).left)
325 exact (continuous_zcCompletedFoxSemidirect_left ProC.finiteQuotientClass X H).comp
327 (ProC := ProC) hι htarget φ hφ)
329omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
330 [TopologicalSpace X] in
331/-- The derivative-vector component of the converging-set completed Fox semidirect lift is
332continuous. -/
334 {ι : X → F}
335 (hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
336 (ProC := ProC) X F ι)
337 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
338 (φ : X → H)
339 (hφconv :
340 ProCGroups.FreeProC.FamilyConvergesToOne
341 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
342 (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
343 (hφgen :
345 (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
346 (Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
348 (ProC := ProC) hι htarget φ hφconv hφgen) := by
349 change Continuous (fun g : F =>
351 (ProC := ProC) hι htarget φ hφconv hφgen g).left)
352 exact (continuous_zcCompletedFoxSemidirect_left ProC.finiteQuotientClass X H).comp
354 (ProC := ProC) hι htarget φ hφconv hφgen)
356omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
357/-- The semidirect generator map attached to a continuous crossed differential is continuous once
358the component maps are continuous. -/
360 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
361 (ψ : F →* H)
362 (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
363 (hdelta : IsCrossedDifferential
364 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
365 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
366 (hbasis :
367 ∀ x : X, delta (ι x) =
368 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
369 Continuous (freeProCZCCompletedFoxSemidirectGenerator
370 (ProC := ProC) (fun x : X => ψ (ι x))) :=
372 (ProC := ProC) hι ψ delta hdelta
374 (ProC := ProC) (X := X) (F := F) (H := H)
375 ψ delta hdelta hdelta_continuous hψ_continuous)
376 hbasis
378omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
379/-- Continuous completed crossed differentials with continuous coefficient homomorphism are
380uniquely identified with the canonical free pro-`C` completed Fox derivative vector. -/
382 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
383 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
384 (ψ : F →* H)
385 (delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
386 (hdelta : IsCrossedDifferential
387 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
388 (hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
389 (hbasis :
390 ∀ x : X, delta (ι x) =
391 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
392 delta =
394 (ProC := ProC) hι htarget (fun x : X => ψ (ι x))
396 (ProC := ProC) X H hι ψ delta hdelta hdelta_continuous hψ_continuous hbasis) :=
398 (ProC := ProC) hι htarget ψ delta hdelta
400 (ProC := ProC) (X := X) (F := F) (H := H)
401 ψ delta hdelta hdelta_continuous hψ_continuous)
402 hbasis
404end
406end FoxDifferential