Yamaguchi Lean 4 Library
Source: ProCGroups.FreeProC.SolvableQuotients
ProCGroups/FreeProC/SolvableQuotients/Source

Source: ProCGroups.FreeProC.SolvableQuotients

1import ProCGroups.FreeProC.Basic
2import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
4/-!
5# Pro C Groups / Free pro-C / Solvable Quotients
7This module transports free pro-\(C\) data to finite-step solvable quotients
8and their derived-series constructions.
9-/
11open scoped Topology
13namespace ProCGroups.FreeProC
15open ProCGroups.FiniteStepSolvableQuotients
17universe u v w
19variable {C : ProCGroups.FiniteGroupClass.{u}}
22variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
23variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
25/-- The endomorphism induced by collapseToFinset on a maximal solvable quotient. -/
26noncomputable def collapseToFinsetQuot
27 {ι : Type v} [DecidableEq ι] (X : ι → F)
28 (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
29 (C := C) ι F X)
30 (S : Finset ι) (m : ℕ) :
31 MaxSolvQuot F m →ₜ* MaxSolvQuot F m :=
35/--
36On the quotient, composing with \(\mathrm{collapseToFinsetQuot}\) leaves a map that is trivial
37outside \(S\) unchanged.
38-/
39theorem comp_collapseToFinsetQuot_eq_of_eq_one_outside
40 {ι : Type v} [DecidableEq ι] (X : ι → F)
41 (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
42 (C := C) ι F X)
43 {H : Type w} [TopologicalSpace H] [Group H] [T2Space H]
44 (S : Finset ι) (m : ℕ) (φ : MaxSolvQuot F m →ₜ* H)
45 (hφ : ∀ j, j ∉ S → φ (continuousToMaxSolvQuot F m (X j)) = 1) :
46 φ.comp (collapseToFinsetQuot X hFree S m) = φ := by
47 let ψ : F →ₜ* H := φ.comp (continuousToMaxSolvQuot F m)
48 have hψ :
49 ψ.comp (hFree.collapseToFinset S) = ψ := by
50 exact
51 hFree.comp_collapseToFinset_eq_of_eq_one_outside ψ S (by
52 intro j hj
53 exact hφ j hj)
54 ext q
55 obtain ⟨x, rfl⟩ := continuousToMaxSolvQuot_surjective (G := F) m q
56 change ψ (hFree.collapseToFinset S x) = ψ x
57 exact congrArg (fun f : F →ₜ* H => f x) hψ
59/--
60The map from the original maximal solvable quotient to the maximal solvable quotient of the
61finite-support retract.
62-/
63noncomputable def finsetSupportRangeQuot
64 {ι : Type v} [DecidableEq ι] (X : ι → F)
65 (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
66 (C := C) ι F X)
67 (S : Finset ι) (m : ℕ) :
68 MaxSolvQuot F m →ₜ* MaxSolvQuot (hFree.FinsetSupportRetract S) m :=
71/--
72The map from the maximal solvable quotient of the finite-support retract to the original maximal
73solvable quotient.
74-/
75noncomputable def finsetSupportInclusionQuot
76 {ι : Type v} [DecidableEq ι] (X : ι → F)
77 (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
78 (C := C) ι F X)
79 (S : Finset ι) (m : ℕ) :
80 MaxSolvQuot (hFree.FinsetSupportRetract S) m →ₜ* MaxSolvQuot F m :=
81 ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap (hFree.collapseToFinsetInclusion S) m
84/--
85The quotient map induced by the finite-support retraction sends the class of `x` to the class of
86its collapsed finite-support image.
87-/
88theorem finsetSupportRangeQuot_apply
89 {ι : Type v} [DecidableEq ι] (X : ι → F)
90 (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
91 (C := C) ι F X)
92 (S : Finset ι) (m : ℕ) (x : F) :
93 finsetSupportRangeQuot X hFree S m (continuousToMaxSolvQuot F m x) =
94 continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m
95 (hFree.collapseToFinsetRange S x) := by
96 change
97 QuotientGroup.map
98 (N := topDerivedTop F m)
99 (M := topDerivedTop (hFree.FinsetSupportRetract S) m)
100 (f := (hFree.collapseToFinsetRange S : F →* hFree.FinsetSupportRetract S))
102 (G := F) (Q := hFree.FinsetSupportRetract S) (f := hFree.collapseToFinsetRange S) m)
103 ((QuotientGroup.mk' (topDerivedTop F m)) x) =
104 (QuotientGroup.mk' (topDerivedTop (hFree.FinsetSupportRetract S) m))
105 (hFree.collapseToFinsetRange S x)
106 rw [QuotientGroup.map_mk']
107 rfl
110/--
111The quotient map induced by inclusion of the finite-support retract sends the class of `x` to
112the class of its image in the original free pro-\(C\) group.
113-/
114theorem finsetSupportInclusionQuot_apply
115 {ι : Type v} [DecidableEq ι] (X : ι → F)
116 (hFree : IsEpimorphicallyFreeProCGroupOnConvergingSet
117 (C := C) ι F X)
118 (S : Finset ι) (m : ℕ) (x : hFree.FinsetSupportRetract S) :
119 finsetSupportInclusionQuot X hFree S m
120 (continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m x) =
121 continuousToMaxSolvQuot F m (hFree.collapseToFinsetInclusion S x) := by
122 change
123 QuotientGroup.map
124 (N := topDerivedTop (hFree.FinsetSupportRetract S) m)
125 (M := topDerivedTop F m)
126 (f := (hFree.collapseToFinsetInclusion S : hFree.FinsetSupportRetract S →* F))
128 (G := hFree.FinsetSupportRetract S) (Q := F)
129 (f := hFree.collapseToFinsetInclusion S) m)
130 ((QuotientGroup.mk' (topDerivedTop (hFree.FinsetSupportRetract S) m)) x) =
131 (QuotientGroup.mk' (topDerivedTop F m)) (hFree.collapseToFinsetInclusion S x)
132 rw [QuotientGroup.map_mk']
133 rfl
135end ProCGroups.FreeProC