Source: ProCGroups.ProC.OpenNormalSubgroups.ClosedCommutator

1import ProCGroups.Abelian.TopologicalAbelianizationLimits

2import ProCGroups.ProC.InverseLimits.FiniteQuotients

3import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation

5/-!

6# Detecting the closed commutator subgroup in finite quotients

8Membership in the topological closure of the commutator subgroup is characterized by the images

9in open-normal pro-\(C\) quotients. Equivalent formulations use quotient commutators and cofinal

10families of open normal subgroups.

11-/

13namespace ProCGroups.ProC

15open scoped Topology

17universe u

19variable {C : FiniteGroupClass.{u}}

20variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

21variable [CompactSpace G] [T2Space G]

23/--

24A quotient-level commutator descent along a surjective homomorphism. If \(f: N \to K\) is onto,

25f n is in the ordinary commutator subgroup of K, and the kernel of f dies in the quotient

26\(N/U\), then the image of n in \(N/U\) is in the ordinary commutator subgroup.

27-/

28theorem quotient_mk_mem_commutator_of_surjective_image_mem_commutator

29 {N K : Type u} [Group N] [Group K]

30 (f : N →* K) (hf : Function.Surjective f)

31 (U : Subgroup N) [U.Normal] (hkerU : f.ker ≤ U)

32 {n : N} (hn : f n ∈ commutator K) :

33 QuotientGroup.mk' U n ∈ commutator (N ⧸ U) := by

34 have hcomm_le :

35 commutator K ≤ (commutator N).map f := by

36 rw [_root_.map_commutator_eq]

37 have hrange : f.range = (⊤ : Subgroup K) := by

38 ext k

39 constructor

40 · intro hk

41 trivial

42 · intro _hk

43 rcases hf k with ⟨n, rfl⟩

44 exact ⟨n, rfl⟩

45 rw [hrange]

46 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)

47 rcases hcomm_le hn with ⟨c, hc, hcn⟩

48 have hdiff : n * c⁻¹ ∈ U := by

49 apply hkerU

50 change f (n * c⁻¹) = 1

51 rw [map_mul, map_inv, ← hcn, mul_inv_cancel]

52 have hquot :

53 QuotientGroup.mk' U n = QuotientGroup.mk' U c :=

54 (QuotientGroup.eq_iff_div_mem (N := U)).2 (by

55 simpa [div_eq_mul_inv] using hdiff)

56 have hcquot :

57 QuotientGroup.mk' U c ∈ commutator (N ⧸ U) := by

58 have hmap :

59 (commutator N).map (QuotientGroup.mk' U) ≤

60 commutator (N ⧸ U) := by

61 rw [_root_.map_commutator_eq]

62 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)

63 exact hmap ⟨c, hc, rfl⟩

64 simpa [hquot] using hcquot

66namespace HasOpenNormalBasisInClass

68/--

69Membership in the closed commutator subgroup of a pro-\(C\) group is detected on every

70open-normal quotient whose quotient lies in \(C\).

71-/

72theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient

73 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G}

74 (hx : ∀ U : OpenNormalSubgroupInClass C G,

75 QuotientGroup.mk' (U.1 : Subgroup G) x ∈

76 Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G))) :

77 x ∈ Subgroup.closedCommutator G := by

78 let S := openNormalSubgroupInClassSystem C G

79 let e := openNormalSubgroupInClassMulEquivInverseLimit (C := C) (G := G) hForm hG

80 letI : Nonempty (OpenNormalSubgroupInClass C G) := openNormalSubgroupInClass_nonempty hG

81 letI : Nonempty (OrderDual (OpenNormalSubgroupInClass C G)) := inferInstance

82 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Group (S.X U) := fun U =>

83 instGroupOpenNormalSubgroupInClassSystemX (C := C) (G := G) U

84 letI : InverseSystems.IsGroupSystem S := by

85 dsimp [S]

86 infer_instance

87 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Finite (S.X U) := fun U => by

88 dsimp [S, openNormalSubgroupInClassSystem]

89 exact C.finite (OrderDual.ofDual U).2

90 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), DiscreteTopology (S.X U) := fun U => by

91 dsimp [S, openNormalSubgroupInClassSystem]

92 exact QuotientGroup.discreteTopology

93 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))

94 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), CompactSpace (S.X U) := fun _ => by

95 infer_instance

96 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), T2Space (S.X U) := fun _ => by

97 infer_instance

98 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G),

99 TotallyDisconnectedSpace (S.X U) := fun _ => by

100 infer_instance

101 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), IsTopologicalGroup (S.X U) :=

102 fun _ => by

103 infer_instance

104 letI : Group S.inverseLimit := by infer_instance

105 letI : IsTopologicalGroup S.inverseLimit := by infer_instance

106 have hlim : e x ∈ Subgroup.closedCommutator S.inverseLimit := by

107 rw [ProCGroups.Abelian.mem_closedCommutator_inverseLimit_iff

108 (S := S) (directed_openNormalSubgroupInClass (C := C) (G := G) hForm)]

109 intro U

110 have hproj :

111 S.projection U (e x) =

112 openNormalSubgroupInClassProj (C := C) (G := G) U x := by

113 simpa [S, e] using

114 openNormalSubgroupInClassMulEquivInverseLimit_projection

115 (C := C) (G := G) hForm hG U x

116 rw [hproj]

117 have hxU := hx (OrderDual.ofDual U)

