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

Source: ProCGroups.FoxDifferential.Completed.FreeProC.NaturalTopology

1import ProCGroups.FreeProC.FiniteBasis
2import ProCGroups.FoxDifferential.Completed.Continuous.Magnus.ClosedGeneratedVector
3import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Topology
4import ProCGroups.FoxDifferential.Completed.FreeProC.RelationReflection
6/-!
7# Fox differential: completed — free pro-\(C\) — natural topology
9The principal declarations in this module are:
11- `freeProCClosedGeneratedTarget_proC_of_surjective`
12 For a surjective map from a free pro-\(C\) group, the closed-generated target is again pro-\(C\).
13- `freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations`
14 Free pro-\(C\) finite-stage separation of \(A_{\psi}(C)\), reduced to the relation-reflection form
15 of the finite source, target, and coefficient reductions. The remaining mathematical content is
16 precisely the reflection hypothesis.
17- `freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations`
18 Free pro-\(C\) Hausdorffness of the finite-stage completed topology on \(A_{\psi}(C)\), reduced to
19 the relation-reflection form of finite-stage separation.
20- `freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed`
21 Closedness of the completed relation submodule implies that finite-stage projections separate
22 points of the completed differential module.
23-/
25namespace CrowellExactSequence
27noncomputable section
29open FoxDifferential
30open ProCGroups.ProC
32universe u
34variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35variable {C : ProCGroups.FiniteGroupClass.{u}}
40/--
41For a surjective map from a free pro-\(C\) group, the closed-generated target is again
42pro-\(C\).
43-/
44theorem freeProCClosedGeneratedTarget_proC_of_surjective
45 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
47 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
48 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
49 (psi : ContinuousMonoidHom sourceData.carrier H)
50 (hpsi : Function.Surjective psi) :
51 HasOpenNormalBasisInClass C
52 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
53 (C := C)
54 (fun i : ULift.{u} (Fin r) =>
55 psi (freeProCChosenULiftFamilyOfBasisCard
56 (C := C) sourceData hbasis i)) : Subgroup
57 (ZCCompletedFoxSemidirect C (ULift.{u} (Fin r)) H)) := by
58 let family : ULift.{u} (Fin r) → sourceData.carrier :=
59 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
60 have hH : HasOpenNormalBasisInClass C H :=
61 HasOpenNormalBasisInClass.of_surjective
62 hC.melnikovFormation.formation
63 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
64 have hAmbient :
65 HasOpenNormalBasisInClass C
66 (ZCCompletedFoxSemidirect C (ULift.{u} (Fin r)) H) :=
68 (C := C) (X := ULift.{u} (Fin r)) (H := H)
69 hC.melnikovFormation hH
70 simpa [family] using
72 (C := C) hC.melnikovFormation.formation
73 hC.hereditary hAmbient
74 (fun i : ULift.{u} (Fin r) => psi (family i))
76omit [C.ContainsTrivialQuotients] in
77/--
78Free pro-\(C\) finite-stage separation of \(A_{\psi}(C)\), reduced to the relation-reflection
79form of the finite source, target, and coefficient reductions. The remaining mathematical
80content is precisely the reflection hypothesis.
81-/
82theorem freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
83 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
84 (psi : ContinuousMonoidHom sourceData.carrier H)
85 (hreflect :
86 zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations
87 C psi.toMonoidHom) :
88 zcCompletedDifferentialModuleStageProjectionsSeparate
89 C psi.toMonoidHom :=
90 zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate
91 C psi.toMonoidHom
92 ((zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations
93 (C := C) (ψ := psi.toMonoidHom)).2 hreflect)
95omit [C.ContainsTrivialQuotients] in
96/--
97Free pro-\(C\) Hausdorffness of the finite-stage completed topology on \(A_{\psi}(C)\), reduced
98to the relation-reflection form of finite-stage separation.
99-/
100theorem freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations
101 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
102 (psi : ContinuousMonoidHom sourceData.carrier H)
103 (hreflect :
104 zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations
105 C psi.toMonoidHom) :
106 @T2Space
107 (ZCCompletedDifferentialModule C psi.toMonoidHom)
108 (zcCompletedDifferentialModuleNaturalTopology
109 C psi.toMonoidHom) :=
110 t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
111 C psi.toMonoidHom
112 (freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
113 (H := H) (C := C) sourceData psi hreflect)
115/--
116Closedness of the completed relation submodule implies that finite-stage projections separate
117points of the completed differential module.
118-/
119theorem freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
121 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
122 (psi : ContinuousMonoidHom sourceData.carrier H)
123 (hclosed :
124 zcCompletedDifferentialModuleRelationSubmoduleClosed
125 C psi.toMonoidHom) :
126 zcCompletedDifferentialModuleStageProjectionsSeparate
127 C psi.toMonoidHom := by
128 letI :
129 Nonempty
130 (ZCCompletedDifferentialModuleIndex
131 C psi.toMonoidHom) :=
132 ⟨zcCompletedDifferentialModuleComapIndex
133 (C := C) (G := sourceData.carrier) (H := H)
134 hC.hereditary psi
136 (C := C) inferInstance),
137 zcCompletedGroupAlgebraTopIndex C H)⟩
138 have hdir :
139 Directed (· ≤ ·)
140 (id :
141 ZCCompletedDifferentialModuleIndex
142 C psi.toMonoidHom →
143 ZCCompletedDifferentialModuleIndex
144 C psi.toMonoidHom) :=
145 directed_zcCompletedDifferentialModuleIndex
146 (C := C) (G := sourceData.carrier) (H := H)
147 (hC.melnikovFormation.formation)
148 hC.hereditary psi
149 exact
150 freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
151 (H := H) (C := C) sourceData psi
152 (zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed
153 C psi.toMonoidHom hdir hclosed)
155/--
156Closedness of the completed relation submodule makes the natural topology on the completed
157differential module Hausdorff.
158-/
159theorem freeProC_t2Space_zcDiffModuleNaturalTopology_of_relSubmoduleClosed
161 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
162 (psi : ContinuousMonoidHom sourceData.carrier H)
163 (hclosed :
164 zcCompletedDifferentialModuleRelationSubmoduleClosed
165 C psi.toMonoidHom) :
166 @T2Space
167 (ZCCompletedDifferentialModule C psi.toMonoidHom)
168 (zcCompletedDifferentialModuleNaturalTopology
169 C psi.toMonoidHom) :=
170 t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
171 C psi.toMonoidHom
172 (freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
173 (H := H) (C := C) (hC := hC) sourceData psi hclosed)
175/--
176Closedness of the completed relation submodule is equivalent to separation by all finite-stage
177projections.
178-/
179theorem freeProC_zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
181 {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
182 {psi : ContinuousMonoidHom sourceData.carrier H} :
183 zcCompletedDifferentialModuleRelationSubmoduleClosed
184 C psi.toMonoidHom ↔
185 zcCompletedDifferentialModuleStageProjectionsSeparate
186 C psi.toMonoidHom := by
187 letI :
188 Nonempty
189 (ZCCompletedDifferentialModuleIndex
190 C psi.toMonoidHom) :=
191 ⟨zcCompletedDifferentialModuleComapIndex
192 (C := C) (G := sourceData.carrier) (H := H)
193 hC.hereditary psi
195 (C := C) inferInstance),
196 zcCompletedGroupAlgebraTopIndex C H)⟩
197 have hdir :
198 Directed (· ≤ ·)
199 (id :
200 ZCCompletedDifferentialModuleIndex
201 C psi.toMonoidHom →
202 ZCCompletedDifferentialModuleIndex
203 C psi.toMonoidHom) :=
204 directed_zcCompletedDifferentialModuleIndex
205 (C := C) (G := sourceData.carrier) (H := H)
206 (hC.melnikovFormation.formation)
207 hC.hereditary psi
208 exact
209 zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
210 (C := C) (ψ := psi.toMonoidHom) hdir
212/--
213Closedness of the completed relation submodule is equivalent to the natural topology being
214Hausdorff.
215-/
216theorem freeProC_zcDiffModuleRelSubmoduleClosed_iff_t2_naturalTopology
218 {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
219 {psi : ContinuousMonoidHom sourceData.carrier H} :
220 zcCompletedDifferentialModuleRelationSubmoduleClosed
221 C psi.toMonoidHom ↔
222 @T2Space
223 (ZCCompletedDifferentialModule C psi.toMonoidHom)
224 (zcCompletedDifferentialModuleNaturalTopology
225 C psi.toMonoidHom) := by
226 letI :
227 Nonempty
228 (ZCCompletedDifferentialModuleIndex
229 C psi.toMonoidHom) :=
230 ⟨zcCompletedDifferentialModuleComapIndex
231 (C := C) (G := sourceData.carrier) (H := H)
232 hC.hereditary psi
234 (C := C) inferInstance),
235 zcCompletedGroupAlgebraTopIndex C H)⟩
236 have hdir :
237 Directed (· ≤ ·)
238 (id :
239 ZCCompletedDifferentialModuleIndex
240 C psi.toMonoidHom →
241 ZCCompletedDifferentialModuleIndex
242 C psi.toMonoidHom) :=
243 directed_zcCompletedDifferentialModuleIndex
244 (C := C) (G := sourceData.carrier) (H := H)
245 (hC.melnikovFormation.formation)
246 hC.hereditary psi
247 exact
248 zcCompletedDifferentialModuleRelationSubmoduleClosed_iff_t2_naturalTopology
249 (C := C) (ψ := psi.toMonoidHom) hdir
251omit [C.ContainsTrivialQuotients] in
252/--
253For a finite free pro-\(C\) basis and a surjective presentation, the completed differential-module
254map is continuous for its natural topology.
255-/
256theorem freeProC_hmodule_continuous_naturalTopology
257 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
259 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
260 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
261 (psi : ContinuousMonoidHom sourceData.carrier H)
262 (hpsi : Function.Surjective psi) :
263 @Continuous sourceData.carrier
264 (ZCCompletedDifferentialModule C psi.toMonoidHom)
265 inferInstance
266 (zcCompletedDifferentialModuleNaturalTopology
267 C psi.toMonoidHom)
268 (fun g : sourceData.carrier =>
269 presentedCompletedDifferentialFamilyMapProCInteger
270 (G := sourceData.carrier) (H := H) C psi
271 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)
272 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
273 (C := C)
274 (freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis)
275 (fun i : ULift.{u} (Fin r) =>
276 psi (freeProCChosenULiftFamilyOfBasisCard
277 (C := C) sourceData hbasis i))
278 (freeProCClosedGeneratedTarget_proC_of_surjective
279 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi)
280 (freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
281 (C := C)
282 (fun i : ULift.{u} (Fin r) =>
283 psi (freeProCChosenULiftFamilyOfBasisCard
284 (C := C) sourceData hbasis i)))
285 g)) := by
286 let family : ULift.{u} (Fin r) → sourceData.carrier :=
287 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
288 let hfree :=
289 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
290 let htarget :=
291 freeProCClosedGeneratedTarget_proC_of_surjective
292 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
293 let hφconv :=
294 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
295 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
296 simpa [family, hfree, htarget, hφconv] using
297 continuous_closedGenerated_module_expansion_naturalTopology
298 (G := sourceData.carrier) (H := H) C psi family hfree htarget hφconv
300end
302end CrowellExactSequence