Source: ProCGroups.Completion.SameFiniteQuotients

1import Mathlib.GroupTheory.Finiteness

2import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

3import ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation

5/-!

6# Pro C Groups / Completion / Same Finite Quotients

8This module compares abstract finite quotients with continuous finite discrete

9quotients and constructs maps between profinite completions from that comparison.

10-/

12open scoped Topology

14namespace ProCGroups.Completion

16universe u

18/-- Topological finite quotient predicate using continuous maps to finite discrete groups. -/

19def HasSameContinuousFiniteDiscreteQuotients

20 (G₁ : Type u) [Group G₁] [TopologicalSpace G₁]

21 (G₂ : Type u) [Group G₂] [TopologicalSpace G₂] : Prop :=

22 ∀ (Q : Type u) [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]

23 [Finite Q] [DiscreteTopology Q],

24 (∃ φ : G₁ →ₜ* Q, Function.Surjective φ) ↔

25 (∃ ψ : G₂ →ₜ* Q, Function.Surjective ψ)

27/--

28The continuous finite quotient hypothesis yields a surjective continuous homomorphism between

29topologically finitely generated profinite groups.

30-/

31theorem

32 exists_surj_continuousMonoidHom_between_profiniteGroups_of_sameContinuousFiniteDiscreteQuotients

33 {G₁ : Type u} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]

34 {G₂ : Type u} [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]

35 [CompactSpace G₁]

36 [CompactSpace G₂] [T2Space G₂] [TotallyDisconnectedSpace G₂]

37 (hG₁fg : FiniteGeneration.TopologicallyFinitelyGenerated G₁)

38 (hquot : HasSameContinuousFiniteDiscreteQuotients G₁ G₂) :

39 ∃ φ : ContinuousMonoidHom G₁ G₂, Function.Surjective φ := by

40 classical

41 let C := FiniteGroupClass.allFinite

42 have hG₂proC : ProC.HasOpenNormalBasisInClass C G₂ := by

43 exact ProC.hasOpenNormalBasisInClass_allFinite

44 let S₂ : InverseSystems.InverseSystem

45 (I := OrderDual (ProC.OpenNormalSubgroupInClass C G₂)) :=

46 ProC.openNormalSubgroupInClassSystem C G₂

47 let SurjHom (U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂)) :=

48 { φ : ContinuousMonoidHom G₁ (S₂.X U) // Function.Surjective φ }

49 letI : Nonempty (ProC.OpenNormalSubgroupInClass C G₂) :=

50 ProC.HasOpenNormalBasisInClass.openNormalSubgroupInClass_nonempty hG₂proC

51 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

52 Group (S₂.X U) := fun U =>

53 ProC.instGroupOpenNormalSubgroupInClassSystemX

54 (C := C) (G := G₂) U

55 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

56 IsTopologicalGroup (S₂.X U) := fun U => by

57 letI : DiscreteTopology (S₂.X U) := by

58 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]

59 exact QuotientGroup.discreteTopology

60 (openNormalSubgroup_isOpen (G := G₂)

61 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G₂))

62 exact topologicalGroup_of_discreteTopology

63 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

64 Finite (S₂.X U) := fun U => by

65 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]

66 exact (OrderDual.ofDual U).2

67 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

68 DiscreteTopology (S₂.X U) := fun U => by

69 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]

70 exact QuotientGroup.discreteTopology

71 (openNormalSubgroup_isOpen (G := G₂)

72 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G₂))

73 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

74 Finite (ContinuousMonoidHom G₁ (S₂.X U)) := fun U => by

75 exact

76 FiniteGeneration.finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated

77 (G := G₁) (R := S₂.X U) hG₁fg

78 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

79 TopologicalSpace (SurjHom U) := fun _ => ⊥

80 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

81 DiscreteTopology (SurjHom U) := fun _ => ⟨rfl⟩

82 let X₂ : InverseSystems.InverseSystem

83 (I := OrderDual (ProC.OpenNormalSubgroupInClass C G₂)) :=

