Source: ProCGroups.FoxDifferential.Completed.Continuous.PresentedCoordinates
1import ProCGroups.FoxDifferential.Common.FiniteFamilyLinearMap
2import ProCGroups.FoxDifferential.Completed.Continuous.Universal.NaturalTopology
4/-!
5# Fox differential: completed — continuous — presented coordinates
7The principal declarations in this module are:
9- `presentedCompletedDifferentialFamilyMapProCInteger`
10 The \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear family map sending the standard coordinate
11 vector \(e_i\) to d(family i).
12- `presentedSeparatedDifferentialFamilyMapProCInteger`
13 The finite-family map into the separated completed differential module.
14- `presentedCompletedDifferentialFamilyMapProCInteger_single`
15 The finite-family map sends the \(i\)-th standard coordinate vector to \(d(\mathrm{family}\ i)\).
16- `presentedSeparatedDifferentialFamilyMapProCInteger_single`
17 The separated finite-family map sends the \(i\)-th standard coordinate vector to the separated
18 differential of \(\mathrm{family}\ i\).
19-/
21namespace CrowellExactSequence
23noncomputable section
25open scoped BigOperators
26open FoxDifferential
28universe u v w
30variable {G H : Type u}
31variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35variable (C : ProCGroups.FiniteGroupClass.{u})
37/--
38The \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear family map sending the standard coordinate
39vector \(e_i\) to d(family i).
40-/
41def presentedCompletedDifferentialFamilyMapProCInteger
42 (psi : ContinuousMonoidHom G H)
43 {X : Type v} [Fintype X] (family : X -> G) :
44 (X -> ZCCompletedGroupAlgebra C H) →ₗ[ZCCompletedGroupAlgebra C H]
45 ZCCompletedDifferentialModule C psi.toMonoidHom :=
46 finiteFamilyLinearMap
47 (R := ZCCompletedGroupAlgebra C H)
48 (fun i : X => zcUniversalDifferential C psi.toMonoidHom (family i))
50omit [IsTopologicalGroup G] in
51/--
52The finite-family map sends the \(i\)-th standard coordinate vector to \(d(\mathrm{family}\
53i)\).
54-/
55@[simp]
56theorem presentedCompletedDifferentialFamilyMapProCInteger_single
57 (psi : ContinuousMonoidHom G H)
58 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) (i : X) :
59 presentedCompletedDifferentialFamilyMapProCInteger
60 (G := G) (H := H) C psi family (Pi.single i 1) =
61 zcUniversalDifferential C psi.toMonoidHom (family i) := by
62 exact
63 finiteFamilyLinearMap_single
64 (R := ZCCompletedGroupAlgebra C H)
65 (fun i : X => zcUniversalDifferential C psi.toMonoidHom (family i)) i
67/-- The finite-family map into the separated completed differential module. -/
68def presentedSeparatedDifferentialFamilyMapProCInteger
69 (psi : ContinuousMonoidHom G H)
70 {X : Type v} [Fintype X] (family : X -> G) :
71 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
72 ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
73 finiteFamilyLinearMap
74 (R := ZCCompletedGroupAlgebra C H)
75 (fun i : X => zcSeparatedUniversalDifferential C psi.toMonoidHom (family i))
77omit [IsTopologicalGroup G] in
78/--
79The separated finite-family map sends the \(i\)-th standard coordinate vector to the separated
80differential of \(\mathrm{family}\ i\).
81-/
82@[simp]
83theorem presentedSeparatedDifferentialFamilyMapProCInteger_single
84 (psi : ContinuousMonoidHom G H)
85 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) (i : X) :
86 presentedSeparatedDifferentialFamilyMapProCInteger
87 (G := G) (H := H) C psi family (Pi.single i 1) =
88 zcSeparatedUniversalDifferential C psi.toMonoidHom (family i) := by
89 exact
90 finiteFamilyLinearMap_single
91 (R := ZCCompletedGroupAlgebra C H)
92 (fun i : X => zcSeparatedUniversalDifferential C psi.toMonoidHom (family i)) i
94omit [IsTopologicalGroup G] in
95/--
96Projecting the separated finite-family map to a finite stage agrees with projecting the
97algebraic finite-family map to the same finite stage.
98-/
99theorem zcSepDiffModuleStageProj_comp_presentedSepFamilyMap
100 (psi : ContinuousMonoidHom G H)
101 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
102 (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :
103 (zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i).comp
104 (presentedSeparatedDifferentialFamilyMapProCInteger
105 (G := G) (H := H) C psi family) =
106 (zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i).comp
107 (presentedCompletedDifferentialFamilyMapProCInteger
108 (G := G) (H := H) C psi family) := by
109 apply linearMap_ext_pi_single
110 intro x
111 rw [LinearMap.comp_apply, LinearMap.comp_apply,
112 presentedSeparatedDifferentialFamilyMapProCInteger_single,
113 presentedCompletedDifferentialFamilyMapProCInteger_single,
114 zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal,
115 zcCompletedDifferentialModuleStageProjection_universal]
117omit [IsTopologicalGroup G] in
118/--
119The finite-family map into \(A_{\psi}(C)\) is continuous for the finite-stage completed
120topology on \(A_{\psi}(C)\).
121-/
122theorem continuous_presentedCompletedDifferentialFamilyMapProCInteger_naturalTopology
123 (psi : ContinuousMonoidHom G H)
124 {X : Type v} [Fintype X] (family : X -> G) :
125 @Continuous
126 (ZCFreeFoxCoordinates C (X := X) (H := H))
127 (ZCCompletedDifferentialModule C psi.toMonoidHom)
128 inferInstance
129 (zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
130 (presentedCompletedDifferentialFamilyMapProCInteger
131 (G := G) (H := H) C psi family) := by
132 classical
133 rw [continuous_induced_rng]
134 change Continuous
135 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
136 fun i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom =>
137 zcCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
138 (presentedCompletedDifferentialFamilyMapProCInteger
139 (G := G) (H := H) C psi family x))
140 refine continuous_pi fun i => ?_
141 letI : TopologicalSpace (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom i) :=
142 inferInstance
143 letI : DiscreteTopology (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom i) :=
144 inferInstance
145 have hstageAction :
146 Continuous (fun p : zcCompletedDifferentialModuleStageRing C psi.toMonoidHom i ×
147 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i => p.1 • p.2) :=
148 continuous_of_discreteTopology
149 have hsum :
150 Continuous
151 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
152 ∑ k, x k •
153 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i (family k)) := by
154 refine continuous_finsetSum _ fun k _ => ?_
155 have hcoeff :
156 Continuous (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
157 zcCompletedGroupAlgebraProjectionRingHom C H i.target (x k)) :=
158 (continuous_zcCompletedGroupAlgebraProjectionRingHom (C := C) (G := H) i.target).comp
159 (continuous_apply k)
160 have hconst :
161 Continuous (fun _ : ZCFreeFoxCoordinates C (X := X) (H := H) =>
162 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i (family k)) :=
163 continuous_const
164 have hterm := hstageAction.comp (hcoeff.prodMk hconst)
165 change Continuous
166 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
167 x k • zcCompletedDifferentialModuleStageDifferential
168 C psi.toMonoidHom i (family k)) at hterm
169 exact hterm
170 have hfun :
171 (fun a : ZCFreeFoxCoordinates C (X := X) (H := H) =>
172 zcCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
173 (presentedCompletedDifferentialFamilyMapProCInteger
174 (G := G) (H := H) C psi family a)) =
175 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
176 ∑ k, x k •
177 zcCompletedDifferentialModuleStageDifferential
178 C psi.toMonoidHom i (family k)) := by
179 funext a
180 simp only [zcCompletedDifferentialModuleStageProjectionAdd_apply,
181 presentedCompletedDifferentialFamilyMapProCInteger,
182 finiteFamilyLinearMap_apply,
183 map_sum, map_smul, zcCompletedDifferentialModuleStageProjection_universal]
184 rw [hfun]
185 exact hsum
187/-- The basis property for a finite family in the Fox completed differential module. -/
188def IsPresentedCompletedDifferentialFamilyBasisProCInteger
189 (psi : ContinuousMonoidHom G H)
190 {X : Type v} [Fintype X] (family : X -> G) : Prop :=
191 Function.Bijective
192 (presentedCompletedDifferentialFamilyMapProCInteger
193 (G := G) (H := H) C psi family)
195omit [IsTopologicalGroup G] in
196/-- The completed differential basis property is invariant under reindexing a finite family. -/
197theorem isPresentedCompletedDifferentialFamilyBasisProCInteger_reindex
198 (psi : ContinuousMonoidHom G H)
199 {X : Type v} [Fintype X]
200 {Y : Type w} [Fintype Y]
201 (e : X ≃ Y) (family : Y -> G)
202 (hbasis_A :
203 IsPresentedCompletedDifferentialFamilyBasisProCInteger
204 (G := G) (H := H) C psi family) :
205 IsPresentedCompletedDifferentialFamilyBasisProCInteger
206 (G := G) (H := H) C psi (fun x : X => family (e x)) := by
207 classical
208 dsimp [IsPresentedCompletedDifferentialFamilyBasisProCInteger]
209 have hmap :
210 presentedCompletedDifferentialFamilyMapProCInteger
211 (G := G) (H := H) C psi (fun x : X => family (e x)) =
212 (presentedCompletedDifferentialFamilyMapProCInteger
213 (G := G) (H := H) C psi family).comp
214 (piReindexLinearEquiv
215 (R := ZCCompletedGroupAlgebra C H) e).toLinearMap := by
216 simpa [presentedCompletedDifferentialFamilyMapProCInteger] using
217 (finiteFamilyLinearMap_reindex
218 (R := ZCCompletedGroupAlgebra C H)
219 (M := ZCCompletedDifferentialModule C psi.toMonoidHom)
220 e (fun y : Y => zcUniversalDifferential C psi.toMonoidHom (family y)))
221 rw [hmap]
222 exact hbasis_A.comp
223 (piReindexLinearEquiv
224 (R := ZCCompletedGroupAlgebra C H) e).bijective
226/-- Coordinates associated to a basis family in \(A_{\psi}(C)\). -/
227def presentedCompletedDifferentialFamilyCoordinatesProCInteger
228 (psi : ContinuousMonoidHom G H)
229 {X : Type v} [Fintype X] (family : X -> G)
230 (hbasis_A :
231 IsPresentedCompletedDifferentialFamilyBasisProCInteger
232 (G := G) (H := H) C psi family) :
233 ZCCompletedDifferentialModule C psi.toMonoidHom ≃ₗ[ZCCompletedGroupAlgebra C H]
234 (X -> ZCCompletedGroupAlgebra C H) :=
235 (LinearEquiv.ofBijective
236 (presentedCompletedDifferentialFamilyMapProCInteger
237 (G := G) (H := H) C psi family)
238 hbasis_A).symm
240omit [IsTopologicalGroup G] in
241/-- The inverse coordinate equivalence has underlying linear map equal to the finite-family map. -/
242theorem presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap
243 (psi : ContinuousMonoidHom G H)
244 {X : Type v} [Fintype X] (family : X -> G)
245 (hbasis_A :
246 IsPresentedCompletedDifferentialFamilyBasisProCInteger
247 (G := G) (H := H) C psi family) :
248 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
249 (G := G) (H := H) C psi family hbasis_A).symm.toLinearMap =
250 presentedCompletedDifferentialFamilyMapProCInteger
251 (G := G) (H := H) C psi family :=
252 rfl
254omit [IsTopologicalGroup G] in
255/--
256The coordinate equivalence sends \(d(\mathrm{family}\ i)\) to the \(i\)-th standard coordinate
257vector.
258-/
259@[simp 900]
260theorem presentedCompletedDifferentialFamilyCoordinatesProCInteger_d_family
261 (psi : ContinuousMonoidHom G H)
262 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
263 (hbasis_A :
264 IsPresentedCompletedDifferentialFamilyBasisProCInteger
265 (G := G) (H := H) C psi family) (i : X) :
266 presentedCompletedDifferentialFamilyCoordinatesProCInteger
267 (G := G) (H := H) C psi family hbasis_A
268 (zcUniversalDifferential C psi.toMonoidHom (family i)) =
269 Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
270 let coords :=
271 presentedCompletedDifferentialFamilyCoordinatesProCInteger
272 (G := G) (H := H) C psi family hbasis_A
273 have hsingle :
274 coords.symm (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
275 zcUniversalDifferential C psi.toMonoidHom (family i) := by
276 change
277 presentedCompletedDifferentialFamilyMapProCInteger
278 (G := G) (H := H) C psi family (Pi.single i 1) =
279 zcUniversalDifferential C psi.toMonoidHom (family i)
280 exact presentedCompletedDifferentialFamilyMapProCInteger_single
281 (G := G) (H := H) C psi family i
282 calc
283 coords (zcUniversalDifferential C psi.toMonoidHom (family i)) =
284 coords (coords.symm (Pi.single i (1 : ZCCompletedGroupAlgebra C H))) := by
285 rw [hsingle]
286 _ = Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
287 exact coords.apply_symm_apply (Pi.single i (1 : ZCCompletedGroupAlgebra C H))
289end
291end CrowellExactSequence