FoxDifferential/Completed/Continuous/Naturality.lean
1import FoxDifferential.Completed.Continuous.Free.Rules
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/Naturality.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Continuous crossed differentials
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.Completion
21open ProCGroups.InverseSystems
22open ProCGroups.ProC
23open scoped BigOperators
25universe u v
27section ContinuousTargetMaps
29variable (C : ProCGroups.FiniteGroupClass.{u})
30variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
31variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
32variable {H K : Type u}
33variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
36omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
37/-- The completed group-algebra map induced by a continuous target homomorphism is continuous. -/
38theorem continuous_zcCompletedGroupAlgebraMap (η : H →ₜ* K) :
39 Continuous (zcCompletedGroupAlgebraMap C hC η) := by
40 refine Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible C K)
41 (continuous_pi fun i => ?_) (fun x => (zcCompletedGroupAlgebraMap C hC η x).2)
42 let sourceIndex : ZCCompletedGroupAlgebraIndex C H :=
43 (i.1, completedGroupAlgebraComapIndexInClass
44 (G := H) (H := K) C hC η i.2)
45 letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H sourceIndex) := ⊥
46 letI : DiscreteTopology (ZCCompletedGroupAlgebraStage C H sourceIndex) := ⟨rfl⟩
47 have hstage : Continuous (zcCompletedGroupAlgebraMapStage C hC η i) :=
48 continuous_of_discreteTopology
49 exact hstage.comp ((continuous_apply sourceIndex).comp continuous_subtype_val)
51/-- A surjective target homomorphism induces a surjective completed group-algebra map. -/
54 (hForm : ProCGroups.FiniteGroupClass.Formation C)
55 (η : H →ₜ* K) (hη : Function.Surjective η) :
56 Function.Surjective (zcCompletedGroupAlgebraMap C hC η) := by
57 let S := zcCompletedGroupAlgebraSystem C K
58 let ψ : ∀ i : ZCCompletedGroupAlgebraIndex C K,
59 ZCCompletedGroupAlgebra C H → S.X i :=
60 fun i x => zcCompletedGroupAlgebraProjection C K i
61 (zcCompletedGroupAlgebraMap C hC η x)
62 have hψcont : ∀ i, Continuous (ψ i) := by
63 intro i
64 exact (continuous_apply i).comp
65 (continuous_subtype_val.comp (continuous_zcCompletedGroupAlgebraMap C hC η))
66 have hψcompat : S.CompatibleMaps ψ := by
67 intro i j hij
68 funext x
69 change zcCompletedGroupAlgebraTransition C K hij
71 (zcCompletedGroupAlgebraMap C hC η x)) =
73 (zcCompletedGroupAlgebraMap C hC η x)
74 exact (zcCompletedGroupAlgebraMap C hC η x).2 i j hij
75 have hψsurj : ∀ i, Function.Surjective (ψ i) := by
76 intro i y
78 C hC η hη i y with ⟨y₀, hy₀⟩
79 rcases zcCompletedGroupAlgebraProjection_surjective C H
80 (i.1, completedGroupAlgebraComapIndexInClass
81 (G := H) (H := K) C hC η i.2) y₀ with ⟨x, hx⟩
82 refine ⟨x, ?_⟩
83 dsimp [ψ]
84 rw [hx, hy₀]
85 letI : Nonempty (ZCCompletedGroupAlgebraIndex C K) :=
86 ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, zcCompletedGroupAlgebraTopIndex C K)⟩
87 have hdir : Directed (· ≤ ·)
88 (id : ZCCompletedGroupAlgebraIndex C K → ZCCompletedGroupAlgebraIndex C K) := by
89 intro i j
90 rcases ProCIntegerIndex.directed_of_formation hForm i.1 j.1 with
91 ⟨n, hin, hjn⟩
93 (C := C) (G := K) hForm i.2 j.2 with
94 ⟨U, hiU, hjU⟩
95 exact ⟨(n, U), ⟨hin, hiU⟩, ⟨hjn, hjU⟩⟩
96 letI : ∀ i : ZCCompletedGroupAlgebraIndex C K, T2Space (S.X i) := fun i => by
97 dsimp [S, zcCompletedGroupAlgebraSystem]
98 infer_instance
99 have hlift : Function.Surjective (S.inverseLimitLift ψ hψcompat) :=
100 S.surjective_inverseLimitLift ψ hψcont hψcompat hψsurj hdir
101 intro y
102 rcases hlift y with ⟨x, hx⟩
103 refine ⟨x, ?_⟩
104 apply Subtype.ext
105 funext i
106 have hi := congrArg (fun z : S.inverseLimit => S.projection i z) hx
107 simpa [S, ψ] using hi
109/-- A surjective completed group-algebra map is a quotient map. -/
112 (hForm : ProCGroups.FiniteGroupClass.Formation C)
113 (η : H →ₜ* K) (hη : Function.Surjective η) :
114 Topology.IsQuotientMap (zcCompletedGroupAlgebraMap C hC η) :=
115 IsQuotientMap.of_surjective_continuous
116 (zcCompletedGroupAlgebraMap_surjective_of_surjective C hC hForm η hη)
117 (continuous_zcCompletedGroupAlgebraMap C hC η)
119/-- A surjective completed group-algebra map is an open quotient map as an additive-group
120homomorphism. -/
123 (hForm : ProCGroups.FiniteGroupClass.Formation C)
124 (η : H →ₜ* K) (hη : Function.Surjective η) :
125 IsOpenQuotientMap (zcCompletedGroupAlgebraMap C hC η) :=
126 AddMonoidHom.isOpenQuotientMap_of_isQuotientMap
127 (isQuotientMap_zcCompletedGroupAlgebraMap_of_surjective C hC hForm η hη)
129variable {X : Type v}
131omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
132/-- The coordinatewise target map on completed Fox-coordinate vectors is continuous. -/
133theorem continuous_zcFreeFoxCoordinatesMap (η : H →ₜ* K) :
134 Continuous (zcFreeFoxCoordinatesMap (X := X) C hC η) := by
135 refine continuous_pi fun x => ?_
136 exact (continuous_zcCompletedGroupAlgebraMap C hC η).comp (continuous_apply x)
138end ContinuousTargetMaps
140section SourceBoundaryNaturality
142variable (C : ProCGroups.FiniteGroupClass.{u})
143variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
144variable {X H K : Type u} [Fintype X]
145variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
146variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
148/-- Source-shaped completed Fox boundary maps are natural in the target group. -/
150 (η : H →ₜ* K) (φ : X → H)
151 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
152 zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v) =
153 freeProCZCCompletedFoxBoundary C (fun x : X => η (φ x))
154 (zcFreeFoxCoordinatesMap (X := X) C hC η v) := by
155 simp only [freeProCZCCompletedFoxBoundary_apply, map_sum, map_mul, map_sub,
158end SourceBoundaryNaturality
160section SemidirectTargetMap
162variable (C : ProCGroups.FiniteGroupClass.{u})
163variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
164variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
165variable {X H K : Type u} [DecidableEq X]
166variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
167variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
169/-- Target functoriality for completed Fox semidirect products. -/
170def zcCompletedFoxSemidirectMapTarget (η : H →ₜ* K) :
171 ZCCompletedFoxSemidirect C X H →* ZCCompletedFoxSemidirect C X K where
172 toFun a :=
173 { left := zcFreeFoxCoordinatesMap (X := X) C hC η a.left
174 right := η a.right }
175 map_one' := by
176 ext x
177 · simp only [ZCCompletedFoxSemidirect.one_left, zcFreeFoxCoordinatesMap_apply,
178 Pi.zero_apply, map_zero, zcCompletedGroupAlgebraProjection_zero, Finsupp.coe_zero]
180 map_mul' a b := by
181 ext x
182 · simp only [ZCCompletedFoxSemidirect.mul_left, zcFreeFoxCoordinatesMap_apply,
186 zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply,
187 MonoidAlgebra.coe_add, MonoidAlgebra.single_mul_apply, one_mul]
190omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
191/-- Left component of the target map on completed Fox semidirect products. -/
192@[simp]
194 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
195 (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).left =
196 zcFreeFoxCoordinatesMap (X := X) C hC η a.left :=
197 rfl
199omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
200/-- Right component of the target map on completed Fox semidirect products. -/
201@[simp]
203 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
204 (zcCompletedFoxSemidirectMapTarget (X := X) C hC η a).right = η a.right :=
205 rfl
207omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
208/-- The target map on completed Fox semidirect products is continuous. -/
210 (η : H →ₜ* K) :
211 Continuous (zcCompletedFoxSemidirectMapTarget (X := X) C hC η) := by
212 rw [continuous_induced_rng]
213 refine (continuous_zcFreeFoxCoordinatesMap (X := X) C hC η).comp
214 (continuous_zcCompletedFoxSemidirect_left C X H) |>.prodMk ?_
215 exact η.continuous_toFun.comp (continuous_zcCompletedFoxSemidirect_right C X H)
217/-- Target functoriality for completed Fox semidirect products as a continuous homomorphism. -/
218def zcCompletedFoxSemidirectMapTargetHom (η : H →ₜ* K) :
219 ZCCompletedFoxSemidirect C X H →ₜ* ZCCompletedFoxSemidirect C X K where
220 toMonoidHom := zcCompletedFoxSemidirectMapTarget (X := X) C hC η
221 continuous_toFun := continuous_zcCompletedFoxSemidirectMapTarget (X := X) C hC η
223omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
224/-- The continuous target map has the expected underlying homomorphism. -/
225@[simp]
227 (η : H →ₜ* K) :
228 (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η).toMonoidHom =
229 zcCompletedFoxSemidirectMapTarget (X := X) C hC η :=
230 rfl
232omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
233/-- Left component of the continuous target map on completed Fox semidirect products. -/
234@[simp]
236 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
237 (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).left =
238 zcFreeFoxCoordinatesMap (X := X) C hC η a.left :=
239 rfl
241omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
242/-- Right component of the continuous target map on completed Fox semidirect products. -/
243@[simp]
245 (η : H →ₜ* K) (a : ZCCompletedFoxSemidirect C X H) :
246 (zcCompletedFoxSemidirectMapTargetHom (X := X) C hC η a).right = η a.right :=
247 rfl
249end SemidirectTargetMap
251section SourceNaturality
253variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
254variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
255variable (hC : ProCGroups.FiniteGroupClass.Hereditary ProC.finiteQuotientClass)
256include hC
257variable {X F H K : Type u}
258variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
259variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
260variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
261variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
263omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] [Fintype X] in
264/-- Target naturality of the canonical completed Fox semidirect lift. -/
266 {ι : X → F}
267 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
268 (htargetH :
269 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
270 (htargetK :
271 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K))
272 (η : H →ₜ* K) (φ : X → H) (g : F) :
273 zcCompletedFoxSemidirectMapTarget (X := X) ProC.finiteQuotientClass hC η
275 (ProC := ProC) hι htargetH φ
277 (ProC := ProC) X H φ) g) =
279 (ProC := ProC) hι htargetK (fun x : X => η (φ x))
281 (ProC := ProC) X K (fun x : X => η (φ x))) g := by
282 let hφH : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) :=
283 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X H φ
284 let φK : X → K := fun x => η (φ x)
285 let hφK : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φK) :=
286 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X K φK
287 let f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K :=
288 (zcCompletedFoxSemidirectMapTarget (X := X) ProC.finiteQuotientClass hC η).comp
290 (ProC := ProC) hι htargetH φ hφH)
291 let h : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K :=
293 (ProC := ProC) hι htargetK φK hφK
294 have hf_continuous : Continuous f :=
296 (X := X) ProC.finiteQuotientClass hC η).comp
298 (ProC := ProC) hι htargetH φ hφH)
299 have hh_continuous : Continuous h :=
301 (ProC := ProC) hι htargetK φK hφK
302 have hfg : ∀ x : X, f (ι x) = h (ι x) := by
303 intro x
304 apply ZCCompletedFoxSemidirect.ext
305 · funext y
306 by_cases hxy : x = y
307 · subst y
308 simp only [MonoidHom.coe_comp, Function.comp_apply, freeProCZCCompletedFoxSemidirectLift_generator,
309 zcCompletedFoxSemidirectMapTarget_left, zcFreeFoxCoordinatesMap, freeProCZCCompletedFoxSemidirectGenerator_left,
311 · simp only [MonoidHom.coe_comp, Function.comp_apply, freeProCZCCompletedFoxSemidirectLift_generator,
312 zcCompletedFoxSemidirectMapTarget_left, zcFreeFoxCoordinatesMap, freeProCZCCompletedFoxSemidirectGenerator_left,
314 · simp only [MonoidHom.coe_comp, Function.comp_apply, freeProCZCCompletedFoxSemidirectLift_generator,
315 zcCompletedFoxSemidirectMapTarget_right, freeProCZCCompletedFoxSemidirectGenerator_right, f, h, φK]
316 have hfh : f = h := hι.hom_ext htargetK hf_continuous hh_continuous hfg
317 exact congrFun (congrArg DFunLike.coe hfh) g
319omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] [Fintype X] in
320/-- Continuous-hom form of target naturality for the canonical completed Fox semidirect lift. -/
322 {ι : X → F}
323 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
324 (htargetH :
325 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
326 (htargetK :
327 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K))
328 (η : H →ₜ* K) (φ : X → H) :
329 (zcCompletedFoxSemidirectMapTargetHom (X := X) ProC.finiteQuotientClass hC η).comp
331 (ProC := ProC) hι htargetH φ
333 (ProC := ProC) X H φ)) =
335 (ProC := ProC) hι htargetK (fun x : X => η (φ x))
337 (ProC := ProC) X K (fun x : X => η (φ x))) := by
338 apply ContinuousMonoidHom.ext
339 intro g
341 (ProC := ProC) (X := X) (F := F) (H := H) (K := K)
342 hC hι htargetH htargetK η φ g
344omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] [Fintype X] in
345/-- Target naturality of the right homomorphism of the canonical completed Fox lift. -/
347 {ι : X → F}
348 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
349 (htargetH :
350 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
351 (htargetK :
352 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K))
353 (η : H →ₜ* K) (φ : X → H) :
355 (ProC := ProC) hι htargetK (fun x : X => η (φ x))
357 (ProC := ProC) X K (fun x : X => η (φ x))) =
358 η.toMonoidHom.comp
360 (ProC := ProC) hι htargetH φ
362 (ProC := ProC) X H φ)) := by
363 ext g
364 have h := congrArg ZCCompletedFoxSemidirect.right
366 (ProC := ProC) (X := X) (F := F) (H := H) (K := K)
367 hC hι htargetH htargetK η φ g)
368 simpa [freeProCZCCompletedFoxRightHom_apply, MonoidHom.comp_apply] using h.symm
370omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] [Fintype X] in
371/-- Target naturality of the derivative vector of the canonical completed Fox lift. -/
373 {ι : X → F}
374 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
375 (htargetH :
376 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
377 (htargetK :
378 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K))
379 (η : H →ₜ* K) (φ : X → H) (g : F) :
381 (ProC := ProC) hι htargetK (fun x : X => η (φ x))
383 (ProC := ProC) X K (fun x : X => η (φ x))) g =
384 zcFreeFoxCoordinatesMap (X := X) ProC.finiteQuotientClass hC η
386 (ProC := ProC) hι htargetH φ
388 (ProC := ProC) X H φ) g) := by
389 have h := congrArg ZCCompletedFoxSemidirect.left
391 (ProC := ProC) (X := X) (F := F) (H := H) (K := K)
392 hC hι htargetH htargetK η φ g)
393 simpa [freeProCZCCompletedFoxDerivativeVector] using h.symm
395omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] [Fintype X] in
396/-- Component form of target naturality for the canonical completed Fox derivative. -/
398 {ι : X → F}
399 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
400 (htargetH :
401 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
402 (htargetK :
403 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K))
404 (η : H →ₜ* K) (φ : X → H) (g : F) (x : X) :
406 (ProC := ProC) hι htargetK (fun x : X => η (φ x))
408 (ProC := ProC) X K (fun x : X => η (φ x))) g x =
409 zcCompletedGroupAlgebraMap ProC.finiteQuotientClass hC η
411 (ProC := ProC) hι htargetH φ
413 (ProC := ProC) X H φ) g x) := by
414 have h := congrFun
416 (ProC := ProC) (X := X) (F := F) (H := H) (K := K)
417 hC hι htargetH htargetK η φ g) x
418 simpa [zcFreeFoxCoordinatesMap] using h
420omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
421/-- Target naturality for the source-shaped boundary applied to the canonical completed Fox
422derivative vector. -/
424 {ι : X → F}
425 (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
426 (htargetH :
427 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
428 (htargetK :
429 ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X K))
430 (η : H →ₜ* K) (φ : X → H) (g : F) :
431 zcCompletedGroupAlgebraMap ProC.finiteQuotientClass hC η
432 (freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass φ
434 (ProC := ProC) hι htargetH φ
436 (ProC := ProC) X H φ) g)) =
437 freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass (fun x : X => η (φ x))
439 (ProC := ProC) hι htargetK (fun x : X => η (φ x))
441 (ProC := ProC) X K (fun x : X => η (φ x))) g) := by
444 (ProC := ProC) (X := X) (F := F) (H := H) (K := K)
445 hC hι htargetH htargetK η φ g]
447end SourceNaturality
449end
451end FoxDifferential