118 simp only [Subgroup.closedCommutator_eq_commutator_of_discrete] at hxU ⊢

119 change

120 openNormalSubgroupInClassProj (C := C) (G := G) U x ∈

121 @commutator (S.X U)

122 (instGroupOpenNormalSubgroupInClassSystemX

123 (C := C) (G := G) U) at hxU

124 exact hxU

125 have hmap :

126 e x ∈

127 ((Subgroup.closedCommutator G).map e.toMulEquiv.toMonoidHom :

128 Subgroup S.inverseLimit) := by

129 rw [Subgroup.closedCommutator_map_eq_of_equiv e]

130 exact hlim

131 rcases hmap with ⟨y, hy, hyx⟩

132 have hy_eq : y = x := by

133 exact e.toMulEquiv.injective hyx

134 subst y

135 exact hy

136

137/--

138Closed-commutator membership in a pro-\(C\) group is equivalent to closed-commutator membership

139after every open-normal quotient whose quotient lies in \(C\).

140-/

141theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient

142 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G} :

143 x ∈ Subgroup.closedCommutator G ↔

144 ∀ U : OpenNormalSubgroupInClass C G,

145 QuotientGroup.mk' (U.1 : Subgroup G) x ∈

146 Subgroup.closedCommutator (G ⧸ (U.1 : Subgroup G)) := by

147 constructor

148 · intro hx U

149 exact Subgroup.closedCommutator_map_le (OpenNormalSubgroupInClass.quotientProj (C := C) U)

150 ⟨x, hx, rfl⟩

151 · exact mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient hForm hG

152

153/--

154An element belongs to the closed commutator subgroup of a pro-\(C\) group when its image belongs

155to the ordinary commutator subgroup in every finite open-normal quotient in \(C\).

156-/

157theorem mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator

158 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G}

159 (hx : ∀ U : OpenNormalSubgroupInClass C G,

160 QuotientGroup.mk' (U.1 : Subgroup G) x ∈

161 commutator (G ⧸ (U.1 : Subgroup G))) :

162 x ∈ Subgroup.closedCommutator G :=

163 mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient hForm hG

164 (by

165 intro U

166 simpa [Subgroup.closedCommutator_eq_commutator_of_discrete] using hx U)

167

168/--

169An element belongs to the closed commutator subgroup when, below every open-normal quotient in

170\(C\), its image belongs to the ordinary commutator subgroup in some smaller open-normal

171quotient in \(C\).

172-/

173theorem mem_closedCommutator_of_forall_exists_openNormalSubgroupInClass_le_quotient_commutator

174 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G}

175 (hx : ∀ U : OpenNormalSubgroupInClass C G,

176 ∃ V : OpenNormalSubgroupInClass C G,

177 (V.1 : Subgroup G) ≤ (U.1 : Subgroup G) ∧

178 QuotientGroup.mk' (V.1 : Subgroup G) x ∈

179 commutator (G ⧸ (V.1 : Subgroup G))) :

180 x ∈ Subgroup.closedCommutator G := by

181 refine

182 mem_closedCommutator_of_forall_openNormalSubgroupInClass_quotient_commutator

183 hForm hG ?_

184 intro U

185 rcases hx U with ⟨V, hVU, hxV⟩

186 let qVU : G ⧸ (V.1 : Subgroup G) →* G ⧸ (U.1 : Subgroup G) :=

187 QuotientGroup.map (V.1 : Subgroup G) (U.1 : Subgroup G)

188 (MonoidHom.id G) (by

189 intro g hg

190 exact hVU hg)

191 have hq :

192 qVU (QuotientGroup.mk' (V.1 : Subgroup G) x) =

193 QuotientGroup.mk' (U.1 : Subgroup G) x := by

194 simp only [QuotientGroup.mk'_apply, QuotientGroup.map_mk, MonoidHom.id_apply, qVU]

195 have hcomm_map :

196 (commutator (G ⧸ (V.1 : Subgroup G))).map qVU ≤

197 commutator (G ⧸ (U.1 : Subgroup G)) := by

198 rw [_root_.map_commutator_eq]

199 exact Subgroup.commutator_mono (by intro y hy; trivial) (by intro y hy; trivial)

200 have hxU :

201 qVU (QuotientGroup.mk' (V.1 : Subgroup G) x) ∈

202 commutator (G ⧸ (U.1 : Subgroup G)) :=

203 hcomm_map ⟨QuotientGroup.mk' (V.1 : Subgroup G) x, hxV, rfl⟩

204 rw [hq] at hxU

205 exact hxU

206

207/--

208Closed-commutator membership in a pro-\(C\) group is equivalent to ordinary commutator

209membership after every finite open-normal quotient in \(C\).

210-/

211theorem mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient_commutator

212 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) {x : G} :

213 x ∈ Subgroup.closedCommutator G ↔

214 ∀ U : OpenNormalSubgroupInClass C G,

215 QuotientGroup.mk' (U.1 : Subgroup G) x ∈

216 commutator (G ⧸ (U.1 : Subgroup G)) := by

217 rw [mem_closedCommutator_iff_forall_openNormalSubgroupInClass_quotient hForm hG]

218 constructor

219 · intro hx U

220 simpa [Subgroup.closedCommutator_eq_commutator_of_discrete] using hx U

221 · intro hx U

222 simpa [Subgroup.closedCommutator_eq_commutator_of_discrete] using hx U

223

224end HasOpenNormalBasisInClass

225

226end ProCGroups.ProC