Source: ProCGroups.ProC.Subgroups.Closed

1import ProCGroups.ProC.InverseLimits.Limits

3/-!

4# Closed subgroups, ranges, and extensions of pro-\(C\) groups

6The pro-\(C\) basis passes to closed subgroups when \(C\) is subgroup-closed,

7to Hausdorff continuous quotients when \(C\) is a formation, and across a

8closed normal extension when \(C\) is extension-closed.

9-/

11open Set

12open scoped Topology Pointwise

14namespace ProCGroups.ProC

16universe u

18section

20variable {C : FiniteGroupClass.{u}}

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

23namespace HasOpenNormalBasisInClass

25omit [IsTopologicalGroup G] in

26/-- A closed subgroup of a pro-\(C\) group is pro-\(C\). -/

27theorem of_closedSubgroup

28 (hIso : FiniteGroupClass.IsomClosed C)

29 (hSub : FiniteGroupClass.SubgroupClosed C)

30 (hG : HasOpenNormalBasisInClass C G) (H : ClosedSubgroup G) :

31 HasOpenNormalBasisInClass C ↥(H : Subgroup G) := by

32 intro W hW h1W

33 have hW_nhds : W ∈ 𝓝 (1 : H) := hW.mem_nhds h1W

34 rcases (mem_nhds_subtype (H : Set G) (1 : H) W).1 hW_nhds with

35 ⟨W₀, hW₀_nhds, hW₀W⟩

36 rcases mem_nhds_iff.mp hW₀_nhds with ⟨W', hW'W₀, hW'open, h1W'⟩

37 rcases hG W' hW'open h1W' with ⟨V, hVW', hCV⟩

38 let VH : OpenNormalSubgroup H :=

39 OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V

40 have hVHW : (((VH : Subgroup H) : Set H)) ⊆ W := by

41 intro x hx

42 exact hW₀W <| by

43 change x.1 ∈ W₀

44 exact hW'W₀ (hVW' hx)

45 let ψ : H →* G ⧸ (V : Subgroup G) :=

46 (QuotientGroup.mk' (V : Subgroup G)).comp ((H : Subgroup G).subtype)

47 have hRange : C ψ.range := hSub ψ.range hCV

48 have hKerEq : (VH : Subgroup H) = ψ.ker := by

49 ext x

50 constructor

51 · intro hx

52 change x.1 ∈ (V : Subgroup G) at hx

53 rw [MonoidHom.mem_ker]

54 change QuotientGroup.mk' (V : Subgroup G) x.1 = 1

55 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) x.1).2 hx

56 · intro hx

57 rw [MonoidHom.mem_ker] at hx

58 change QuotientGroup.mk' (V : Subgroup G) x.1 = 1 at hx

59 change x.1 ∈ (V : Subgroup G)

60 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) x.1).1

61 hx

62 have hQuotVH : C (H ⧸ (VH : Subgroup H)) := by

63 let e1 : H ⧸ (VH : Subgroup H) ≃* H ⧸ ψ.ker :=

64 QuotientGroup.quotientMulEquivOfEq hKerEq

65 exact hIso

66 ⟨(e1.trans (QuotientGroup.quotientKerEquivRange ψ)).symm⟩

67 hRange

68 exact ⟨VH, hVHW, hQuotVH⟩

70omit [IsTopologicalGroup G] in

71/-- A closed ordinary subgroup of a pro-\(C\) group is pro-\(C\) with the induced topology. -/

72theorem of_isClosed_subgroup

73 (hIso : FiniteGroupClass.IsomClosed C)

74 (hSub : FiniteGroupClass.SubgroupClosed C)

