ProCGroups/FreeProC/SolvableQuotients.lean
1import ProCGroups.FreeProC.Basic
2import ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/FreeProC/SolvableQuotients.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15This file records the maps induced on maximal finite-step solvable quotients by the finite-support
16retractions of a free pro-`C` group.
17-/
19open scoped Topology
21namespace ProCGroups.FreeProC
23open ProCGroups.FiniteStepSolvableQuotients
25universe u v w
27variable {C : ProCGroups.FiniteGroupClass.{u}}
28variable [Fact (ProCGroups.FiniteGroupClass.Variety C)]
29variable [Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
30variable {F : Type u} [TopologicalSpace F] [Group F] [IsTopologicalGroup F]
32/-- The endomorphism induced by `collapseToFinset` on a maximal solvable quotient. -/
33noncomputable def collapseToFinsetQuot
34 {ι : Type v} [DecidableEq ι] (X : ι → F)
35 (hFree : IsFreeProCGroupOnConvergingSet
36 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
37 (S : Finset ι) (m : ℕ) :
38 MaxSolvQuot F m →ₜ* MaxSolvQuot F m :=
39 ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap (hFree.collapseToFinset S) m
41/-- On the quotient, a map that is trivial outside `S` is unchanged after composition with
42`collapseToFinsetQuot`. -/
44 {ι : Type v} [DecidableEq ι] (X : ι → F)
45 (hFree : IsFreeProCGroupOnConvergingSet
46 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
47 {H : Type w} [TopologicalSpace H] [Group H] [IsTopologicalGroup H] [T2Space H]
48 (S : Finset ι) (m : ℕ) (φ : MaxSolvQuot F m →ₜ* H)
49 (hφ : ∀ j, j ∉ S → φ (continuousToMaxSolvQuot F m (X j)) = 1) :
50 φ.comp (collapseToFinsetQuot X hFree S m) = φ := by
51 let ψ : F →ₜ* H := φ.comp (continuousToMaxSolvQuot F m)
52 have hψ :
53 ψ.comp (hFree.collapseToFinset S) = ψ := by
54 exact
55 hFree.comp_collapseToFinset_eq_of_eq_one_outside ψ S (by
56 intro j hj
57 exact hφ j hj)
58 ext q
59 obtain ⟨x, rfl⟩ := continuousToMaxSolvQuot_surjective (G := F) m q
60 change ψ (hFree.collapseToFinset S x) = ψ x
61 exact congrArg (fun f : F →ₜ* H => f x) hψ
63/-- The map from the original maximal solvable quotient to the maximal solvable quotient of the
65noncomputable def finsetSupportRangeQuot
66 {ι : Type v} [DecidableEq ι] (X : ι → F)
67 (hFree : IsFreeProCGroupOnConvergingSet
68 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
69 (S : Finset ι) (m : ℕ) :
70 MaxSolvQuot F m →ₜ* MaxSolvQuot (hFree.FinsetSupportRetract S) m :=
71 ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap (hFree.collapseToFinsetRange S) m
73/-- The map from the maximal solvable quotient of the finite-support retract to the original
75noncomputable def finsetSupportInclusionQuot
76 {ι : Type v} [DecidableEq ι] (X : ι → F)
77 (hFree : IsFreeProCGroupOnConvergingSet
78 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
79 (S : Finset ι) (m : ℕ) :
80 MaxSolvQuot (hFree.FinsetSupportRetract S) m →ₜ* MaxSolvQuot F m :=
81 ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap (hFree.collapseToFinsetInclusion S) m
83theorem finsetSupportRangeQuot_apply
84 {ι : Type v} [DecidableEq ι] (X : ι → F)
85 (hFree : IsFreeProCGroupOnConvergingSet
86 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
87 (S : Finset ι) (m : ℕ) (x : F) :
88 finsetSupportRangeQuot X hFree S m (continuousToMaxSolvQuot F m x) =
89 continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m
90 (hFree.collapseToFinsetRange S x) := by
91 change
92 QuotientGroup.map
93 (N := topDerivedTop F m)
94 (M := topDerivedTop (hFree.FinsetSupportRetract S) m)
95 (f := (hFree.collapseToFinsetRange S : F →* hFree.FinsetSupportRetract S))
97 (G := F) (Q := hFree.FinsetSupportRetract S) (f := hFree.collapseToFinsetRange S) m)
98 ((QuotientGroup.mk' (topDerivedTop F m)) x) =
99 (QuotientGroup.mk' (topDerivedTop (hFree.FinsetSupportRetract S) m))
100 (hFree.collapseToFinsetRange S x)
101 rw [QuotientGroup.map_mk']
102 rfl
105 {ι : Type v} [DecidableEq ι] (X : ι → F)
106 (hFree : IsFreeProCGroupOnConvergingSet
107 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
108 (S : Finset ι) (m : ℕ) (x : hFree.FinsetSupportRetract S) :
109 finsetSupportInclusionQuot X hFree S m
110 (continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m x) =
111 continuousToMaxSolvQuot F m (hFree.collapseToFinsetInclusion S x) := by
112 change
113 QuotientGroup.map
114 (N := topDerivedTop (hFree.FinsetSupportRetract S) m)
115 (M := topDerivedTop F m)
116 (f := (hFree.collapseToFinsetInclusion S : hFree.FinsetSupportRetract S →* F))
118 (G := hFree.FinsetSupportRetract S) (Q := F)
119 (f := hFree.collapseToFinsetInclusion S) m)
120 ((QuotientGroup.mk' (topDerivedTop (hFree.FinsetSupportRetract S) m)) x) =
121 (QuotientGroup.mk' (topDerivedTop F m)) (hFree.collapseToFinsetInclusion S x)
122 rw [QuotientGroup.map_mk']
123 rfl
125end ProCGroups.FreeProC