FoxDifferential/Completed/Continuous/Universal/System.lean
1import FoxDifferential.Completed.Continuous.Universal.FiniteStage
2import ProCGroups.InverseSystems.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Continuous/Universal/System.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 ProCGroups.ProC
24universe u
26variable (C : ProCGroups.FiniteGroupClass.{u})
27variable {G H : Type u}
28variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30variable (ψ : G →* H)
32/-- The inverse system of finite source/target/coefficient stages of `A_psi(C)`. -/
34 InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
35 X := fun i => ZCCompletedDifferentialModuleStage C ψ i
36 topologicalSpace := fun _ => ⊥
37 map := fun {i j} hij => zcCompletedDifferentialModuleStageTransition C ψ hij
38 continuous_map := by
39 intro i j hij
40 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := ⊥
41 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ j) := ⊥
42 letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ j) := ⟨rfl⟩
43 exact continuous_of_discreteTopology
44 map_id := by
45 intro i
46 funext x
47 exact congrFun
48 (congrArg DFunLike.coe
50 map_comp := by
51 intro i j k hij hjk
52 funext x
53 exact congrFun
54 (congrArg DFunLike.coe
55 (zcCompletedDifferentialModuleStageTransition_comp C ψ hij hjk)) x
58 (i : ZCCompletedDifferentialModuleIndex C ψ) :
59 AddCommGroup ((zcCompletedDifferentialModuleStageSystem C ψ).X i) := by
61 infer_instance
63/-- The finite stages of `A_psi(C)` form an additive-group-valued inverse system. -/
67 intro i j hij
68 exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_zero
70 intro i j hij x y
71 exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_add x y
72 map_neg := by
73 intro i j hij x
74 exact map_neg (zcCompletedDifferentialModuleStageTransition C ψ hij) x
76omit [IsTopologicalGroup G] in
77@[simp]
79 {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
80 (x : ZCCompletedDifferentialModuleStage C ψ j) :
81 (zcCompletedDifferentialModuleStageSystem C ψ).map hij x =
82 zcCompletedDifferentialModuleStageTransition C ψ hij x :=
83 rfl
85omit [IsTopologicalGroup G] in
86@[simp]
88 (x : (zcCompletedDifferentialModuleStageSystem C ψ).inverseLimit)
89 (i j : ZCCompletedDifferentialModuleIndex C ψ) (hij : i ≤ j) :
91 ((zcCompletedDifferentialModuleStageSystem C ψ).projection j x) =
92 (zcCompletedDifferentialModuleStageSystem C ψ).projection i x :=
93 (zcCompletedDifferentialModuleStageSystem C ψ).projection_compatible x i j hij
95/-- The inverse system of finite pre-modules before quotienting by crossed-differential
96relations. -/
98 InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
99 X := fun i =>
103 topologicalSpace := fun _ => ⊥
104 map := fun {i j} hij => zcCompletedDifferentialModulePreStageTransition C ψ hij
105 continuous_map := by
106 intro i j hij
107 letI : TopologicalSpace
110 (zcCompletedDifferentialModuleStageSource C ψ i)) := ⊥
111 letI : TopologicalSpace
114 (zcCompletedDifferentialModuleStageSource C ψ j)) := ⊥
115 letI : DiscreteTopology
118 (zcCompletedDifferentialModuleStageSource C ψ j)) := ⟨rfl⟩
119 exact continuous_of_discreteTopology
120 map_id := by
121 intro i
122 funext x
123 exact congrFun
124 (congrArg DFunLike.coe
126 map_comp := by
127 intro i j k hij hjk
128 funext x
129 exact congrFun
130 (congrArg DFunLike.coe
131 (zcCompletedDifferentialModulePreStageTransition_comp C ψ hij hjk)) x
133/-- Compatible inverse-limit families of finite pre-stage elements. -/
134abbrev ZCCompletedDifferentialPreModuleStageFamily : Type u :=
135 (zcCompletedDifferentialPreModuleStageSystem C ψ).inverseLimit
137omit [IsTopologicalGroup G] in
138@[simp]
140 {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
143 (zcCompletedDifferentialModuleStageSource C ψ j)) :
144 (zcCompletedDifferentialPreModuleStageSystem C ψ).map hij x =
145 zcCompletedDifferentialModulePreStageTransition C ψ hij x :=
146 rfl
148omit [IsTopologicalGroup G] in
149/-- The explicit finite pre-stage reductions of a completed pre-module element are compatible
153 (fun i : ZCCompletedDifferentialModuleIndex C ψ =>
154 zcCompletedDifferentialModulePreStageMap C ψ i) := by
155 intro i j hij
156 funext x
157 exact zcCompletedDifferentialModulePreStageTransition_preStageMap C ψ hij x
159/-- The map from the completed pre-module to the inverse limit of all finite pre-stages. -/
164 (fun i : ZCCompletedDifferentialModuleIndex C ψ =>
168omit [IsTopologicalGroup G] in
169@[simp]
171 (i : ZCCompletedDifferentialModuleIndex C ψ)
172 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
173 (zcCompletedDifferentialPreModuleStageSystem C ψ).projection i
175 zcCompletedDifferentialModulePreStageMap C ψ i x :=
176 rfl
178end
180end FoxDifferential