75 (hG : HasOpenNormalBasisInClass C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :

76 HasOpenNormalBasisInClass C H := by

77 let HC : ClosedSubgroup G := ⟨H, hH⟩

78 simpa using of_closedSubgroup (C := C) hIso hSub hG HC

80omit [IsTopologicalGroup G] in

81/-- Closed-subgroup permanence for pro-\(C\) groups from a full formation package. -/

82theorem of_closedSubgroup_of_fullFormation

83 (hC : FiniteGroupClass.FullFormation C)

84 (hG : HasOpenNormalBasisInClass C G) (H : ClosedSubgroup G) :

85 HasOpenNormalBasisInClass C ↥(H : Subgroup G) :=

86 of_closedSubgroup hC.isomClosed hC.subgroupClosed hG H

88omit [IsTopologicalGroup G] in

89/-- Closed-subgroup permanence in ordinary subgroup form from a full formation package. -/

90theorem of_isClosed_subgroup_of_fullFormation

91 (hC : FiniteGroupClass.FullFormation C)

92 (hG : HasOpenNormalBasisInClass C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :

93 HasOpenNormalBasisInClass C H :=

94 of_isClosed_subgroup hC.isomClosed hC.subgroupClosed hG H hH

96/--

97The range of a continuous homomorphism from a pro-\(C\) group to a Hausdorff topological group

98is again pro-\(C\), with the induced subtype topology.

99-/

100theorem range

101 (hIso : FiniteGroupClass.IsomClosed C)

102 (hQuot : FiniteGroupClass.QuotientClosed C)

103 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

104 (hG : HasOpenNormalBasisInClass C G)

105 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]

106 (f : G →ₜ* H) :

107 HasOpenNormalBasisInClass C f.toMonoidHom.range := by

108 let K : Subgroup G := f.toMonoidHom.ker

109 have hKclosed : IsClosed (K : Set G) := by

110 dsimp [K]

111 exact ContinuousMonoidHom.isClosed_ker f

112 letI : K.Normal := by

113 dsimp [K]

114 infer_instance

115 have hQuotG : HasOpenNormalBasisInClass C (G ⧸ K) :=

116 quotient_closedNormalSubgroup (C := C) hIso hQuot hG K hKclosed

117 have e : (G ⧸ K) ≃ₜ* f.toMonoidHom.range := by

118 simpa [K] using ContinuousMonoidHom.quotientKerContinuousMulEquivRange f

119 exact HasOpenNormalBasisInClass.ofContinuousMulEquiv (C := C) (G := G ⧸ K) hQuotG e

120

121end HasOpenNormalBasisInClass

122

123/-- A Hausdorff continuous quotient of a group with an open-normal \(C\)-basis again has such a

124basis. -/

125theorem HasOpenNormalBasisInClass.of_surjective

126 (hForm : FiniteGroupClass.Formation C)

127 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

128 (hG : HasOpenNormalBasisInClass C G)

129 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]

130 (f : G →ₜ* H) (hf : Function.Surjective f) :

131 HasOpenNormalBasisInClass C H := by

132 let R : Subgroup H := f.toMonoidHom.range

133 have hR : HasOpenNormalBasisInClass C R :=

134 HasOpenNormalBasisInClass.range hForm.isomClosed hForm.quotientClosed hG f

135 letI : CompactSpace R :=

136 isCompact_iff_compactSpace.mp (by

137 simpa [R] using isCompact_range f.continuous_toFun)

138 let e : R ≃ₜ* H :=

139 ContinuousMulEquiv.ofBijectiveCompactToT2 (Subgroup.subtype R)

140 continuous_subtype_val

141 ⟨by

142 intro x y hxy

143 exact Subtype.ext hxy,

144 by

145 intro h

146 rcases hf h with ⟨g, rfl⟩

147 exact ⟨⟨f g, ⟨g, rfl⟩⟩, rfl⟩⟩

148 exact HasOpenNormalBasisInClass.ofContinuousMulEquiv hR e

149

150namespace HasOpenNormalBasisInClass

151

152variable {E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]

153

154/--

155If E is profinite, K is a normal pro-\(C\) subgroup of E, and E/K is pro-\(C\), then E is

156pro-\(C\).

157-/

158theorem extension

159 (hIso : FiniteGroupClass.IsomClosed C)

160 (hQuot : FiniteGroupClass.QuotientClosed C)

161 (hExt : FiniteGroupClass.ExtensionClosed C)

