Source: ProCGroups.FoxDifferential.Completed.Continuous.Universal.System
1import ProCGroups.FoxDifferential.Completed.Continuous.Universal.FiniteStage
2import ProCGroups.InverseSystems.Basic
4/-!
5# Fox differential: completed — continuous — universal — system
7The principal declarations in this module are:
9- `zcCompletedDifferentialModuleStageSystem`
10 The inverse system of finite source, target, and coefficient stages of \(A_{\psi}(C)\).
11- `zcCompletedDifferentialPreModuleStageSystem`
12 The inverse system of finite pre-modules before quotienting by crossed-differential relations.
13- `zcCompletedDifferentialModuleStageSystem_map_apply`
14 The system map on completed differential modules is evaluated coordinatewise at each finite
15 coefficient stage.
16- `zcCompletedDifferentialModuleStageSystem_projection_compatible`
17 Inverse-limit projections of the finite \(A_{\psi}(C)\) stage system are compatible with
18 transition maps.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
30variable (C : ProCGroups.FiniteGroupClass.{u})
31variable {G H : Type u}
32variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34variable (ψ : G →* H)
36/-- The inverse system of finite source, target, and coefficient stages of \(A_{\psi}(C)\). -/
37def zcCompletedDifferentialModuleStageSystem :
38 InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
39 X := fun i => ZCCompletedDifferentialModuleStage C ψ i
40 topologicalSpace := fun _ => ⊥
41 map := fun {i j} hij => zcCompletedDifferentialModuleStageTransition C ψ hij
42 continuous_map := by
43 intro i j hij
44 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ i) := ⊥
45 letI : TopologicalSpace (ZCCompletedDifferentialModuleStage C ψ j) := ⊥
46 letI : DiscreteTopology (ZCCompletedDifferentialModuleStage C ψ j) := ⟨rfl⟩
47 exact continuous_of_discreteTopology
48 map_id := by
49 intro i
50 funext x
51 exact congrFun
52 (congrArg DFunLike.coe
53 (zcCompletedDifferentialModuleStageTransition_id C ψ i)) x
54 map_comp := by
55 intro i j k hij hjk
56 funext x
57 exact congrFun
58 (congrArg DFunLike.coe
59 (zcCompletedDifferentialModuleStageTransition_comp C ψ hij hjk)) x
61/-- Addition in the finite-stage completed differential-module system is defined coordinatewise. -/
62instance instAddCommGroupZCCompletedDifferentialModuleStageSystemStage
63 (i : ZCCompletedDifferentialModuleIndex C ψ) :
64 AddCommGroup ((zcCompletedDifferentialModuleStageSystem C ψ).X i) := by
65 dsimp [zcCompletedDifferentialModuleStageSystem]
66 infer_instance
68/--
69The inverse system of finite-stage group algebras has addition defined coordinatewise on
70compatible families.
71-/
72instance instIsAddGroupSystemZCCompletedDifferentialModuleStageSystem :
73 IsAddGroupSystem (zcCompletedDifferentialModuleStageSystem C ψ) where
74 map_zero := by
75 intro i j hij
76 exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_zero
77 map_add := by
78 intro i j hij x y
79 exact (zcCompletedDifferentialModuleStageTransition C ψ hij).map_add x y
80 map_neg := by
81 intro i j hij x
82 exact map_neg (zcCompletedDifferentialModuleStageTransition C ψ hij) x
84omit [IsTopologicalGroup G] in
85/--
86The system map on completed differential modules is evaluated coordinatewise at each finite
87coefficient stage.
88-/
89@[simp]
90theorem zcCompletedDifferentialModuleStageSystem_map_apply
91 {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
92 (x : ZCCompletedDifferentialModuleStage C ψ j) :
93 (zcCompletedDifferentialModuleStageSystem C ψ).map hij x =
94 zcCompletedDifferentialModuleStageTransition C ψ hij x :=
95 rfl
97omit [IsTopologicalGroup G] in
98/--
99Inverse-limit projections of the finite \(A_{\psi}(C)\) stage system are compatible with
100transition maps.
101-/
102@[simp]
103theorem zcCompletedDifferentialModuleStageSystem_projection_compatible
104 (x : (zcCompletedDifferentialModuleStageSystem C ψ).inverseLimit)
105 (i j : ZCCompletedDifferentialModuleIndex C ψ) (hij : i ≤ j) :
106 zcCompletedDifferentialModuleStageTransition C ψ hij
107 ((zcCompletedDifferentialModuleStageSystem C ψ).projection j x) =
108 (zcCompletedDifferentialModuleStageSystem C ψ).projection i x :=
109 (zcCompletedDifferentialModuleStageSystem C ψ).projection_compatible x i j hij
111/--
112The inverse system of finite pre-modules before quotienting by crossed-differential relations.
113-/
114def zcCompletedDifferentialPreModuleStageSystem :
115 InverseSystem (I := ZCCompletedDifferentialModuleIndex C ψ) where
116 X := fun i =>
117 CrossedDifferentialPreModule
118 (zcCompletedDifferentialModuleStageRing C ψ i)
119 (zcCompletedDifferentialModuleStageSource C ψ i)
120 topologicalSpace := fun _ => ⊥
121 map := fun {i j} hij => zcCompletedDifferentialModulePreStageTransition C ψ hij
122 continuous_map := by
123 intro i j hij
124 letI : TopologicalSpace
125 (CrossedDifferentialPreModule
126 (zcCompletedDifferentialModuleStageRing C ψ i)
127 (zcCompletedDifferentialModuleStageSource C ψ i)) := ⊥
128 letI : TopologicalSpace
129 (CrossedDifferentialPreModule
130 (zcCompletedDifferentialModuleStageRing C ψ j)
131 (zcCompletedDifferentialModuleStageSource C ψ j)) := ⊥
132 letI : DiscreteTopology
133 (CrossedDifferentialPreModule
134 (zcCompletedDifferentialModuleStageRing C ψ j)
135 (zcCompletedDifferentialModuleStageSource C ψ j)) := ⟨rfl⟩
136 exact continuous_of_discreteTopology
137 map_id := by
138 intro i
139 funext x
140 exact congrFun
141 (congrArg DFunLike.coe
142 (zcCompletedDifferentialModulePreStageTransition_id C ψ i)) x
143 map_comp := by
144 intro i j k hij hjk
145 funext x
146 exact congrFun
147 (congrArg DFunLike.coe
148 (zcCompletedDifferentialModulePreStageTransition_comp C ψ hij hjk)) x
150/-- Compatible inverse-limit families of finite pre-stage elements. -/
151abbrev ZCCompletedDifferentialPreModuleStageFamily : Type u :=
152 (zcCompletedDifferentialPreModuleStageSystem C ψ).inverseLimit
154omit [IsTopologicalGroup G] in
155/--
156The finite pre-module inverse-system map evaluates as the explicit pre-stage transition.
157-/
158@[simp]
159theorem zcCompletedDifferentialPreModuleStageSystem_map_apply
160 {i j : ZCCompletedDifferentialModuleIndex C ψ} (hij : i ≤ j)
161 (x : CrossedDifferentialPreModule
162 (zcCompletedDifferentialModuleStageRing C ψ j)
163 (zcCompletedDifferentialModuleStageSource C ψ j)) :
164 (zcCompletedDifferentialPreModuleStageSystem C ψ).map hij x =
165 zcCompletedDifferentialModulePreStageTransition C ψ hij x :=
166 rfl
168omit [IsTopologicalGroup G] in
169/--
170The explicit finite pre-stage reductions of a completed pre-module element are compatible with
171finite transitions.
172-/
173theorem zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap :
174 (zcCompletedDifferentialPreModuleStageSystem C ψ).CompatibleMaps
175 (fun i : ZCCompletedDifferentialModuleIndex C ψ =>
176 zcCompletedDifferentialModulePreStageMap C ψ i) := by
177 intro i j hij
178 funext x
179 exact zcCompletedDifferentialModulePreStageTransition_preStageMap C ψ hij x
181/--
182The finite-stage family map sends a completed pre-module element to its compatible family of
183finite source, target, and coefficient stages.
184-/
185def zcCompletedDifferentialPreModuleStageFamilyMap :
186 CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →
187 ZCCompletedDifferentialPreModuleStageFamily C ψ :=
188 (zcCompletedDifferentialPreModuleStageSystem C ψ).inverseLimitLift
189 (fun i : ZCCompletedDifferentialModuleIndex C ψ =>
190 zcCompletedDifferentialModulePreStageMap C ψ i)
191 (zcCompletedDifferentialPreModuleStageSystem_compatible_preStageMap C ψ)
193omit [IsTopologicalGroup G] in
194/--
195Projecting the finite-stage pre-module family map at a stage recovers the explicit pre-stage map
196at that stage.
197-/
198@[simp]
199theorem zcCompletedDifferentialPreModuleStageFamilyMap_projection
200 (i : ZCCompletedDifferentialModuleIndex C ψ)
201 (x : CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :
202 (zcCompletedDifferentialPreModuleStageSystem C ψ).projection i
203 (zcCompletedDifferentialPreModuleStageFamilyMap C ψ x) =
204 zcCompletedDifferentialModulePreStageMap C ψ i x :=
205 rfl
207end
209end FoxDifferential