Source: ProCGroups.ProC.InverseLimits.Limits
1import ProCGroups.InverseSystems.FiniteStageFactorization
2import ProCGroups.ProC.InverseLimits.FiniteQuotients
3import ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies
4import ProCGroups.Topologies.ContinuousMulEquiv
6/-!
7# Inverse limits and closed-normal quotients
9This file equips inverse limits of finite topological group systems with their canonical topology
10and proves the pro-\(C\) basis property for the resulting limits and for quotients by closed
11normal subgroups.
12-/
14open Set
15open scoped Topology Pointwise
17namespace ProCGroups.ProC
19universe u v
21open InverseSystems
23section
25variable {C : FiniteGroupClass.{u}}
26variable {I : Type u} [Preorder I] [Nonempty I]
27variable (S : InverseSystems.InverseSystem (I := I))
28/--
29The constructed object carries the topological space structure inherited from its construction.
30-/
31instance instTopologicalSpaceX (i : I) : TopologicalSpace (S.X i) := S.topologicalSpace i
32variable [∀ i, Group (S.X i)]
33variable [∀ i, IsTopologicalGroup (S.X i)]
34variable [InverseSystems.IsGroupSystem S]
36/-- A directed inverse limit of pro-\(C\) groups is pro-\(C\). -/
37theorem inverseLimit
38 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
39 [∀ i, TotallyDisconnectedSpace (S.X i)]
40 (hIso : FiniteGroupClass.IsomClosed C)
41 (hQuot : FiniteGroupClass.QuotientClosed C)
42 (hdir : Directed (· ≤ ·) (id : I → I))
43 (hX : ∀ i, HasOpenNormalBasisInClass C (S.X i)) :
44 HasOpenNormalBasisInClass C S.inverseLimit := by
45 letI : T2Space S.inverseLimit :=
46 InverseSystems.InverseSystem.t2Space_inverseLimit (S := S)
47 letI : TotallyDisconnectedSpace S.inverseLimit :=
48 InverseSystems.InverseSystem.totallyDisconnectedSpace_inverseLimit (S := S)
49 refine HasOpenNormalBasisInClass.of_allOpenNormalQuotients (C := C) ?_
50 intro U
51 letI : CompactSpace S.inverseLimit := inferInstance
52 letI : Finite (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
53 openNormalSubgroup_finiteQuotient (G := S.inverseLimit) U
54 letI : DiscreteTopology (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
55 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := S.inverseLimit) U)
56 let β : S.inverseLimit →* S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) :=
57 QuotientGroup.mk' (U : Subgroup S.inverseLimit)
58 rcases InverseSystems.InverseSystem.factors_through_projection_finite_group_hom
59 (S := S) hdir β continuous_quotient_mk' with ⟨k, βk, hβk_continuous, hβfac⟩
60 have hβk_surj : Function.Surjective βk := by
61 intro q
62 rcases QuotientGroup.mk'_surjective (U : Subgroup S.inverseLimit) q with ⟨x, rfl⟩
63 refine ⟨S.projection k x, ?_⟩
64 change βk (S.projection k x) = β x
65 exact
66 (congrArg
67 (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) => f x)
68 hβfac).symm
69 have hker_closed : IsClosed ((βk.ker : Subgroup (S.X k)) : Set (S.X k)) := by
70 change IsClosed {y : S.X k | βk y = 1}
71 exact isClosed_eq hβk_continuous continuous_const
72 have hker_finite : Finite (S.X k ⧸ βk.ker) := by
73 exact Finite.of_injective (QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj)
74 (QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj).injective
75 have hker_open : IsOpen ((βk.ker : Subgroup (S.X k)) : Set (S.X k)) :=
76 (subgroup_isOpen_iff_isClosed_finite_quotient (G := S.X k) (U := βk.ker)).2
77 ⟨hker_closed, hker_finite⟩
78 let V : OpenNormalSubgroup (S.X k) :=
79 { toOpenSubgroup := ⟨βk.ker, hker_open⟩
80 isNormal' := inferInstance }
81 have hQV : C (S.X k ⧸ (V : Subgroup (S.X k))) :=
82 HasOpenNormalBasisInClass.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
83 hIso hQuot (hX k) V
84 exact hIso ⟨QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj⟩ hQV
86variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
88/--
89If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by a
90closed normal subgroup is again pro-\(C\).
91-/
92theorem quotient_closedNormalSubgroup
93 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
94 (hIso : FiniteGroupClass.IsomClosed C)
95 (hQuot : FiniteGroupClass.QuotientClosed C)
96 (hG : HasOpenNormalBasisInClass C G)
97 (K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
98 HasOpenNormalBasisInClass C (G ⧸ K) := by
99 classical
100 let topU : OpenNormalSubgroup G :=
101 { toOpenSubgroup := ⟨⊤, isOpen_univ⟩
102 isNormal' := inferInstance }
103 letI : Nonempty (OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) :=
104 ⟨OrderDual.toDual ⟨topU, le_top⟩⟩
105 let S : InverseSystems.InverseSystem
106 (I := OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) := {
107 X := fun U => G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
108 topologicalSpace := fun _ => inferInstance
109 map := fun {U V} hUV =>
110 QuotientGroup.map
111 (((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G)
112 (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
113 (MonoidHom.id G)
114 hUV
115 continuous_map := by
116 intro U V hUV
117 letI : DiscreteTopology
118 (G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) :=
119 QuotientGroup.discreteTopology
120 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
121 exact continuous_of_discreteTopology
122 map_id := by
123 intro U
124 simp only [QuotientGroup.map_id, MonoidHom.coe_id]
125 map_comp := by
126 intro U V W hUV hVW
127 funext x
128 simpa [Function.comp] using congrArg (fun f => f x)
129 (QuotientGroup.map_comp_map
130 (N := (((OrderDual.ofDual W).1 : OpenNormalSubgroup G) : Subgroup G))
131 (M := (((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G))
132 (O := (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
133 (f := MonoidHom.id G) (g := MonoidHom.id G) hVW hUV) }
134 letI : InverseSystems.IsGroupSystem S := {
135 map_one := by
136 intro i j hij
137 rfl
138 map_mul := by
139 intro i j hij x y
140 change
141 QuotientGroup.map
142 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
143 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
144 (MonoidHom.id G) hij (x * y) =
145 QuotientGroup.map
146 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
147 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
148 (MonoidHom.id G) hij x *
149 QuotientGroup.map
150 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
151 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
152 (MonoidHom.id G) hij y
153 exact
154 (QuotientGroup.map
155 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
156 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
157 (MonoidHom.id G) hij).map_mul x y
158 map_inv := by
159 intro i j hij x
160 change
161 QuotientGroup.map
162 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
163 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
164 (MonoidHom.id G) hij x⁻¹ =
165 (QuotientGroup.map
166 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
167 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
168 (MonoidHom.id G) hij x)⁻¹
169 exact
170 (QuotientGroup.map
171 ((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
172 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
173 (MonoidHom.id G) hij).map_inv x }
174 have hdir :
175 Directed (· ≤ ·) (id : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)} →
176 OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) := by
177 intro i j
178 refine ⟨OrderDual.toDual ⟨(OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1, ?_⟩, ?_, ?_⟩
179 · intro x hx
180 exact ⟨(OrderDual.ofDual i).2 hx, (OrderDual.ofDual j).2 hx⟩
181 · exact show
182 (((OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G) ≤
183 ((OrderDual.ofDual i).1 : Subgroup G) from inf_le_left
184 · exact show
185 (((OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G) ≤
186 ((OrderDual.ofDual j).1 : Subgroup G) from inf_le_right
187 have hX :
188 ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
189 HasOpenNormalBasisInClass C (S.X i) :=
190 by
191 intro i
192 let U : OpenNormalSubgroup G := (OrderDual.ofDual i).1
193 letI : Finite (G ⧸ (U : Subgroup G)) :=
194 openNormalSubgroup_finiteQuotient (G := G) U
195 letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
196 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
197 exact HasOpenNormalBasisInClass.of_finite_discrete (C := C) (G := G ⧸ (U : Subgroup G))
198 hQuot
199 (HasOpenNormalBasisInClass.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
200 hIso hQuot hG U)
201 letI : ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
202 Finite (S.X i) := fun i => by
203 dsimp [S]
204 exact openNormalSubgroup_finiteQuotient (G := G) (OrderDual.ofDual i).1
205 letI : ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
206 DiscreteTopology (S.X i) := fun i => by
207 dsimp [S]
208 exact QuotientGroup.discreteTopology
209 (openNormalSubgroup_isOpen (G := G) (OrderDual.ofDual i).1)
210 letI : ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
211 CompactSpace (S.X i) := fun _ => by infer_instance
212 letI : ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
213 T2Space (S.X i) := fun _ => by infer_instance
214 letI : ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
215 TotallyDisconnectedSpace (S.X i) := fun _ => by infer_instance
216 have hSinv : HasOpenNormalBasisInClass C S.inverseLimit :=
217 inverseLimit (C := C) (S := S) hIso hQuot hdir hX
218 let ψ :
219 ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
220 G ⧸ K → S.X i := fun i =>
221 QuotientGroup.map
222 K
223 (((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)
224 (MonoidHom.id G)
225 (OrderDual.ofDual i).2
226 have hψcont :
227 ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}, Continuous (ψ i) := by
228 intro i
229 let U : Subgroup G := (((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)
230 have hmk : Continuous (QuotientGroup.mk' U : G → G ⧸ U) := continuous_quotient_mk'
231 have hconst :
232 ∀ a b : G, QuotientGroup.leftRel K a b →
233 (QuotientGroup.mk' U) a = (QuotientGroup.mk' U) b := by
234 intro a b hab
235 apply QuotientGroup.eq.2
236 exact (OrderDual.ofDual i).2 (by simpa using (QuotientGroup.leftRel_apply.mp hab))
237 refine (QuotientGroup.isQuotientMap_mk K).continuous_iff.2 ?_
238 change Continuous fun g : G => QuotientGroup.mk' U g
239 exact hmk
240 have hψcompat : S.CompatibleMaps ψ := by
241 intro i j hij
242 funext x
243 rcases QuotientGroup.mk'_surjective K x with ⟨g, rfl⟩
244 rfl
245 let φ : G ⧸ K →* S.inverseLimit := {
246 toFun := S.inverseLimitLift ψ hψcompat
247 map_one' := by
248 apply S.ext
249 intro i
250 rfl
251 map_mul' := by
252 intro x y
253 apply S.ext
254 intro i
255 rcases QuotientGroup.mk'_surjective K x with ⟨gx, rfl⟩
256 rcases QuotientGroup.mk'_surjective K y with ⟨gy, rfl⟩
257 rfl }
258 have hφcont : Continuous φ := S.continuous_inverseLimitLift ψ hψcont hψcompat
259 have hφsurj : Function.Surjective φ := by
260 letI : CompactSpace (G ⧸ K) := by
261 infer_instance
262 letI : T2Space (G ⧸ K) := by
263 letI : IsClosed (K : Set G) := hK
264 infer_instance
265 exact InverseSystems.InverseSystem.surjective_inverseLimitLift
266 (S := S) ψ hψcont hψcompat
267 (fun i => by
268 intro x
269 rcases QuotientGroup.mk'_surjective
270 ((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)) x with ⟨g, rfl⟩
271 exact ⟨QuotientGroup.mk' K g, rfl⟩)
272 hdir
273 have hφinj : Function.Injective φ := by
274 intro x y hxy
275 rcases QuotientGroup.mk'_surjective K x with ⟨gx, rfl⟩
276 rcases QuotientGroup.mk'_surjective K y with ⟨gy, rfl⟩
277 apply QuotientGroup.eq.2
278 have hmem :
279 ∀ U : OpenNormalSubgroup G, K ≤ (U : Subgroup G) → gx⁻¹ * gy ∈ (U : Subgroup G) := by
280 intro U hKU
281 let i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)} :=
282 OrderDual.toDual ⟨U, hKU⟩
283 have hi : ψ i (QuotientGroup.mk' K gx) = ψ i (QuotientGroup.mk' K gy) := by
284 have hcoord := congrArg (fun z : S.inverseLimit => S.projection i z) hxy
285 change ψ i (QuotientGroup.mk' K gx) = ψ i (QuotientGroup.mk' K gy) at hcoord
286 exact hcoord
287 exact QuotientGroup.eq.mp hi
288 let HC : ClosedSubgroup G := { toSubgroup := K, isClosed' := hK }
289 have hx :
290 gx⁻¹ * gy ∈
291 sInf {N : Subgroup G | IsOpen (N : Set G) ∧ K ≤ N ∧ N.Normal} := by
292 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
293 intro N hN
294 let U : OpenNormalSubgroup G :=
295 { toOpenSubgroup := ⟨N, hN.1⟩
296 isNormal' := hN.2.2 }
297 exact hmem U hN.2.1
298 have hxK : gx⁻¹ * gy ∈ K := by
299 have hEq :
300 (K : Subgroup G) =
301 sInf {N : Subgroup G | IsOpen (N : Set G) ∧ K ≤ N ∧ N.Normal} :=
302 closedSubgroup_eq_sInf_openNormal (G := G) HC
303 exact hEq.symm ▸ hx
304 exact hxK
305 letI : CompactSpace (G ⧸ K) := by
306 infer_instance
307 letI : T2Space S.inverseLimit :=
308 InverseSystems.InverseSystem.t2Space_inverseLimit (S := S)
309 let e : G ⧸ K ≃ₜ* S.inverseLimit :=
310 ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont ⟨hφinj, hφsurj⟩
311 simpa using HasOpenNormalBasisInClass.ofContinuousMulEquiv (C := C) hSinv e.symm
313end
315end ProCGroups.ProC