162 [CompactSpace E] [T2Space E] [TotallyDisconnectedSpace E]

163 (K : Subgroup E) [K.Normal] (hKclosed : IsClosed (K : Set E))

164 (hK : HasOpenNormalBasisInClass C K) (hQ : HasOpenNormalBasisInClass C (E ⧸ K)) :

165 HasOpenNormalBasisInClass C E := by

166 letI : IsClosed (K : Set E) := hKclosed

167 refine HasOpenNormalBasisInClass.of_allOpenNormalQuotients (C := C)

168 ?_

169 intro U

170 letI : CompactSpace (E ⧸ K) := by infer_instance

171 letI : T2Space (E ⧸ K) := by infer_instance

172 let M : Subgroup E := K ⊔ (U : Subgroup E)

173 let Wsub : Subgroup (E ⧸ K) := Subgroup.map (QuotientGroup.mk' K) M

174 have hWclosed : IsClosed (Wsub : Set (E ⧸ K)) := by

175 have hMclosed : IsClosed (M : Set E) := by

176 have hMopen : IsOpen (M : Set E) := by

177 exact Subgroup.isOpen_of_openSubgroup M (show (U : Subgroup E) ≤ M from le_sup_right)

178 exact Subgroup.isClosed_of_isOpen M hMopen

179 have hMcompact : IsCompact (M : Set E) := hMclosed.isCompact

180 have hcont : Continuous (QuotientGroup.mk' K : E → E ⧸ K) := continuous_quotient_mk'

181 have himage : IsCompact ((QuotientGroup.mk' K) '' (M : Set E)) := hMcompact.image hcont

182 have hEq : (QuotientGroup.mk' K) '' (M : Set E) = (Wsub : Set (E ⧸ K)) := by

183 ext x

184 simp only [QuotientGroup.mk'_apply, mem_image, SetLike.mem_coe, Subgroup.coe_map, M, Wsub]

185 rw [← hEq]

186 exact himage.isClosed

187 have hWfinite : Finite ((E ⧸ K) ⧸ Wsub) := by

188 have hMopen : IsOpen (M : Set E) := by

189 exact Subgroup.isOpen_of_openSubgroup M (show (U : Subgroup E) ≤ M from le_sup_right)

190 have hMfinite : Finite (E ⧸ M) :=

191 (subgroup_isOpen_iff_isClosed_finite_quotient (G := E) (U := M)).1 hMopen |>.2

192 let e : (E ⧸ K) ⧸ Wsub ≃* E ⧸ M := by

193 simpa [Wsub, M, Subgroup.map_sup] using

194 (QuotientGroup.quotientQuotientEquivQuotient K M (show K ≤ M from le_sup_left))

195 exact Finite.of_injective e e.injective

196 have hWopen : IsOpen (Wsub : Set (E ⧸ K)) :=

197 (subgroup_isOpen_iff_isClosed_finite_quotient (G := E ⧸ K) (U := Wsub)).2

198 ⟨hWclosed, hWfinite⟩

199 letI : Wsub.Normal := by

200 dsimp [Wsub, M]

201 have hMnormal : M.Normal := by infer_instance

202 exact Subgroup.Normal.map hMnormal (QuotientGroup.mk' K) (QuotientGroup.mk'_surjective K)

203 let W : OpenNormalSubgroup (E ⧸ K) :=

204 { toOpenSubgroup := ⟨Wsub, hWopen⟩

205 isNormal' := inferInstance }

206 have hQuotM : C (E ⧸ M) := by

207 let e : (E ⧸ K) ⧸ (W : Subgroup (E ⧸ K)) ≃* E ⧸ M := by

208 simpa [W, Wsub, M, Subgroup.map_sup] using

209 (QuotientGroup.quotientQuotientEquivQuotient K M (show K ≤ M from le_sup_left))

210 exact hIso ⟨e⟩

211 (HasOpenNormalBasisInClass.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed

212 hIso hQuot hQ W)

213 let KU : OpenNormalSubgroup K :=

214 OpenNormalSubgroup.comap (K.subtype) continuous_subtype_val U

215 let ψ : K →* E ⧸ (U : Subgroup E) :=

216 (QuotientGroup.mk' (U : Subgroup E)).comp K.subtype

217 have hKerEq : (KU : Subgroup K) = ψ.ker := by

218 ext x

219 constructor

220 · intro hx

221 simpa [MonoidHom.mem_ker, KU, ψ] using

222 (QuotientGroup.eq_one_iff (N := (U : Subgroup E)) x.1).2 hx

223 · intro hx

224 exact (QuotientGroup.eq_one_iff (N := (U : Subgroup E)) x.1).1

225 (by simpa [MonoidHom.mem_ker, KU, ψ] using hx)

226 have hKernelC : C ψ.range := by

227 have hQuotKU : C (K ⧸ (KU : Subgroup K)) :=

228 HasOpenNormalBasisInClass.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed

229 hIso hQuot hK KU

230 let e1 : K ⧸ (KU : Subgroup K) ≃* K ⧸ ψ.ker :=

231 QuotientGroup.quotientMulEquivOfEq hKerEq

232 exact hIso ⟨e1.trans (QuotientGroup.quotientKerEquivRange ψ)⟩ hQuotKU

233 let L : Subgroup (E ⧸ (U : Subgroup E)) := Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) K

234 have hRangeEq : ψ.range = L := by

235 ext x

236 simp only [MonoidHom.mem_range, MonoidHom.coe_comp, QuotientGroup.coe_mk', Subgroup.coe_subtype,

237 Function.comp_apply, Subtype.exists, exists_prop, Subgroup.mem_map, QuotientGroup.mk'_apply, ψ, L]

238 have hLC : C L := by

239 exact hIso ⟨MulEquiv.subgroupCongr hRangeEq⟩ hKernelC

240 have hMapUbot : Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) (U : Subgroup E) = ⊥ := by

241 ext x

242 constructor

243 · intro hx

244 rcases (Subgroup.mem_map).1 hx with ⟨u, hu, hux⟩

245 rw [Subgroup.mem_bot]

246 have hu1 : QuotientGroup.mk' (U : Subgroup E) u = 1 :=

247 (QuotientGroup.eq_one_iff (N := (U : Subgroup E)) u).2 hu

248 exact hux.symm.trans hu1

249 · intro hx

250 rcases Subgroup.mem_bot.1 hx with rfl

251 exact ⟨1, U.one_mem, by simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]⟩

252 have hMapM : Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M = L := by

253 calc

254 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M

255 = Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) K ⊔

256 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) (U : Subgroup E) := by

257 simp only [Subgroup.map_sup, QuotientGroup.map_mk'_self, bot_le, sup_of_le_left, M]

258 _ = L ⊔ ⊥ := by simp only [hMapUbot, bot_le, sup_of_le_left, L]

259 _ = L := by simp only [bot_le, sup_of_le_left]

260 have hQuotL : C ((E ⧸ (U : Subgroup E)) ⧸ L) := by

261 let e0 : (E ⧸ (U : Subgroup E)) ⧸ L ≃* (E ⧸ (U : Subgroup E)) ⧸

262 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M :=

263 QuotientGroup.quotientMulEquivOfEq hMapM.symm

264 let e1 : (E ⧸ (U : Subgroup E)) ⧸

265 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M ≃* E ⧸ M :=

266 QuotientGroup.quotientQuotientEquivQuotient (U : Subgroup E) M

267 (show (U : Subgroup E) ≤ M from le_sup_right)

268 exact hIso ⟨(e0.trans e1).symm⟩ hQuotM

269 letI : L.Normal := by

270 dsimp [L]

271 exact Subgroup.Normal.map inferInstance (QuotientGroup.mk' (U : Subgroup E))

272 (QuotientGroup.mk'_surjective (U : Subgroup E))

273 exact hExt L hLC hQuotL

274

275end HasOpenNormalBasisInClass

276

277end

278

279end ProCGroups.ProC