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

Source: ProCGroups.FoxDifferential.Completed.FreeProC.FundamentalFormula

1import ProCGroups.FoxDifferential.Completed.FreeProC.Coordinates
2import ProCGroups.FoxDifferential.Completed.FiniteStage.ClosedGeneratedCycles
4/-!
5# Fox differential: completed — free pro-\(C\) — fundamental formula
7The principal declarations in this module are:
9- `freeProCChosenULift_closedGenerated_fundamental_formula_stageProj`
10 At each finite stage, the chosen \(U\)-lift closed-generation map satisfies the fundamental
11 formula after projection.
12- `freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate`
13 Separation by finite-stage projections implies the closed-generation fundamental formula for the
14 chosen \(U\)-lifts.
15- `freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed`
16 Closedness of the completed relation submodule implies the closed-generation fundamental formula
17 for the chosen \(U\)-lifts.
18- `freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula`
19 The closed-generation fundamental formula implies closedness of the completed differential-module
20 relation submodule.
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}}
37omit [C.ContainsTrivialQuotients] in
38/--
39At each finite stage, the chosen \(U\)-lift closed-generation map satisfies the fundamental
40formula after projection.
41-/
42theorem freeProCChosenULift_closedGenerated_fundamental_formula_stageProj
43 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
45 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
46 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
47 (psi : ContinuousMonoidHom sourceData.carrier H)
48 (hpsi : Function.Surjective psi)
49 (i : ZCCompletedDifferentialModuleIndex
50 C psi.toMonoidHom)
51 (g : sourceData.carrier) :
52 zcCompletedDifferentialModuleStageProjection
53 C psi.toMonoidHom i
54 (presentedCompletedDifferentialFamilyMapProCInteger
55 (G := sourceData.carrier) (H := H) C psi
56 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
57 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
58 (C := C)
59 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
60 (fun i : ULift.{u} (Fin r) =>
61 psi (freeProCChosenULiftFamilyOfBasisCard
62 (C := C) sourceData hbasis i))
63 (freeProCClosedGeneratedTarget_proC_of_surjective
64 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)
65 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
66 (C := C)
67 (fun i : ULift.{u} (Fin r) =>
68 psi (freeProCChosenULiftFamilyOfBasisCard
69 (C := C) sourceData hbasis i)))
70 g)) =
71 zcCompletedDifferentialModuleStageProjection
72 C psi.toMonoidHom i
73 (zcUniversalDifferential C psi.toMonoidHom g) := by
74 let family : ULift.{u} (Fin r) → sourceData.carrier :=
75 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
76 let hfree :=
77 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
78 let htarget :=
79 freeProCClosedGeneratedTarget_proC_of_surjective
80 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
81 let hφconv :=
82 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
83 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
85 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
86 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
87 have hφHconv :
89 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
90 simpa [family] using
91 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
92 (C := C) sourceData hbasis psi.toMonoidHom
93 have hφHgen :
95 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
96 simpa [family] using
97 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
98 (C := C) sourceData hbasis psi hpsi
99 simpa [family, hfree, htarget, hφconv] using
100 closedGenerated_fundamental_formula_stageProj
101 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
102 hH hφHconv hφHgen i g
104omit [C.ContainsTrivialQuotients] in
105/--
106Separation by finite-stage projections implies the closed-generation fundamental formula for
107the chosen \(U\)-lifts.
108-/
109theorem freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate
110 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
112 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
113 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
114 (psi : ContinuousMonoidHom sourceData.carrier H)
115 (hpsi : Function.Surjective psi)
116 (hsep :
117 zcCompletedDifferentialModuleStageProjectionsSeparate
118 C psi.toMonoidHom) :
119 ∀ g : sourceData.carrier,
120 presentedCompletedDifferentialFamilyMapProCInteger
121 (G := sourceData.carrier) (H := H) C psi
122 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
123 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
124 (C := C)
125 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
126 (fun i : ULift.{u} (Fin r) =>
127 psi (freeProCChosenULiftFamilyOfBasisCard
128 (C := C) sourceData hbasis i))
129 (freeProCClosedGeneratedTarget_proC_of_surjective
130 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)
131 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
132 (C := C)
133 (fun i : ULift.{u} (Fin r) =>
134 psi (freeProCChosenULiftFamilyOfBasisCard
135 (C := C) sourceData hbasis i)))
136 g) =
137 zcUniversalDifferential C psi.toMonoidHom g := by
138 let family : ULift.{u} (Fin r) → sourceData.carrier :=
139 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
140 let hfree :=
141 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
142 let htarget :=
143 freeProCClosedGeneratedTarget_proC_of_surjective
144 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
145 let hφconv :=
146 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
147 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
149 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
150 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
151 have hφHconv :
153 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
154 simpa [family] using
155 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
156 (C := C) sourceData hbasis psi.toMonoidHom
157 have hφHgen :
159 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
160 simpa [family] using
161 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
162 (C := C) sourceData hbasis psi hpsi
163 simpa [family, hfree, htarget, hφconv] using
164 closedGenerated_fundamental_formula_naturalTopology_of_separating
165 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
166 hsep hH hφHconv hφHgen
168/--
169Closedness of the completed relation submodule implies the closed-generation fundamental
170formula for the chosen \(U\)-lifts.
171-/
172theorem freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
173 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
175 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
176 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
177 (psi : ContinuousMonoidHom sourceData.carrier H)
178 (hpsi : Function.Surjective psi)
179 (hclosed :
180 zcCompletedDifferentialModuleRelationSubmoduleClosed
181 C psi.toMonoidHom) :
182 ∀ g : sourceData.carrier,
183 presentedCompletedDifferentialFamilyMapProCInteger
184 (G := sourceData.carrier) (H := H) C psi
185 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
186 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
187 (C := C)
188 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
189 (fun i : ULift.{u} (Fin r) =>
190 psi (freeProCChosenULiftFamilyOfBasisCard
191 (C := C) sourceData hbasis i))
192 (freeProCClosedGeneratedTarget_proC_of_surjective
193 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)
194 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
195 (C := C)
196 (fun i : ULift.{u} (Fin r) =>
197 psi (freeProCChosenULiftFamilyOfBasisCard
198 (C := C) sourceData hbasis i)))
199 g) =
200 zcUniversalDifferential C psi.toMonoidHom g := by
201 exact
202 freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate
203 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
204 (freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
205 (H := H) (C := C) (hC := hC) sourceData psi hclosed)
208/--
209The closed-generation fundamental formula implies closedness of the completed
210differential-module relation submodule.
211-/
212theorem freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula
213 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
215 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
216 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
217 (psi : ContinuousMonoidHom sourceData.carrier H)
218 (hpsi : Function.Surjective psi)
219 (hfundamental :
220 let htarget :=
221 freeProCClosedGeneratedTarget_proC_of_surjective
222 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
223 ∀ g : sourceData.carrier,
224 presentedCompletedDifferentialFamilyMapProCInteger
225 (G := sourceData.carrier) (H := H) C psi
226 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
227 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
228 (C := C)
229 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
230 (fun i : ULift.{u} (Fin r) =>
231 psi (freeProCChosenULiftFamilyOfBasisCard
232 (C := C) sourceData hbasis i))
233 htarget
234 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
235 (C := C)
236 (fun i : ULift.{u} (Fin r) =>
237 psi (freeProCChosenULiftFamilyOfBasisCard
238 (C := C) sourceData hbasis i)))
239 g) =
240 zcUniversalDifferential C psi.toMonoidHom g) :
241 zcCompletedDifferentialModuleRelationSubmoduleClosed
242 C psi.toMonoidHom := by
243 let family : ULift.{u} (Fin r) → sourceData.carrier :=
244 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
245 let hfree :=
246 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
247 let htarget :=
248 freeProCClosedGeneratedTarget_proC_of_surjective
249 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
250 let hφconv :=
251 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
252 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
253 have hH : HasOpenNormalBasisInClass C H :=
254 HasOpenNormalBasisInClass.of_surjective
255 hC.melnikovFormation.formation
256 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
257 have hφHconv :
259 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
260 simpa [family] using
261 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
262 (C := C) sourceData hbasis psi.toMonoidHom
263 have hφHgen :
265 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
266 simpa [family] using
267 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
268 (C := C) sourceData hbasis psi hpsi
269 exact
270 zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_fundFormula
271 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
272 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass hH hφHconv hφHgen
273 (by simpa [family, hfree, htarget, hφconv] using hfundamental)
275-- Coordinate injectivity and the fundamental formula are independent consequences of closedness.
276/-- For the chosen finite free pro-`C` basis, relation-submodule closedness is equivalent to
277injectivity of the closed-generated coordinate map. -/
278theorem freeProC_zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj
279 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
281 {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
282 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
283 {psi : ContinuousMonoidHom sourceData.carrier H}
284 (hpsi : Function.Surjective psi) :
285 zcCompletedDifferentialModuleRelationSubmoduleClosed
286 C psi.toMonoidHom ↔
287 Function.Injective
288 (freeProCChosenULift_closedGeneratedCoordinateMap
289 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi) := by
290 letI :
291 Nonempty
292 (ZCCompletedDifferentialModuleIndex
293 C psi.toMonoidHom) :=
294 ⟨zcCompletedDifferentialModuleComapIndex
295 (C := C) (G := sourceData.carrier) (H := H)
296 hC.hereditary psi
298 (C := C) inferInstance),
299 zcCompletedGroupAlgebraTopIndex C H)⟩
300 have hdir :
301 Directed (· ≤ ·)
302 (id :
303 ZCCompletedDifferentialModuleIndex
304 C psi.toMonoidHom →
305 ZCCompletedDifferentialModuleIndex
306 C psi.toMonoidHom) :=
307 directed_zcCompletedDifferentialModuleIndex
308 (C := C) (G := sourceData.carrier) (H := H)
309 (hC.melnikovFormation.formation)
310 hC.hereditary psi
311 let family : ULift.{u} (Fin r) → sourceData.carrier :=
312 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
313 let hfree :=
314 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
315 let htarget :=
316 freeProCClosedGeneratedTarget_proC_of_surjective
317 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
318 let hφconv :=
319 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
320 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
322 HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation
323 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
324 have hφHconv :
326 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
327 simpa [family] using
328 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
329 (C := C) sourceData hbasis psi.toMonoidHom
330 have hφHgen :
332 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
333 simpa [family] using
334 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
335 (C := C) sourceData hbasis psi hpsi
336 have hiff :=
337 zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj_of_hasOpenNormalBasisInClass
338 (G := sourceData.carrier) (H := H) (C := C) (psi := psi)
339 (family := family) (hfree := hfree) (htarget := htarget) (hφconv := hφconv)
340 hdir sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass hH hφHconv hφHgen
341 simpa [freeProCChosenULift_closedGeneratedCoordinateMap, family, hfree, htarget, hφconv,
342 hH, hφHconv, hφHgen] using hiff
344/--
345Injectivity of the closed-generated coordinate map implies closedness of the completed
346differential-module relation submodule.
347-/
348theorem freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj
349 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
351 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
352 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
353 (psi : ContinuousMonoidHom sourceData.carrier H)
354 (hpsi : Function.Surjective psi)
355 (hcoord_inj :
356 Function.Injective
357 (freeProCChosenULift_closedGeneratedCoordinateMap
358 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)) :
359 zcCompletedDifferentialModuleRelationSubmoduleClosed
360 C psi.toMonoidHom :=
361 (freeProC_zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj
362 (H := H) (C := C) (hC := hC) (sourceData := sourceData) hbasis
363 (psi := psi) hpsi).2 hcoord_inj
365/--
366Injectivity of the closed-generated coordinate map implies the closed-generated fundamental
367formula for the chosen \(U\)-lifts.
368-/
369theorem freeProCChosenULift_closedGen_fundFormula_of_closedGenCoord_inj
370 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
372 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
373 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
374 (psi : ContinuousMonoidHom sourceData.carrier H)
375 (hpsi : Function.Surjective psi)
376 (hcoord_inj :
377 Function.Injective
378 (freeProCChosenULift_closedGeneratedCoordinateMap
379 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)) :
380 let htarget :=
381 freeProCClosedGeneratedTarget_proC_of_surjective
382 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
383 ∀ g : sourceData.carrier,
384 presentedCompletedDifferentialFamilyMapProCInteger
385 (G := sourceData.carrier) (H := H) C psi
386 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
387 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
388 (C := C)
389 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
390 (fun i : ULift.{u} (Fin r) =>
391 psi (freeProCChosenULiftFamilyOfBasisCard
392 (C := C) sourceData hbasis i))
393 htarget
394 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
395 (C := C)
396 (fun i : ULift.{u} (Fin r) =>
397 psi (freeProCChosenULiftFamilyOfBasisCard
398 (C := C) sourceData hbasis i)))
399 g) =
400 zcUniversalDifferential C psi.toMonoidHom g := by
401 exact
402 freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
403 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
404 (freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj
405 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi hcoord_inj)
408/--
409The closed-generation fundamental formula supplies the required chosen-\(U\)-lift basis data
410for \(A\).
411-/
412theorem chosenULift_hbasis_A_of_closedGen_fundFormula
413 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
415 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
416 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
417 (psi : ContinuousMonoidHom sourceData.carrier H)
418 (hpsi : Function.Surjective psi)
419 (htarget :
420 HasOpenNormalBasisInClass C
421 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
422 (C := C)
423 (fun i : ULift.{u} (Fin r) =>
424 psi (freeProCChosenULiftFamilyOfBasisCard
425 (C := C) sourceData hbasis i)) : Subgroup
426 (ZCCompletedFoxSemidirect
427 C (ULift.{u} (Fin r)) H)))
428 (hfundamental :
429 ∀ g : sourceData.carrier,
430 presentedCompletedDifferentialFamilyMapProCInteger
431 (G := sourceData.carrier) (H := H) C psi
432 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
433 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
434 (C := C)
435 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
436 (fun i : ULift.{u} (Fin r) =>
437 psi (freeProCChosenULiftFamilyOfBasisCard
438 (C := C) sourceData hbasis i))
439 htarget
440 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
441 (C := C)
442 (fun i : ULift.{u} (Fin r) =>
443 psi (freeProCChosenULiftFamilyOfBasisCard
444 (C := C) sourceData hbasis i)))
445 g) =
446 zcUniversalDifferential C psi.toMonoidHom g) :
447 IsPresentedCompletedDifferentialFamilyBasisProCInteger
448 (G := sourceData.carrier) (H := H) C psi
449 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) := by
450 let family : ULift.{u} (Fin r) → sourceData.carrier :=
451 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
452 let hfree :=
453 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
454 let hφconv :=
455 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
456 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
457 have hH : HasOpenNormalBasisInClass C H :=
458 HasOpenNormalBasisInClass.of_surjective
459 hForm
460 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
461 have hφHconv :
463 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
464 simpa [family] using
465 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
466 (C := C) sourceData hbasis psi.toMonoidHom
467 have hφHgen :
469 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
470 simpa [family] using
471 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
472 (C := C) sourceData hbasis psi hpsi
473 exact
474 isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
475 (G := sourceData.carrier) (H := H) C psi family hfree
476 (by simpa [family] using htarget) hφconv hH hφHconv hφHgen
477 (by simpa [family, hfree, hφconv] using hfundamental)
479omit [C.ContainsTrivialQuotients] in
480/--
481Continuity of the closed-generated and universal differential formulas promotes the chosen lifted
482finite family to a basis of the presented completed differential module.
483-/
484theorem chosenULift_hbasis_A_of_closedGen_fundFormula_continuous
485 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
487 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
488 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
489 (psi : ContinuousMonoidHom sourceData.carrier H)
490 (hpsi : Function.Surjective psi)
491 [TopologicalSpace (ZCCompletedDifferentialModule
492 C psi.toMonoidHom)]
493 [T2Space (ZCCompletedDifferentialModule
494 C psi.toMonoidHom)]
495 (htarget :
496 HasOpenNormalBasisInClass C
497 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
498 (C := C)
499 (fun i : ULift.{u} (Fin r) =>
500 psi (freeProCChosenULiftFamilyOfBasisCard
501 (C := C) sourceData hbasis i)) : Subgroup
502 (ZCCompletedFoxSemidirect
503 C (ULift.{u} (Fin r)) H)))
504 (hmodule_continuous :
505 Continuous
506 (fun g : sourceData.carrier =>
507 presentedCompletedDifferentialFamilyMapProCInteger
508 (G := sourceData.carrier) (H := H) C psi
509 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
510 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
511 (C := C)
512 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree
513 (C := C) sourceData hbasis)
514 (fun i : ULift.{u} (Fin r) =>
515 psi (freeProCChosenULiftFamilyOfBasisCard
516 (C := C) sourceData hbasis i))
517 htarget
518 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
519 (C := C)
520 (fun i : ULift.{u} (Fin r) =>
521 psi (freeProCChosenULiftFamilyOfBasisCard
522 (C := C) sourceData hbasis i)))
523 g)))
524 (huniv_continuous :
525 Continuous
526 (fun g : sourceData.carrier =>
527 zcUniversalDifferential C psi.toMonoidHom g)) :
528 IsPresentedCompletedDifferentialFamilyBasisProCInteger
529 (G := sourceData.carrier) (H := H) C psi
530 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) := by
531 let family : ULift.{u} (Fin r) → sourceData.carrier :=
532 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
533 let hfree :=
534 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
535 let hφconv :=
536 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
537 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
538 have hH : HasOpenNormalBasisInClass C H :=
539 HasOpenNormalBasisInClass.of_surjective
540 hForm
541 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
542 have hφHconv :
544 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
545 simpa [family] using
546 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
547 (C := C) sourceData hbasis psi.toMonoidHom
548 have hφHgen :
550 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
551 simpa [family] using
552 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
553 (C := C) sourceData hbasis psi hpsi
554 have hfundamental :
555 ∀ g : sourceData.carrier,
556 presentedCompletedDifferentialFamilyMapProCInteger
557 (G := sourceData.carrier) (H := H) C psi family
558 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
559 (C := C) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
560 (by simpa [family] using htarget) hφconv g) =
561 zcUniversalDifferential C psi.toMonoidHom g :=
562 closedGenerated_fundamental_formula_of_continuous
563 (G := sourceData.carrier) (H := H) C psi family hfree
564 (by simpa [family] using htarget) hφconv hH hφHconv hφHgen
565 (by simpa [family, hfree, hφconv] using hmodule_continuous)
566 (by simpa using huniv_continuous)
567 exact
568 chosenULift_hbasis_A_of_closedGen_fundFormula
569 (H := H) (C := C) hForm sourceData hbasis psi hpsi htarget
570 (by simpa [family, hfree, hφconv] using hfundamental)
572/--
573Closedness of the completed relation submodule gives the required basis-indexed
574chosen-\(U\)-lift family in the Crowell module \(A\).
575-/
576theorem freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed
577 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
579 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
580 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
581 (psi : ContinuousMonoidHom sourceData.carrier H)
582 (hpsi : Function.Surjective psi)
583 (hclosed :
584 zcCompletedDifferentialModuleRelationSubmoduleClosed
585 C psi.toMonoidHom) :
586 IsPresentedCompletedDifferentialFamilyBasisProCInteger
587 (G := sourceData.carrier) (H := H) C psi
588 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) := by
589 let htarget :=
590 freeProCClosedGeneratedTarget_proC_of_surjective
591 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
592 have hfundamental :
593 ∀ g : sourceData.carrier,
594 presentedCompletedDifferentialFamilyMapProCInteger
595 (G := sourceData.carrier) (H := H) C psi
596 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
597 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
598 (C := C)
599 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
600 (fun i : ULift.{u} (Fin r) =>
601 psi (freeProCChosenULiftFamilyOfBasisCard
602 (C := C) sourceData hbasis i))
603 htarget
604 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
605 (C := C)
606 (fun i : ULift.{u} (Fin r) =>
607 psi (freeProCChosenULiftFamilyOfBasisCard
608 (C := C) sourceData hbasis i)))
609 g) =
610 zcUniversalDifferential C psi.toMonoidHom g := by
611 simpa [htarget] using
612 freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
613 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi hclosed
614 exact
615 chosenULift_hbasis_A_of_closedGen_fundFormula
616 (H := H) (C := C) hC.melnikovFormation.formation
617 sourceData hbasis psi hpsi htarget hfundamental
619/--
620Injectivity of the closed-generated coordinate map gives the finite \(A_{\psi}(C)\)-basis
621theorem for the chosen lifted basis family.
622-/
623theorem freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_closedGenCoord_inj
624 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
626 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
627 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
628 (psi : ContinuousMonoidHom sourceData.carrier H)
629 (hpsi : Function.Surjective psi)
630 (hcoord_inj :
631 Function.Injective
632 (freeProCChosenULift_closedGeneratedCoordinateMap
633 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)) :
634 IsPresentedCompletedDifferentialFamilyBasisProCInteger
635 (G := sourceData.carrier) (H := H) C psi
636 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) :=
637 freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed
638 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
639 (freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj
640 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi hcoord_inj)
642end
644end CrowellExactSequence