Source: ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
1import ProCGroups.InverseSystems.ProfiniteSpace
2import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
3import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
4import ProCGroups.Topologies.ContinuousMulEquiv
5import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
7/-!
8# Presenting pro-\(C\) groups as inverse limits
10The canonical map to the inverse limit of all finite open-normal quotients is identified stage by
11stage and shown to be a multiplicative equivalence. An exact quotient-basis condition then yields
12the Hausdorff, totally disconnected, and pro-\(C\) structures.
13-/
15namespace ProCGroups.ProC
17universe u v
19variable {C : FiniteGroupClass.{u}}
20variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
22namespace HasOpenNormalBasisInClass
24/-! ## Compatibility with mathlib's finite-quotient presentation -/
26/-- On open normal subgroups whose quotient lies in \(C\), mathlib's finite-quotient
27functor uses the same transition maps as `openNormalSubgroupInClassSystem`. -/
28@[simp] theorem toFiniteQuotientFunctor_map_apply_openNormalSubgroupInClass
29 [CompactSpace G] [TotallyDisconnectedSpace G]
30 {U V : OpenNormalSubgroupInClass C G}
31 (hUV : U.1 ≤ V.1) (x : G ⧸ (U.1 : Subgroup G)) :
32 (ProfiniteGrp.toFiniteQuotientFunctor (ProfiniteGrp.of G)).map
33 (CategoryTheory.homOfLE hUV) x =
34 OpenNormalSubgroupInClass.map (C := C) (G := G) (U := V) (V := U)
35 (show (U.1 : Subgroup G) ≤ (V.1 : Subgroup G) from hUV) x := by
36 rfl
38/-- The coordinate of mathlib's canonical `ProfiniteGrp.toLimit` map at an in-class open
39normal subgroup is the quotient projection used by `openNormalSubgroupInClassSystem`.
41We state this through the explicit `.val` coordinate of `ProfiniteGrp.limit`; this avoids choosing
42a second, potentially non-definitionally-equal `HasLimit` instance merely to name the projection. -/
43@[simp] theorem toLimit_val_openNormalSubgroupInClass
44 [CompactSpace G] [TotallyDisconnectedSpace G]
45 (U : OpenNormalSubgroupInClass C G) (g : G) :
46 (ProfiniteGrp.toLimit (ProfiniteGrp.of G) g).val U.1 =
47 openNormalSubgroupInClassProj (C := C) (G := G) (OrderDual.toDual U) g := by
48 rfl
50/--
51A pro-\(C\) group is canonically the inverse limit of its quotients by open normal subgroups
52whose quotients lie in \(C\).
53-/
54noncomputable def openNormalSubgroupInClassMulEquivInverseLimit
55 [CompactSpace G] [T2Space G]
56 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
57 G ≃ₜ* (openNormalSubgroupInClassSystem C G).inverseLimit := by
58 let S := openNormalSubgroupInClassSystem C G
59 letI : Nonempty (OpenNormalSubgroupInClass C G) := openNormalSubgroupInClass_nonempty hG
60 letI : Nonempty (OrderDual (OpenNormalSubgroupInClass C G)) := inferInstance
61 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Group (S.X U) := fun U =>
62 instGroupOpenNormalSubgroupInClassSystemX (C := C) (G := G) U
63 letI : InverseSystems.IsGroupSystem S := by
64 dsimp [S]
65 infer_instance
66 letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), T2Space (S.X U) := fun U => by
67 letI : DiscreteTopology (S.X U) := by
68 dsimp [S, openNormalSubgroupInClassSystem]
69 exact QuotientGroup.discreteTopology
70 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
71 infer_instance
72 letI : Group S.inverseLimit := by infer_instance
73 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
74 let φ : G →* S.inverseLimit :=
75 { toFun := S.inverseLimitLift
76 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
77 openNormalSubgroupInClassProj (C := C) (G := G) U)
78 (openNormalSubgroupInClassProj_compatible (C := C) (G := G))
79 map_one' := by
80 apply S.ext
81 intro i
82 rfl
83 map_mul' := by
84 intro x y
85 apply S.ext
86 intro i
87 rfl }
88 have hφcont : Continuous φ :=
89 S.continuous_inverseLimitLift
90 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
91 openNormalSubgroupInClassProj (C := C) (G := G) U)
92 (fun _ => continuous_quotient_mk')
93 (openNormalSubgroupInClassProj_compatible (C := C) (G := G))
94 have hφinj : Function.Injective φ := by
95 intro x y hxy
96 have hmem :
97 x⁻¹ * y ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
98 rw [Subgroup.mem_iInf]
99 intro U
100 let i : OrderDual (OpenNormalSubgroupInClass C G) := OrderDual.toDual U
101 have hi :
102 openNormalSubgroupInClassProj (C := C) (G := G) i x =
103 openNormalSubgroupInClassProj (C := C) (G := G) i y := by
104 have hcoord :=
105 congrArg (fun z : S.inverseLimit => S.projection i z) hxy
106 change
107 openNormalSubgroupInClassProj (C := C) (G := G) i x =
108 openNormalSubgroupInClassProj (C := C) (G := G) i y at hcoord
109 exact hcoord
110 change
111 QuotientGroup.mk' (U.1 : Subgroup G) x =
112 QuotientGroup.mk' (U.1 : Subgroup G) y at hi
113 exact QuotientGroup.eq.1 hi
114 have hone : x⁻¹ * y = 1 := by
115 have : x⁻¹ * y ∈ (⊥ : Subgroup G) := by
116 simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hmem
117 simpa using this
118 calc
119 x = x * 1 := by simp only [mul_one]
120 _ = x * (x⁻¹ * y) := by rw [hone]
121 _ = y := by simp only [mul_inv_cancel_left]
122 have hφsurj : Function.Surjective φ :=
123 InverseSystems.InverseSystem.surjective_inverseLimitLift (S := S)
124 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
125 openNormalSubgroupInClassProj (C := C) (G := G) U)
126 (fun _ => continuous_quotient_mk')
127 (openNormalSubgroupInClassProj_compatible (C := C) (G := G))
128 (fun U => openNormalSubgroupInClassProj_surjective (C := C) (G := G) U)
129 (directed_openNormalSubgroupInClass (C := C) (G := G) hForm)
130 exact ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont ⟨hφinj, hφsurj⟩
132/--
133Under the canonical equivalence from a pro-\(C\) group to the inverse limit of its open-normal
134\(C\)-quotients, the \(U\)-coordinate of an element is its quotient class modulo \(U\).
135-/
136@[simp] theorem openNormalSubgroupInClassMulEquivInverseLimit_projection
137 [CompactSpace G] [T2Space G]
138 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
139 (U : OrderDual (OpenNormalSubgroupInClass C G)) (g : G) :
140 (openNormalSubgroupInClassSystem C G).projection U
141 (openNormalSubgroupInClassMulEquivInverseLimit
142 (C := C) (G := G) hForm hG g) =
143 openNormalSubgroupInClassProj (C := C) (G := G) U g := by
144 simp only [openNormalSubgroupInClassMulEquivInverseLimit,
145 ContinuousMulEquiv.ofBijectiveCompactToT2,
146 MonoidHom.coe_mk, OneHom.coe_mk, ContinuousMulEquiv.coe_mk',
147 Equiv.toHomeomorphOfContinuousClosed_apply,
148 Equiv.ofBijective_apply, InverseSystems.InverseSystem.inverseLimitLift,
149 InverseSystems.InverseSystem.projection_apply]
151/-- The concrete pro-\(C\) presentation and mathlib's finite-quotient presentation have
152identical canonical coordinates. The generic concrete/categorical-limit comparison is
153`InverseSystems.InverseSystem.profiniteGrpConeIsLimit`. -/
154theorem openNormalSubgroupInClassMulEquivInverseLimit_projection_eq_toLimit_val
155 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
156 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)
157 (U : OpenNormalSubgroupInClass C G) (g : G) :
158 (openNormalSubgroupInClassSystem C G).projection (OrderDual.toDual U)
159 (openNormalSubgroupInClassMulEquivInverseLimit
160 (C := C) (G := G) hForm hG g) =
161 (ProfiniteGrp.toLimit (ProfiniteGrp.of G) g).val U.1 := by
162 rw [openNormalSubgroupInClassMulEquivInverseLimit_projection,
163 toLimit_val_openNormalSubgroupInClass]
165/--
166A pro-\(C\) group is topologically isomorphic to an inverse limit of finite groups in \(C\),
167realized using the quotient system indexed by the open normal subgroups whose quotients lie in
168\(C\).
169-/
170theorem isomorphic_to_inverseLimit_finiteGroupsInClass
171 [CompactSpace G] [T2Space G]
172 (hForm : FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
173 let S := openNormalSubgroupInClassSystem C G
174 (∀ U : OrderDual (OpenNormalSubgroupInClass C G), C (S.X U) ∧ Finite (S.X U)) ∧
175 Nonempty (G ≃ₜ* S.inverseLimit) := by
176 let S := openNormalSubgroupInClassSystem C G
177 refine ⟨?_, ⟨openNormalSubgroupInClassMulEquivInverseLimit (C := C) (G := G) hForm hG⟩⟩
178 intro U
179 dsimp [S, openNormalSubgroupInClassSystem]
180 refine ⟨(OrderDual.ofDual U).2, ?_⟩
181 exact C.finite (OrderDual.ofDual U).2
183end HasOpenNormalBasisInClass
185/--
186Existence of an open-normal subgroup basis whose quotients lie in \(C\) and whose quotient
187presentations are exact.
188-/
189def HasExactOpenNormalQuotientBasisInClass (C : FiniteGroupClass.{u})
190 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
191 CompactSpace G ∧
192 ∃ ι : Type u, ∃ U : ι → OpenNormalSubgroup G,
193 (∀ i, C (G ⧸ (U i : Subgroup G))) ∧
194 (∀ W : Set G, IsOpen W → (1 : G) ∈ W →
195 ∃ i, (((U i : Subgroup G) : Set G)) ⊆ W) ∧
196 iInf (fun i => (U i : Subgroup G)) = (⊥ : Subgroup G)
198/-- An open-normal family with trivial intersection makes the group Hausdorff. -/
199theorem t2Space_of_exactOpenNormalQuotientBasisInClass
200 (hC : HasExactOpenNormalQuotientBasisInClass C G) : T2Space G := by
201 rcases hC with ⟨_, ι, U, _, _, hInf⟩
202 refine ⟨?_⟩
203 intro x y hxy
204 have hxy' : x⁻¹ * y ≠ 1 := by
205 intro h1
206 apply hxy
207 simpa using inv_mul_eq_one.mp h1
208 have hsep : ∃ i : ι, x⁻¹ * y ∉ (U i : Subgroup G) := by
209 by_contra hsep
210 have hxall : ∀ i : ι, x⁻¹ * y ∈ (U i : Subgroup G) := by
211 intro i
212 by_contra hxyi
213 exact hsep ⟨i, hxyi⟩
214 have hxinf : x⁻¹ * y ∈ iInf (fun i => (U i : Subgroup G)) := by
215 simpa [Subgroup.mem_iInf] using hxall
216 have hxbot : x⁻¹ * y ∈ (⊥ : Subgroup G) := by
217 simpa [hInf] using hxinf
218 exact hxy' (by simpa using hxbot)
219 rcases hsep with ⟨i, hxyi⟩
220 have hclopenCoset :
221 ∀ z : G, IsClopen {g : G | z⁻¹ * g ∈ (U i : Subgroup G)} := by
222 intro z
223 let f : G → G := fun g => z⁻¹ * g
224 have hf : Continuous f := continuous_const.mul continuous_id
225 refine ⟨?_, ?_⟩
226 · change IsClosed (f ⁻¹' ((U i).toOpenSubgroup : Set G))
227 exact (openSubgroup_isClosed (G := G) (U i).toOpenSubgroup).preimage hf
228 · change IsOpen (f ⁻¹' ((U i).toOpenSubgroup : Set G))
229 exact (openSubgroup_isOpen (G := G) (U i).toOpenSubgroup).preimage hf
230 refine ⟨{g : G | x⁻¹ * g ∈ (U i : Subgroup G)},
231 {g : G | y⁻¹ * g ∈ (U i : Subgroup G)}, ?_, ?_, ?_, ?_, ?_⟩
232 · exact (hclopenCoset x).2
233 · exact (hclopenCoset y).2
234 · simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem]
235 · simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem]
236 · refine Set.disjoint_left.2 ?_
237 intro g hx hg
238 apply hxyi
239 have hmul :
240 (x⁻¹ * g) * (y⁻¹ * g)⁻¹ ∈ (U i : Subgroup G) :=
241 (U i).mul_mem hx ((U i).inv_mem hg)
242 simpa [mul_assoc] using hmul
244/-- An open-normal family yields a clopen basis and total disconnectedness. -/
245theorem totallyDisconnectedSpace_of_exactOpenNormalQuotientBasisInClass
246 (hC : HasExactOpenNormalQuotientBasisInClass C G) : TotallyDisconnectedSpace G := by
247 have hC' := hC
248 rcases hC' with ⟨_, ι, U, _, hbasis, _⟩
249 letI : T2Space G := t2Space_of_exactOpenNormalQuotientBasisInClass (C := C) hC
250 have hclopenBasis : TopologicalSpace.IsTopologicalBasis {s : Set G | IsClopen s} := by
251 refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
252 · intro s hs
253 exact hs.2
254 · intro x W hxW hW
255 let W₁ : Set G := (fun g : G => x * g) ⁻¹' W
256 have hW₁ : IsOpen W₁ := hW.preimage (continuous_const.mul continuous_id)
257 have h1W₁ : (1 : G) ∈ W₁ := by
258 simpa [W₁] using hxW
259 rcases hbasis W₁ hW₁ h1W₁ with ⟨i, hi⟩
260 have hclopenCoset : IsClopen {g : G | x⁻¹ * g ∈ (U i : Subgroup G)} := by
261 let f : G → G := fun g => x⁻¹ * g
262 have hf : Continuous f := continuous_const.mul continuous_id
263 refine ⟨?_, ?_⟩
264 · change IsClosed (f ⁻¹' ((U i).toOpenSubgroup : Set G))
265 exact (openSubgroup_isClosed (G := G) (U i).toOpenSubgroup).preimage hf
266 · change IsOpen (f ⁻¹' ((U i).toOpenSubgroup : Set G))
267 exact (openSubgroup_isOpen (G := G) (U i).toOpenSubgroup).preimage hf
268 refine ⟨{g : G | x⁻¹ * g ∈ (U i : Subgroup G)}, ?_, by simp only
269 [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem], ?_⟩
270 · exact hclopenCoset
271 · intro g hg
272 have hxgW₁ : x⁻¹ * g ∈ W₁ := hi hg
273 simpa [W₁, mul_assoc] using hxgW₁
274 exact InverseSystems.totallyDisconnectedSpace_of_t2_basis_clopen G hclopenBasis
276omit [IsTopologicalGroup G] in
277/-- An exact open-normal quotient basis in \(C\) implies `HasOpenNormalBasisInClass C G`. This
278direction needs no formation closure because the chosen basis already supplies the required
279open-normal quotients in \(C\). -/
280theorem hasOpenNormalBasisInClass_of_hasExactOpenNormalQuotientBasisInClass
281 (hC : HasExactOpenNormalQuotientBasisInClass C G) : HasOpenNormalBasisInClass C G := by
282 rcases hC with ⟨_, ι, U, hCU, hbasis, _⟩
283 intro W hW h1W
284 rcases hbasis W hW h1W with ⟨i, hiW⟩
285 exact ⟨U i, hiW, hCU i⟩
287end ProCGroups.ProC