84 { X := SurjHom

85 topologicalSpace := fun _ => ⊥

86 map := fun {U V} hUV φ => by

87 have hUV' : ((OrderDual.ofDual V).1 : Subgroup G₂) ≤ (OrderDual.ofDual U).1 := hUV

88 let qUV : ContinuousMonoidHom (S₂.X V) (S₂.X U) :=

89 { toMonoidHom := by

90 dsimp [S₂, ProC.openNormalSubgroupInClassSystem]

91 exact ProC.OpenNormalSubgroupInClass.map

92 (C := C) (G := G₂)

93 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'

94 continuous_toFun := continuous_of_discreteTopology }

95 refine ⟨qUV.comp φ.1, ?_⟩

96 intro x

97 rcases (ProC.OpenNormalSubgroupInClass.map_surjective

98 (C := C) (G := G₂)

99 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV') x with ⟨y, hy⟩

100 rcases φ.2 y with ⟨z, hz⟩

101 refine ⟨z, ?_⟩

102 calc

103 (qUV.comp φ.1) z = qUV (φ.1 z) := rfl

104 _ = qUV y := by rw [hz]

105 _ = x := hy

106 continuous_map := by

107 intro U V hUV

108 exact continuous_of_discreteTopology

109 map_id := by

110 intro U

111 funext φ

112 apply Subtype.ext

113 apply ContinuousMonoidHom.ext

114 intro x

115 change ProC.OpenNormalSubgroupInClass.map

116 (C := C) (G := G₂)

117 (U := OrderDual.ofDual U) (V := OrderDual.ofDual U) (le_rfl)

118 (φ.1 x) = φ.1 x

119 exact congrFun

120 (congrArg DFunLike.coe

121 (ProC.OpenNormalSubgroupInClass.map_id

122 (C := C) (G := G₂) (U := OrderDual.ofDual U)))

123 (φ.1 x)

124 map_comp := by

125 intro U V W hUV hVW

126 have hUV' : ((OrderDual.ofDual V).1 : Subgroup G₂) ≤ (OrderDual.ofDual U).1 := hUV

127 have hVW' : ((OrderDual.ofDual W).1 : Subgroup G₂) ≤ (OrderDual.ofDual V).1 := hVW

128 funext φ

129 apply Subtype.ext

130 apply ContinuousMonoidHom.ext

131 intro x

132 change ProC.OpenNormalSubgroupInClass.map

133 (C := C) (G := G₂)

134 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV'

135 (ProC.OpenNormalSubgroupInClass.map

136 (C := C) (G := G₂)

137 (U := OrderDual.ofDual V) (V := OrderDual.ofDual W) hVW' (φ.1 x)) =

138 ProC.OpenNormalSubgroupInClass.map

139 (C := C) (G := G₂)

140 (U := OrderDual.ofDual U) (V := OrderDual.ofDual W) (hVW'.trans hUV')

141 (φ.1 x)

142 exact

143 congrArg

144 (fun f : G₂ ⧸ (((OrderDual.ofDual W).1 : OpenNormalSubgroup G₂) : Subgroup G₂) →*

145 G₂ ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G₂) : Subgroup G₂) =>

146 f (φ.1 x))

147 (ProC.OpenNormalSubgroupInClass.map_comp

148 (C := C) (G := G₂)

149 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) (W := OrderDual.ofDual W)

150 hUV' hVW') }

151 letI : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

152 Nonempty (X₂.X U) := fun U => by

153 dsimp [X₂]

154 let qU : G₂ →ₜ* S₂.X U :=

