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

Source: ProCGroups.FoxDifferential.Completed.FreeProC.RelationReflection

1import ProCGroups.FoxDifferential.Completed.FiniteStage.RelationReflection
2import ProCGroups.FoxDifferential.Completed.FreeProC.FiniteQuotientStages
3import ProCGroups.FoxDifferential.Completed.Continuous.Universal.NaturalTopology
4import ProCGroups.FreeProC.FiniteBasis
6/-!
7# Relation reflection for free pro-\(C\) presentations
9This module supplies the finite free-basis family used to reflect completed
10Fox relations through finite quotient stages, and relates stagewise
11vanishing to equality in the completed differential module.
12-/
14namespace CrowellExactSequence
16noncomputable section
18open scoped Topology
19open ProCGroups.InverseSystems
20open ProCGroups.ProC
21open FoxDifferential
23universe u v
25section FreeRelationReflection
27variable {C : ProCGroups.FiniteGroupClass.{u}}
28variable {H : Type u}
29variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30variable [T2Space H]
32/-- The universe-lifted finite free basis supplies the relation-reflection family. -/
33abbrev freeProCReflectionFamily
34 (sourceData :
35 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
36 {r : Nat}
37 (hbasis : Cardinal.mk sourceData.basis = r) : ULift.{u} (Fin r) → sourceData.carrier :=
38 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
40omit [T2Space H] in
41/-- The target images of the chosen basis topologically generate a surjective target. -/
42theorem freeProCReflectionFamily_target_generates
43 (sourceData :
44 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
45 {r : Nat}
46 (hbasis : Cardinal.mk sourceData.basis = r)
47 (psi : ContinuousMonoidHom sourceData.carrier H)
48 (hpsi : Function.Surjective psi) :
50 (G := H)
51 (Set.range (fun i : ULift.{u} (Fin r) =>
52 psi (freeProCReflectionFamily (C := C) sourceData hbasis i))) := by
53 simpa [freeProCReflectionFamily] using
54 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
55 (C := C) sourceData hbasis psi hpsi
57/-- The free-group map onto the source quotient used by a differential-module finite stage. -/
58def freeProCRelationReflectionStageSourceHom
59 (sourceData :
60 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
61 {r : Nat}
62 (hbasis : Cardinal.mk sourceData.basis = r)
63 (psi : ContinuousMonoidHom sourceData.carrier H)
64 (i : ZCCompletedDifferentialModuleIndex
65 C psi.toMonoidHom) :
66 FreeGroup (ULift.{u} (Fin r)) →*
67 zcCompletedDifferentialModuleStageSource
68 C psi.toMonoidHom i :=
69 (zcCompletedDifferentialModuleStageSourceProj
70 C psi.toMonoidHom i).comp
71 (FreeGroup.lift (freeProCReflectionFamily (C := C) sourceData hbasis))
73/--
74The source kernel used by a differential-module stage, pulled back to the abstract free group
75on the chosen basis.
76-/
77def freeProCRelationReflectionStageKernel
78 (sourceData :
79 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
80 {r : Nat}
81 (hbasis : Cardinal.mk sourceData.basis = r)
82 (psi : ContinuousMonoidHom sourceData.carrier H)
83 (i : ZCCompletedDifferentialModuleIndex
84 C psi.toMonoidHom) :
85 Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
86 MonoidHom.ker
87 (freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i)
89/--
90The relation-reflection stage kernel is a normal subgroup of the free group on the lifted
91finite basis.
92-/
93instance freeProCRelationReflectionStageKernel_normal
94 (sourceData :
95 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
96 {r : Nat}
97 (hbasis : Cardinal.mk sourceData.basis = r)
98 (psi : ContinuousMonoidHom sourceData.carrier H)
99 (i : ZCCompletedDifferentialModuleIndex
100 C psi.toMonoidHom) :
101 (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i).Normal := by
102 dsimp [freeProCRelationReflectionStageKernel]
103 infer_instance
105omit [IsTopologicalGroup H] [T2Space H] in
106/-- The chosen free basis surjects onto every finite source quotient stage. -/
107theorem freeProCRelationReflectionStageSourceHom_surjective
108 (sourceData :
109 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
110 {r : Nat}
111 (hbasis : Cardinal.mk sourceData.basis = r)
112 (psi : ContinuousMonoidHom sourceData.carrier H)
113 (i : ZCCompletedDifferentialModuleIndex
114 C psi.toMonoidHom) :
115 Function.Surjective
116 (freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i) := by
117 classical
118 let X : Type u := ULift.{u} (Fin r)
119 let ι : X → sourceData.carrier := freeProCReflectionFamily (C := C) sourceData hbasis
120 let Q : Type u :=
121 zcCompletedDifferentialModuleStageSource
122 C psi.toMonoidHom i
123 letI : DiscreteTopology Q :=
124 QuotientGroup.discreteTopology i.source.1.toOpenSubgroup.isOpen'
125 let g : X → Q := fun x =>
126 zcCompletedDifferentialModuleStageSourceProj
127 C psi.toMonoidHom i (ι x)
128 have hsource :
130 (G := sourceData.carrier) (Set.range ι) := by
131 simpa [ι, freeProCReflectionFamily] using
132 freeProCChosenULiftFamilyOfBasisCard_generates (C := C) sourceData hbasis
133 have hquot_image :
135 (G := Q)
136 ((QuotientGroup.mk' (i.source.1 : Subgroup sourceData.carrier)) '' Set.range ι) := by
137 simpa [Q] using
139 (G := sourceData.carrier) (N := (i.source.1 : Subgroup sourceData.carrier)) hsource
140 have hrange :
141 ((QuotientGroup.mk' (i.source.1 : Subgroup sourceData.carrier)) '' Set.range ι) =
142 Set.range g := by
143 ext y
144 constructor
145 · rintro ⟨x, ⟨a, rfl⟩, rfl⟩
146 exact ⟨a, rfl⟩
147 · rintro ⟨a, rfl⟩
148 exact ⟨ι a, ⟨a, rfl⟩, rfl⟩
149 have hg :
151 rw [← hrange]
152 exact hquot_image
153 have hsurj : Function.Surjective (FreeGroup.lift g) :=
155 (G := Q) g hg
156 have hlift :
157 FreeGroup.lift g =
158 freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i := by
159 apply FreeGroup.ext_hom
160 intro x
161 rw [FreeGroup.lift_apply_of]
162 change
163 zcCompletedDifferentialModuleStageSourceProj
164 C psi.toMonoidHom i (ι x) =
165 zcCompletedDifferentialModuleStageSourceProj
166 C psi.toMonoidHom i
167 ((FreeGroup.lift (freeProCReflectionFamily (C := C) sourceData hbasis))
168 (FreeGroup.of x))
169 rw [FreeGroup.lift_apply_of]
170 simpa [hlift] using hsurj
172/-- Identification of the source quotient stage with the corresponding free-group quotient. -/
173def freeProCRelationReflectionStageSourceEquiv
174 (sourceData :
175 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
176 {r : Nat}
177 (hbasis : Cardinal.mk sourceData.basis = r)
178 (psi : ContinuousMonoidHom sourceData.carrier H)
179 (i : ZCCompletedDifferentialModuleIndex
180 C psi.toMonoidHom) :
181 foxAlgebraicStageTargetQuotient
182 (X := ULift.{u} (Fin r))
183 (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i) ≃*
184 zcCompletedDifferentialModuleStageSource
185 C psi.toMonoidHom i :=
186 QuotientGroup.quotientKerEquivOfSurjective
187 (freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i)
188 (freeProCRelationReflectionStageSourceHom_surjective
189 (C := C) sourceData hbasis psi i)
191omit [IsTopologicalGroup H] [T2Space H] in
192/--
193The relation-reflection source-stage equivalence sends the quotient class of a free word to its
194image under the corresponding source-stage homomorphism.
195-/
196@[simp]
197theorem freeProCRelationReflectionStageSourceEquiv_mk
198 (sourceData :
199 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
200 {r : Nat}
201 (hbasis : Cardinal.mk sourceData.basis = r)
202 (psi : ContinuousMonoidHom sourceData.carrier H)
203 (i : ZCCompletedDifferentialModuleIndex
204 C psi.toMonoidHom)
205 (w : FreeGroup (ULift.{u} (Fin r))) :
206 freeProCRelationReflectionStageSourceEquiv (C := C) sourceData hbasis psi i
207 (QuotientGroup.mk'
208 (freeProCRelationReflectionStageKernel (C := C) sourceData hbasis psi i) w) =
209 freeProCRelationReflectionStageSourceHom (C := C) sourceData hbasis psi i w :=
210 rfl
212/--
213The target finite Fox relation kernel attached to the target quotient of a
214\(\mathbb{Z}_C\)-completed differential-module index.
215-/
216abbrev freeProCRelationReflectionTargetStageKernel
217 (sourceData :
218 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
219 {r : Nat}
220 (hbasis : Cardinal.mk sourceData.basis = r)
221 (psi : ContinuousMonoidHom sourceData.carrier H)
222 (i : ZCCompletedDifferentialModuleIndex
223 C psi.toMonoidHom) :
224 Subgroup (FreeGroup (ULift.{u} (Fin r))) :=
225 freeProCFiniteQuotientStageKernel
226 (C := C)
227 (fun x : ULift.{u} (Fin r) =>
228 psi (freeProCReflectionFamily (C := C) sourceData hbasis x))
229 i.target.2
231/-- The target finite Fox relation kernel is normal. -/
232instance freeProCRelationReflectionTargetStageKernel_normal
233 (sourceData :
234 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
235 {r : Nat}
236 (hbasis : Cardinal.mk sourceData.basis = r)
237 (psi : ContinuousMonoidHom sourceData.carrier H)
238 (i : ZCCompletedDifferentialModuleIndex
239 C psi.toMonoidHom) :
240 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i).Normal :=
241 inferInstance
243omit [T2Space H] in
244/-- Target finite Fox kernels are antitone along differential-module stage refinement. -/
245theorem freeProCRelationReflectionTargetStageKernel_antitone
246 (sourceData :
247 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
248 {r : Nat}
249 (hbasis : Cardinal.mk sourceData.basis = r)
250 (psi : ContinuousMonoidHom sourceData.carrier H)
251 {i j : ZCCompletedDifferentialModuleIndex
252 C psi.toMonoidHom} (hij : i ≤ j) :
253 freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi j ≤
254 freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i := by
255 exact freeProCFiniteQuotientStageKernel_antitone
256 (C := C)
257 (fun x : ULift.{u} (Fin r) =>
258 psi (freeProCReflectionFamily (C := C) sourceData hbasis x))
259 hij.2.2
261/-- The canonical target quotient comparison map \(H/U_i \to F_X/N_i\). -/
262def freeProCRelationReflectionTargetStageQMap
263 (sourceData :
264 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
265 {r : Nat}
266 (hbasis : Cardinal.mk sourceData.basis = r)
267 (psi : ContinuousMonoidHom sourceData.carrier H)
268 (hpsi : Function.Surjective psi)
269 (i : ZCCompletedDifferentialModuleIndex
270 C psi.toMonoidHom) :
271 CompletedGroupAlgebraQuotientInClass H C i.target.2 →*
272 foxAlgebraicStageTargetQuotient
273 (X := ULift.{u} (Fin r))
274 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i) := by
275 let φ : ULift.{u} (Fin r) → H := fun x =>
276 psi (freeProCReflectionFamily (C := C) sourceData hbasis x)
277 have hφgen :
279 simpa [φ] using
280 freeProCReflectionFamily_target_generates (C := C) sourceData hbasis psi hpsi
281 letI : DiscreteTopology
282 (CompletedGroupAlgebraQuotientInClass H C i.target.2) :=
283 QuotientGroup.discreteTopology
285 ((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H))
286 exact freeProCFiniteQuotientStageQMap
287 (C := C) φ i.target.2
288 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
289 (C := C) φ i.target.2 hφgen)
291omit [T2Space H] in
292/--
293The generator formula for the free pro-\(C\) relation-reflection target finite-stage quotient
294map identifies the specified Crowell boundary or coordinate map.
295-/
296@[simp 900]
297theorem freeProCRelationReflectionTargetStageQMap_generator
298 (sourceData :
299 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
300 {r : Nat}
301 (hbasis : Cardinal.mk sourceData.basis = r)
302 (psi : ContinuousMonoidHom sourceData.carrier H)
303 (hpsi : Function.Surjective psi)
304 (i : ZCCompletedDifferentialModuleIndex
305 C psi.toMonoidHom)
306 (x : ULift.{u} (Fin r)) :
307 freeProCRelationReflectionTargetStageQMap (C := C) sourceData hbasis psi hpsi i
308 (QuotientGroup.mk
309 (psi (freeProCReflectionFamily (C := C) sourceData hbasis x))) =
310 QuotientGroup.mk'
311 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
312 (FreeGroup.of x) := by
313 let φ : ULift.{u} (Fin r) → H := fun x =>
314 psi (freeProCReflectionFamily (C := C) sourceData hbasis x)
315 change
316 freeProCRelationReflectionTargetStageQMap
317 (C := C) sourceData hbasis psi hpsi i (QuotientGroup.mk (φ x)) =
318 QuotientGroup.mk'
319 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
320 (FreeGroup.of x)
321 unfold freeProCRelationReflectionTargetStageQMap
322 simp only [freeProCFiniteQuotientStageQMap_generator,
323 freeProCRelationReflectionTargetStageKernel, ContinuousMonoidHom.coe_toMonoidHom,
324 QuotientGroup.mk'_apply, φ]
326omit [T2Space H] in
327/-- Target quotient comparison maps commute with differential-module stage refinement. -/
328theorem freeProCRelationReflectionTargetStageQMap_transition
329 (sourceData :
330 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
331 {r : Nat}
332 (hbasis : Cardinal.mk sourceData.basis = r)
333 (psi : ContinuousMonoidHom sourceData.carrier H)
334 (hpsi : Function.Surjective psi)
335 {i j : ZCCompletedDifferentialModuleIndex
336 C psi.toMonoidHom} (hij : i ≤ j)
337 (q : CompletedGroupAlgebraQuotientInClass H C j.target.2) :
338 freeProCRelationReflectionTargetStageQMap (C := C) sourceData hbasis psi hpsi i
339 ((OpenNormalSubgroupInClass.map
340 (C := C) (G := H)
341 (U := OrderDual.ofDual i.target.2)
342 (V := OrderDual.ofDual j.target.2) hij.2.2) q) =
343 foxAlgebraicStageTargetQuotientMap
344 (X := ULift.{u} (Fin r))
345 (freeProCRelationReflectionTargetStageKernel_antitone
346 (C := C) sourceData hbasis psi hij)
347 (freeProCRelationReflectionTargetStageQMap
348 (C := C) sourceData hbasis psi hpsi j q) := by
349 let φ : ULift.{u} (Fin r) → H := fun x =>
350 psi (freeProCReflectionFamily (C := C) sourceData hbasis x)
351 have hφgen :
353 simpa [φ] using
354 freeProCReflectionFamily_target_generates (C := C) sourceData hbasis psi hpsi
355 letI : DiscreteTopology
356 (CompletedGroupAlgebraQuotientInClass H C i.target.2) :=
357 QuotientGroup.discreteTopology
359 ((OrderDual.ofDual i.target.2).1 : OpenNormalSubgroup H))
360 letI : DiscreteTopology
361 (CompletedGroupAlgebraQuotientInClass H C j.target.2) :=
362 QuotientGroup.discreteTopology
364 ((OrderDual.ofDual j.target.2).1 : OpenNormalSubgroup H))
365 unfold freeProCRelationReflectionTargetStageQMap
366 exact freeProCFiniteQuotientStageQMap_transition
367 (C := C) φ hij.2.2
368 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
369 (C := C) φ i.target.2 hφgen)
370 (freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
371 (C := C) φ j.target.2 hφgen)
372 q
374/-- The target component map used by finite Fox semidirect stages. -/
375def freeProCRelationReflectionTargetStageRight
376 (sourceData :
377 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
378 {r : Nat}
379 (hbasis : Cardinal.mk sourceData.basis = r)
380 (psi : ContinuousMonoidHom sourceData.carrier H)
381 (hpsi : Function.Surjective psi)
382 (i : ZCCompletedDifferentialModuleIndex
383 C psi.toMonoidHom) :
384 H →* foxAlgebraicStageTargetQuotient
385 (X := ULift.{u} (Fin r))
386 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i) :=
387 (freeProCRelationReflectionTargetStageQMap
388 (C := C) sourceData hbasis psi hpsi i).comp
389 (openNormalSubgroupInClassProj
390 (C := C) (G := H) i.target.2)
392omit [T2Space H] in
393/--
394The target-stage right map sends the chosen generator to its quotient class in the
395relation-reflection target stage.
396-/
397@[simp 900]
398theorem freeProCRelationReflectionTargetStageRight_generator
399 (sourceData :
400 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
401 {r : Nat}
402 (hbasis : Cardinal.mk sourceData.basis = r)
403 (psi : ContinuousMonoidHom sourceData.carrier H)
404 (hpsi : Function.Surjective psi)
405 (i : ZCCompletedDifferentialModuleIndex
406 C psi.toMonoidHom)
407 (x : ULift.{u} (Fin r)) :
408 freeProCRelationReflectionTargetStageRight (C := C) sourceData hbasis psi hpsi i
409 (psi (freeProCReflectionFamily (C := C) sourceData hbasis x)) =
410 QuotientGroup.mk'
411 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
412 (FreeGroup.of x) := by
413 change
414 freeProCRelationReflectionTargetStageQMap
415 (C := C) sourceData hbasis psi hpsi i
416 (QuotientGroup.mk
417 (psi (freeProCReflectionFamily (C := C) sourceData hbasis x))) =
418 QuotientGroup.mk'
419 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
420 (FreeGroup.of x)
421 exact freeProCRelationReflectionTargetStageQMap_generator
422 (C := C) sourceData hbasis psi hpsi i x
424/-- The finite Fox semidirect projection attached to one target quotient stage. -/
425def freeProCRelationReflectionTargetStageMap
426 (sourceData :
427 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
428 {r : Nat}
429 (hbasis : Cardinal.mk sourceData.basis = r)
430 (psi : ContinuousMonoidHom sourceData.carrier H)
431 (hpsi : Function.Surjective psi)
432 (i : ZCCompletedDifferentialModuleIndex
433 C psi.toMonoidHom) :
434 ZCCompletedFoxSemidirect C (ULift.{u} (Fin r)) H →*
435 FoxAlgebraicStageSemidirect
436 (X := ULift.{u} (Fin r))
437 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
438 i.target.1.modulus := by
439 letI : ∀ j : ZCCompletedDifferentialModuleIndex
440 C psi.toMonoidHom,
441 Fact (0 < j.target.1.modulus) :=
443 exact
444 freeProCZCCompletedFoxSemidirectZCBifilteredStageMap
445 (C := C) (X := ULift.{u} (Fin r)) (H := H)
446 (Nstage := fun j =>
447 freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi j)
448 (nstage := fun j => j.target.1.modulus)
449 (zcIndex := fun j => j.target)
450 (hmod := fun _ => dvd_rfl)
451 (qmap := fun j =>
452 freeProCRelationReflectionTargetStageQMap
453 (C := C) sourceData hbasis psi hpsi j)
454 i
456omit [T2Space H] in
457/--
458Each target finite stage attached to the chosen free pro-\(C\) basis satisfies the finite Fox
459relation-boundary module exactness needed by the approximation theorem.
460-/
461theorem freeProCRelationReflection_finiteStage_relationBoundaryModuleExact
462 (sourceData :
463 ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
464 {r : Nat}
465 (hbasis : Cardinal.mk sourceData.basis = r)
466 (psi : ContinuousMonoidHom sourceData.carrier H)
467 (i : ZCCompletedDifferentialModuleIndex
468 C psi.toMonoidHom) :
469 foxAlgebraicStageRelationBoundaryModuleExact
470 (X := ULift.{u} (Fin r))
471 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
472 i.target.1.modulus := by
473 exact
474 foxAlgebraicStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction
475 (X := ULift.{u} (Fin r))
476 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
477 i.target.1.modulus
478 (foxAlgebraicStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives
479 (X := ULift.{u} (Fin r))
480 (freeProCRelationReflectionTargetStageKernel (C := C) sourceData hbasis psi i)
481 i.target.1.modulus)
483end FreeRelationReflection
485end
487end CrowellExactSequence