Yamaguchi Lean 4 Library
ProCGroups/ProC/OpenNormalSubgroups/ClosedCommutator.lean
ProCGroups/ProC/OpenNormalSubgroups/ClosedCommutator/Source

ProCGroups/ProC/OpenNormalSubgroups/ClosedCommutator.lean

1import ProCGroups.Abelian.TopologicalAbelianizationLimits
2import ProCGroups.ProC.GroupPredicates.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/ClosedCommutator.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Closed commutators and the canonical open-normal quotient system
16This file records the finite-quotient detection form of the closed commutator subgroup for
17pro-`C` groups, using the canonical inverse-limit presentation by open normal quotients in `C`.
18-/
20namespace ProCGroups.ProC
22open scoped Topology
24universe u
26variable {C : FiniteGroupClass.{u}}
27variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29/-- A quotient-level commutator descent along a surjective homomorphism.
31If `f : N -> K` is onto, `f n` is in the ordinary commutator subgroup of `K`, and the
32kernel of `f` dies in the quotient `N/U`, then the image of `n` in `N/U` is in the ordinary
33commutator subgroup. -/
35 {N K : Type u} [Group N] [Group K]
36 (f : N →* K) (hf : Function.Surjective f)
37 (U : Subgroup N) [U.Normal] (hkerU : f.ker ≤ U)
38 {n : N} (hn : f n ∈ commutator K) :
39 QuotientGroup.mk' U n ∈ commutator (N ⧸ U) := by
40 have hcomm_le :
41 commutator K ≤ (commutator N).map f := by
42 rw [_root_.map_commutator_eq]
43 have hrange : f.range = (⊤ : Subgroup K) := by
44 ext k
45 constructor
46 · intro hk
47 trivial
48 · intro _hk
49 rcases hf k with ⟨n, rfl⟩
50 exact ⟨n, rfl⟩
51 rw [hrange]
52 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
53 rcases hcomm_le hn with ⟨c, hc, hcn⟩
54 have hdiff : n * c⁻¹ ∈ U := by
55 apply hkerU
56 change f (n * c⁻¹) = 1
57 rw [map_mul, map_inv, ← hcn, mul_inv_cancel]
58 have hquot :
59 QuotientGroup.mk' U n = QuotientGroup.mk' U c :=
60 (QuotientGroup.eq_iff_div_mem (N := U)).2 (by
61 simpa [div_eq_mul_inv] using hdiff)
62 have hcquot :
63 QuotientGroup.mk' U c ∈ commutator (N ⧸ U) := by
64 have hmap :
65 (commutator N).map (QuotientGroup.mk' U) ≤
66 commutator (N ⧸ U) := by
67 rw [_root_.map_commutator_eq]
68 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
69 exact hmap ⟨c, hc, rfl⟩
70 simpa [hquot] using hcquot
72namespace IsProCGroup
74/-- Membership in the closed commutator subgroup of a pro-`C` group is detected on every
75open-normal quotient whose quotient lies in `C`. -/
76theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient
77 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G}
78 (hx : ∀ U : OpenNormalSubgroupInClass C G,
79 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
80 Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))) :
83 let e := openNormalSubgroupInClassMulEquivInverseLimit (C := C) (G := G) hForm hG
84 letI : Nonempty (OpenNormalSubgroupInClass C G) := openNormalSubgroupInClass_nonempty hG
85 letI : Nonempty (OrderDual (OpenNormalSubgroupInClass C G)) := inferInstance
86 letI : CompactSpace G := hG.compactSpace
87 letI : T2Space G := hG.t2Space
88 letI : TotallyDisconnectedSpace G := hG.totallyDisconnectedSpace
89 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Group (S.X U) := fun U => by
91 infer_instance
92 letI : InverseSystems.IsGroupSystem S := by
93 dsimp [S]
94 infer_instance
95 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Finite (S.X U) := fun U => by
97 exact hForm.finiteOnly (OrderDual.ofDual U).2
98 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), DiscreteTopology (S.X U) := fun U => by
100 exact QuotientGroup.discreteTopology
101 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
102 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), CompactSpace (S.X U) := fun _ => by
103 infer_instance
104 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), T2Space (S.X U) := fun _ => by
105 infer_instance
106 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G),
107 TotallyDisconnectedSpace (S.X U) := fun _ => by
108 infer_instance
109 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), IsTopologicalGroup (S.X U) :=
110 fun _ => by
111 infer_instance
112 letI : Group S.inverseLimit := by infer_instance
113 letI : IsTopologicalGroup S.inverseLimit := by infer_instance
114 have hlim : e x ∈ Subgroup.closedCommutator S.inverseLimit := by
116 (S := S) (directed_openNormalSubgroupInClass (C := C) (G := G) hForm)]
117 intro U
118 have hproj :
119 S.projection U (e x) =
120 openNormalSubgroupInClassProj (C := C) (G := G) U x := by
121 simpa [S, e] using
123 (C := C) (G := G) hForm hG U x
124 rw [hproj]
125 simpa [openNormalSubgroupInClassProj] using hx (OrderDual.ofDual U)
126 have hmap :
127 e x ∈
128 ((Subgroup.closedCommutator G).map e.toMulEquiv.toMonoidHom :
129 Subgroup S.inverseLimit) := by
131 exact hlim
132 rcases hmap with ⟨y, hy, hyx⟩
133 have hy_eq : y = x := by
134 exact e.toMulEquiv.injective hyx
135 simpa [hy_eq] using hy
137/-- Closed-commutator membership in a pro-`C` group is equivalent to closed-commutator
138membership after every open-normal quotient whose quotient lies in `C`. -/
139theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient
140 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G} :
143 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
144 Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G)) := by
145 constructor
146 · intro hx U
147 exact Subgroup.closedCommutator_map_le (OpenNormalSubgroupInClass.quotientProj (C := C) U)
148 ⟨x, hx, rfl⟩
149 · exact mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient hForm hG
151/-- To prove membership in the closed commutator subgroup of a pro-`C` group, it is enough to
152prove ordinary commutator membership in every finite open-normal quotient in `C`.
154This is the finite-stage form used by Magnus-kernel arguments: each quotient stage is discrete, so
155its closed commutator is the ordinary algebraic commutator subgroup. -/
156theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
157 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G}
158 (hx : ∀ U : OpenNormalSubgroupInClass C G,
159 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
160 commutator (G ⧸ (U.1 : Subgroup G))) :
162 mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient hForm hG
163 (by
164 intro U
167/-- Cofinal finite-stage form of closed-commutator detection.
169It is enough to prove ordinary commutator membership after passing, below every open-normal
170quotient in `C`, to some smaller open-normal quotient in `C`. -/
171theorem mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
172 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G}
173 (hx : ∀ U : OpenNormalSubgroupInClass C G,
175 (V.1 : Subgroup G) ≤ (U.1 : Subgroup G) ∧
176 QuotientGroup.mk' (V.1 : Subgroup G) x ∈
177 commutator (G ⧸ (V.1 : Subgroup G))) :
179 refine
180 mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
181 hForm hG ?_
182 intro U
183 rcases hx U with ⟨V, hVU, hxV⟩
184 let qVU : G ⧸ (V.1 : Subgroup G) →* G ⧸ (U.1 : Subgroup G) :=
185 QuotientGroup.map (V.1 : Subgroup G) (U.1 : Subgroup G)
186 (MonoidHom.id G) (by
187 intro g hg
188 exact hVU hg)
189 have hq :
190 qVU (QuotientGroup.mk' (V.1 : Subgroup G) x) =
191 QuotientGroup.mk' (U.1 : Subgroup G) x := by
192 simp only [QuotientGroup.mk'_apply, QuotientGroup.map_mk, MonoidHom.id_apply, qVU]
193 have hcomm_map :
194 (commutator (G ⧸ (V.1 : Subgroup G))).map qVU ≤
195 commutator (G ⧸ (U.1 : Subgroup G)) := by
196 rw [_root_.map_commutator_eq]
197 exact Subgroup.commutator_mono (by intro y hy; trivial) (by intro y hy; trivial)
198 have hxU :
199 qVU (QuotientGroup.mk' (V.1 : Subgroup G) x) ∈
200 commutator (G ⧸ (U.1 : Subgroup G)) :=
201 hcomm_map ⟨QuotientGroup.mk' (V.1 : Subgroup G) x, hxV, rfl⟩
202 simpa [hq] using hxU
204/-- Closed-commutator membership in a pro-`C` group is equivalent to ordinary commutator
205membership after every finite open-normal quotient in `C`. -/
206theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator
207 (hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) {x : G} :
210 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
211 commutator (G ⧸ (U.1 : Subgroup G)) := by
212 rw [mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient hForm hG]
213 constructor
214 · intro hx U
216 · intro hx U
219end IsProCGroup
221namespace ProCGroup
223/-- `ProCGroup`-namespace form of closed-commutator detection by finite open-normal quotients. -/
224theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient
225 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
226 [hG : ProCGroup ProC G] {x : G}
227 (hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
228 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
229 Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))) :
231 IsProCGroup.mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient
232 (C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup hx
234/-- `ProCGroup`-namespace iff form of closed-commutator detection by finite open-normal
235quotients. -/
236theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient
237 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
238 [hG : ProCGroup ProC G] {x : G} :
240 ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
241 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
242 Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G)) :=
243 IsProCGroup.mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient
244 (C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup
246/-- `ProCGroup`-namespace finite-stage form with ordinary commutators in the discrete quotient
247stages. -/
248theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
249 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
250 [hG : ProCGroup ProC G] {x : G}
251 (hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
252 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
253 commutator (G ⧸ (U.1 : Subgroup G))) :
255 IsProCGroup.mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator
256 (C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup hx
258/-- `ProCGroup`-namespace cofinal finite-stage form with ordinary commutators. -/
259theorem mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
260 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
261 [hG : ProCGroup ProC G] {x : G}
262 (hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
263 ∃ V : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
264 (V.1 : Subgroup G) ≤ (U.1 : Subgroup G) ∧
265 QuotientGroup.mk' (V.1 : Subgroup G) x ∈
266 commutator (G ⧸ (V.1 : Subgroup G))) :
268 IsProCGroup.mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator
269 (C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup hx
271/-- `ProCGroup`-namespace iff form with ordinary commutators in the discrete quotient stages. -/
272theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator
273 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
274 [hG : ProCGroup ProC G] {x : G} :
276 ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
277 QuotientGroup.mk' (U.1 : Subgroup G) x ∈
278 commutator (G ⧸ (U.1 : Subgroup G)) :=
279 IsProCGroup.mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator
280 (C := ProC.finiteQuotientClass) ProC.finiteQuotientFormation hG.isProCGroup
284end ProCGroups.ProC