155 { toMonoidHom := ProC.openNormalSubgroupInClassProj

156 (C := C) (G := G₂) U

157 continuous_toFun := by

158 change Continuous

159 (QuotientGroup.mk'

160 (((OrderDual.ofDual U).1 : OpenNormalSubgroup G₂) : Subgroup G₂))

161 exact continuous_quotient_mk' }

162 have hqUsurj : Function.Surjective qU :=

163 ProC.openNormalSubgroupInClassProj_surjective

164 (C := C) (G := G₂) U

165 rcases (hquot (S₂.X U)).2 ⟨qU, hqUsurj⟩ with ⟨φ, hφsurj⟩

166 exact ⟨⟨φ, hφsurj⟩⟩

167 have hdir₂ :

168 Directed

169 (α := OrderDual (ProC.OpenNormalSubgroupInClass C G₂))

170 (· ≤ ·) (fun U => U) := by

171 intro U V

172 let W : ProC.OpenNormalSubgroupInClass C G₂ :=

173 ⟨(OrderDual.ofDual U).1 ⊓ (OrderDual.ofDual V).1,

174 FiniteGroupClass.Formation.quotient_inf_mem

175 (C := C) (G := G₂)

176 FiniteGroupClass.allFinite_formation

177 (OrderDual.ofDual U).1 (OrderDual.ofDual V).1

178 (OrderDual.ofDual U).2 (OrderDual.ofDual V).2⟩

179 refine ⟨OrderDual.toDual W, ?_, ?_⟩

180 · change ((W.1 : Subgroup G₂) ≤ ((OrderDual.ofDual U).1 : Subgroup G₂))

181 exact inf_le_left

182 · change ((W.1 : Subgroup G₂) ≤ ((OrderDual.ofDual V).1 : Subgroup G₂))

183 exact inf_le_right

184 rcases InverseSystems.InverseSystem.nonempty_inverseLimit_of_finite (S := X₂) hdir₂ with ⟨x₂⟩

185 let ψ₂ : ∀ U : OrderDual (ProC.OpenNormalSubgroupInClass C G₂),

186 G₁ → S₂.X U := fun U => (x₂.1 U).1

187 have hψ₂cont : ∀ U, Continuous (ψ₂ U) := by

188 intro U

189 exact ((x₂.1 U).1).continuous_toFun

190 have hψ₂compat : S₂.CompatibleMaps ψ₂ := by

191 intro U V hUV

192 funext x

193 have hEq : X₂.map hUV (x₂.1 V) = x₂.1 U := x₂.2 U V hUV

194 have hEq' : (X₂.map hUV (x₂.1 V)).1 = (x₂.1 U).1 := congrArg Subtype.val hEq

195 exact congrArg (fun φ : ContinuousMonoidHom G₁ (S₂.X U) => φ x) hEq'

196 have hψ₂surj : ∀ U, Function.Surjective (ψ₂ U) := by

197 intro U

198 exact (x₂.1 U).2

199 let fToInv : ContinuousMonoidHom G₁ S₂.inverseLimit :=

200 { toMonoidHom :=

201 { toFun := S₂.inverseLimitLift ψ₂ hψ₂compat

202 map_one' := by

203 apply S₂.ext

204 intro U

205 calc

206 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat 1) = ψ₂ U 1 := by

207 simpa [Function.comp] using congrFun (S₂.projection_comp_inverseLimitLift ψ₂

208 hψ₂compat U) (1 : G₁)

209 _ = 1 := by simp only [map_one, ψ₂]

210 map_mul' := by

211 intro x y

212 apply S₂.ext

213 intro U

214 calc

215 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat (x * y)) = ψ₂ U (x * y) := by

216 simpa [Function.comp] using

217 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) (x * y)

218 _ = ψ₂ U x * ψ₂ U y := by simp only [map_mul, ψ₂]

219 _ = S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat x) *

220 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat y) := by

221 have hπx :

222 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat x) = ψ₂ U x := by

223 simpa [Function.comp] using

224 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) x

225 have hπy :

226 S₂.projection U (S₂.inverseLimitLift ψ₂ hψ₂compat y) = ψ₂ U y := by

227 simpa [Function.comp] using

228 congrFun (S₂.projection_comp_inverseLimitLift ψ₂ hψ₂compat U) y

229 rw [← hπx, ← hπy] }

230 continuous_toFun := S₂.continuous_inverseLimitLift ψ₂ hψ₂cont hψ₂compat }

