Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.FreeProC.Coordinates
ProCGroups/FoxDifferential/Completed/FreeProC/Coordinates/Source

Source: ProCGroups.FoxDifferential.Completed.FreeProC.Coordinates

1import ProCGroups.FoxDifferential.Completed.FreeProC.NaturalTopology
2import ProCGroups.FoxDifferential.Completed.Continuous.Magnus.KernelClosedCommutator
3import ProCGroups.FreeProC.FiniteBasis
5/-!
6# Fox differential: completed — free pro-\(C\) — coordinates
8The principal declarations in this module are:
10- `freeProCChosenULift_closedGeneratedCoordinateMap`
11 The coordinate map determined by the chosen \(U\)-lifts has the specified closed generated image.
12- `freeProCChosenULift_sepFamilyMap`
13 The separated finite-family map sends lifted chosen-basis coordinates to the separated completed
14 differential module.
15- `freeProCChosenULift_sepFamilyMap_single`
16 The separated family map sends the standard vector at a chosen lifted basis element to its
17 separated universal differential.
18- `freeProCChosenULift_sepCoordinateMap_universal`
19 The separated coordinate map sends the separated universal differential to the closed-generated
20 Fox derivative vector.
21-/
23namespace CrowellExactSequence
25noncomputable section
27open FoxDifferential
28open ProCGroups.ProC
30universe u
32variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33variable {C : ProCGroups.FiniteGroupClass.{u}}
37/--
38The coordinate map determined by the chosen \(U\)-lifts has the specified closed generated
39image.
40-/
41def freeProCChosenULift_closedGeneratedCoordinateMap
42 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
44 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
45 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
46 (psi : ContinuousMonoidHom sourceData.carrier H)
47 (hpsi : Function.Surjective psi) :
48 ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[
49 ZCCompletedGroupAlgebra C H]
50 ZCFreeFoxCoordinates C
51 (X := ULift.{u} (Fin r)) (H := H) := by
52 let family : ULift.{u} (Fin r) → sourceData.carrier :=
53 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
54 let hfree :=
55 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
56 let htarget :=
57 freeProCClosedGeneratedTarget_proC_of_surjective
58 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
59 let hφconv :=
60 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
61 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
63 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
64 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
65 have hφHconv :
67 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
68 simpa [family] using
69 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
70 (C := C) sourceData hbasis psi.toMonoidHom
71 have hφHgen :
73 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
74 simpa [family] using
75 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
76 (C := C) sourceData hbasis psi hpsi
77 exact
78 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
79 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
80 hH hφHconv hφHgen
82/--
83The separated finite-family map sends lifted chosen-basis coordinates to the separated
84completed differential module.
85-/
86def freeProCChosenULift_sepFamilyMap
87 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
88 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
89 (psi : ContinuousMonoidHom sourceData.carrier H) :
90 ZCFreeFoxCoordinates C
91 (X := ULift.{u} (Fin r)) (H := H) →ₗ[
92 ZCCompletedGroupAlgebra C H]
93 ZCSeparatedCompletedDifferentialModule
94 C psi.toMonoidHom :=
95 presentedSeparatedDifferentialFamilyMapProCInteger
96 (G := sourceData.carrier) (H := H) C psi
97 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
99omit [C.ContainsTrivialQuotients] in
100/--
101The separated family map sends the standard vector at a chosen lifted basis element to its separated
102universal differential.
103-/
104@[simp 900]
105theorem freeProCChosenULift_sepFamilyMap_single
106 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
107 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
108 (psi : ContinuousMonoidHom sourceData.carrier H)
109 (i : ULift.{u} (Fin r)) :
110 freeProCChosenULift_sepFamilyMap
111 (H := H) (C := C) sourceData hbasis psi
112 (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
113 zcSeparatedUniversalDifferential
114 C psi.toMonoidHom
115 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i) := by
116 exact
117 presentedSeparatedDifferentialFamilyMapProCInteger_single
118 (G := sourceData.carrier) (H := H) C psi
119 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i
121/-- The separated closed-generated coordinate map for the chosen finite free pro-\(C\) basis. -/
122def freeProCChosenULift_sepCoordinateMap
123 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
125 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
126 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
127 (psi : ContinuousMonoidHom sourceData.carrier H)
128 (hpsi : Function.Surjective psi)
129 [T1Space
130 (ZCFreeFoxCoordinates C
131 (X := ULift.{u} (Fin r)) (H := H))] :
132 ZCSeparatedCompletedDifferentialModule
133 C psi.toMonoidHom →ₗ[
134 ZCCompletedGroupAlgebra C H]
135 ZCFreeFoxCoordinates C
136 (X := ULift.{u} (Fin r)) (H := H) := by
137 letI :
138 Nonempty
139 (ZCCompletedDifferentialModuleIndex
140 C psi.toMonoidHom) :=
141 ⟨zcCompletedDifferentialModuleComapIndex
142 (C := C) (G := sourceData.carrier) (H := H)
143 hC.hereditary psi
145 (C := C) inferInstance),
146 zcCompletedGroupAlgebraTopIndex C H)⟩
147 have hdir :
148 Directed (· ≤ ·)
149 (id :
150 ZCCompletedDifferentialModuleIndex
151 C psi.toMonoidHom →
152 ZCCompletedDifferentialModuleIndex
153 C psi.toMonoidHom) :=
154 directed_zcCompletedDifferentialModuleIndex
155 (C := C) (G := sourceData.carrier) (H := H)
156 (hC.melnikovFormation.formation)
157 hC.hereditary psi
158 let family : ULift.{u} (Fin r) → sourceData.carrier :=
159 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
160 let hfree :=
161 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
162 let htarget :=
163 freeProCClosedGeneratedTarget_proC_of_surjective
164 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
165 let hφconv :=
166 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
167 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
169 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
170 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
171 have hφHconv :
173 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
174 simpa [family] using
175 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
176 (C := C) sourceData hbasis psi.toMonoidHom
177 have hφHgen :
179 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
180 simpa [family] using
181 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
182 (C := C) sourceData hbasis psi hpsi
183 exact
184 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
185 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
186 hdir sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass hH hφHconv hφHgen
188/--
189The separated coordinate map sends the separated universal differential to the closed-generated
190Fox derivative vector.
191-/
192@[simp 900]
193theorem freeProCChosenULift_sepCoordinateMap_universal
194 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
196 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
197 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
198 (psi : ContinuousMonoidHom sourceData.carrier H)
199 (hpsi : Function.Surjective psi)
200 [T1Space
201 (ZCFreeFoxCoordinates C
202 (X := ULift.{u} (Fin r)) (H := H))]
203 (g : sourceData.carrier) :
204 freeProCChosenULift_sepCoordinateMap
205 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
206 (zcSeparatedUniversalDifferential
207 C psi.toMonoidHom g) =
208 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
209 (C := C)
210 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
211 (fun i : ULift.{u} (Fin r) =>
212 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i))
213 (freeProCClosedGeneratedTarget_proC_of_surjective
214 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)
215 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
216 (C := C)
217 (fun i : ULift.{u} (Fin r) =>
218 psi (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis i)))
219 g := by
220 letI :
221 Nonempty
222 (ZCCompletedDifferentialModuleIndex
223 C psi.toMonoidHom) :=
224 ⟨zcCompletedDifferentialModuleComapIndex
225 (C := C) (G := sourceData.carrier) (H := H)
226 hC.hereditary psi
228 (C := C) inferInstance),
229 zcCompletedGroupAlgebraTopIndex C H)⟩
230 have hdir :
231 Directed (· ≤ ·)
232 (id :
233 ZCCompletedDifferentialModuleIndex
234 C psi.toMonoidHom →
235 ZCCompletedDifferentialModuleIndex
236 C psi.toMonoidHom) :=
237 directed_zcCompletedDifferentialModuleIndex
238 (C := C) (G := sourceData.carrier) (H := H)
239 (hC.melnikovFormation.formation)
240 hC.hereditary psi
241 let family : ULift.{u} (Fin r) → sourceData.carrier :=
242 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
243 let hfree :=
244 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
245 let htarget :=
246 freeProCClosedGeneratedTarget_proC_of_surjective
247 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
248 let hφconv :=
249 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
250 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
252 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
253 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
254 have hφHconv :
256 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
257 simpa [family] using
258 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
259 (C := C) sourceData hbasis psi.toMonoidHom
260 have hφHgen :
262 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
263 simpa [family] using
264 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
265 (C := C) sourceData hbasis psi hpsi
266 simpa [freeProCChosenULift_sepCoordinateMap, family, hfree, htarget, hφconv] using
267 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
268 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
269 hdir sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass hH hφHconv hφHgen g
271/-- The separated coordinate equivalence for the chosen finite free pro-\(C\) basis. -/
272def freeProCChosenULift_sepCoordinateEquiv
273 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
275 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
276 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
277 (psi : ContinuousMonoidHom sourceData.carrier H)
278 (hpsi : Function.Surjective psi)
279 [T1Space
280 (ZCFreeFoxCoordinates C
281 (X := ULift.{u} (Fin r)) (H := H))] :
282 ZCSeparatedCompletedDifferentialModule
283 C psi.toMonoidHom ≃ₗ[
284 ZCCompletedGroupAlgebra C H]
285 ZCFreeFoxCoordinates C
286 (X := ULift.{u} (Fin r)) (H := H) := by
287 letI :
288 Nonempty
289 (ZCCompletedDifferentialModuleIndex
290 C psi.toMonoidHom) :=
291 ⟨zcCompletedDifferentialModuleComapIndex
292 (C := C) (G := sourceData.carrier) (H := H)
293 hC.hereditary psi
295 (C := C) inferInstance),
296 zcCompletedGroupAlgebraTopIndex C H)⟩
297 have hdir :
298 Directed (· ≤ ·)
299 (id :
300 ZCCompletedDifferentialModuleIndex
301 C psi.toMonoidHom →
302 ZCCompletedDifferentialModuleIndex
303 C psi.toMonoidHom) :=
304 directed_zcCompletedDifferentialModuleIndex
305 (C := C) (G := sourceData.carrier) (H := H)
306 (hC.melnikovFormation.formation)
307 hC.hereditary psi
308 let family : ULift.{u} (Fin r) → sourceData.carrier :=
309 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
310 let hfree :=
311 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
312 let htarget :=
313 freeProCClosedGeneratedTarget_proC_of_surjective
314 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
315 let hφconv :=
316 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
317 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
319 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
320 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
321 have hφHconv :
323 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
324 simpa [family] using
325 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
326 (C := C) sourceData hbasis psi.toMonoidHom
327 have hφHgen :
329 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
330 simpa [family] using
331 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
332 (C := C) sourceData hbasis psi hpsi
333 exact
334 separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
335 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
336 hdir sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass hH hφHconv hφHgen
338end
340end CrowellExactSequence