231 have hfToInv_surj : Function.Surjective (S₂.inverseLimitLift ψ₂ hψ₂compat) :=

232 S₂.surjective_inverseLimitLift ψ₂ hψ₂cont hψ₂compat hψ₂surj hdir₂

233 let e₂ : G₂ ≃ₜ* S₂.inverseLimit :=

234 ProC.HasOpenNormalBasisInClass.openNormalSubgroupInClassMulEquivInverseLimit

235 (C := C) (G := G₂)

236 FiniteGroupClass.allFinite_formation hG₂proC

237 let e₂symmHom : ContinuousMonoidHom S₂.inverseLimit G₂ :=

238 { toMonoidHom := e₂.symm.toMonoidHom

239 continuous_toFun := e₂.symm.continuous_toFun }

240 refine ⟨e₂symmHom.comp fToInv, ?_⟩

241 intro y

242 rcases hfToInv_surj (e₂ y) with ⟨x, hx⟩

243 refine ⟨x, ?_⟩

244 change e₂.symm (S₂.inverseLimitLift ψ₂ hψ₂compat x) = y

245 rw [hx]

246 exact e₂.symm_apply_apply y

247

248/--

249Topologically finitely generated profinite groups are determined by their continuous finite

250discrete quotients.

251-/

252theorem topologicallyFinitelyGenerated_profiniteGroups_iso_of_sameContinuousFiniteQuotients

253 {G₁ : Type u} [Group G₁] [TopologicalSpace G₁] [IsTopologicalGroup G₁]

254 {G₂ : Type u} [Group G₂] [TopologicalSpace G₂] [IsTopologicalGroup G₂]

255 [CompactSpace G₁] [T2Space G₁] [TotallyDisconnectedSpace G₁]

256 [CompactSpace G₂] [T2Space G₂] [TotallyDisconnectedSpace G₂]

257 (hfg₁ : FiniteGeneration.TopologicallyFinitelyGenerated G₁)

258 (hfg₂ : FiniteGeneration.TopologicallyFinitelyGenerated G₂)

259 (hquot : HasSameContinuousFiniteDiscreteQuotients G₁ G₂) :

260 Nonempty (G₁ ≃ₜ* G₂) := by

261 classical

262 rcases

263 exists_surj_continuousMonoidHom_between_profiniteGroups_of_sameContinuousFiniteDiscreteQuotients

264 (G₁ := G₁) (G₂ := G₂) hfg₁ hquot with ⟨φ, hφsurj⟩

265 have hquot_symm : HasSameContinuousFiniteDiscreteQuotients G₂ G₁ := by

266 intro Q _ _ _ _ _

267 exact (hquot Q).symm

268 rcases

269 exists_surj_continuousMonoidHom_between_profiniteGroups_of_sameContinuousFiniteDiscreteQuotients

270 (G₁ := G₂) (G₂ := G₁) hfg₂ hquot_symm with ⟨ψ, hψsurj⟩

271 let ψφ : ContinuousMonoidHom G₁ G₁ := ψ.comp φ

272 have hψφsurj : Function.Surjective ψφ := by

273 simpa [ψφ] using hψsurj.comp hφsurj

274 rcases

275 (FiniteGeneration.surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated

276 (G := G₁) hfg₁ ψφ hψφsurj) with ⟨e, he⟩

277 have hψφinj : Function.Injective ψφ := by

278 intro x y hxy

279 apply e.injective

280 calc

281 e x = ψφ x := he x

282 _ = ψφ y := hxy

283 _ = e y := (he y).symm

284 have hφinj : Function.Injective φ := by

285 intro x y hxy

286 apply hψφinj

287 change ψ (φ x) = ψ (φ y)

288 exact congrArg ψ hxy

289 exact ⟨ContinuousMulEquiv.ofBijectiveCompactToT2

290 φ.toMonoidHom φ.continuous_toFun ⟨hφinj, hφsurj⟩⟩

291

292

293end ProCGroups.Completion