Yamaguchi Lean 4 Library
Source: ProCGroups.Order.Basic
ProCGroups/Order/Basic/Source

Source: ProCGroups.Order.Basic

1import ProCGroups.InverseSystems.FiniteStageFactorization
2import ProCGroups.ProC.OpenNormalSubgroups.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies
4import ProCGroups.Profinite.Basic
6/-!
7# The order structure on closed subgroups
9This module equips closed subgroups with basic lattice operations, develops continuous images and
10preimages, and relates order-theoretic constructions to finite quotients of profinite groups.
11-/
13open Set
14open scoped Topology Pointwise BigOperators
16namespace ProCGroups.Order
18universe u v w
20open ProCGroups.InverseSystems
21open ProCGroups.ProC
23namespace ClosedSubgroup
25variable {G : Type u} [Group G] [TopologicalSpace G]
26variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
28/-- Closed subgroups have a top element: the whole group. -/
29instance instTopClosedSubgroup : Top (ClosedSubgroup G) :=
30 ⟨{ toSubgroup := ⊤, isClosed' := isClosed_univ }⟩
32/--
33Closed subgroups have a bottom element: the trivial subgroup, closed in a \(T_1\) topological
34group.
35-/
36instance instBotClosedSubgroup [T1Space G] : Bot (ClosedSubgroup G) :=
37 ⟨{ toSubgroup := ⊥
38 isClosed' := by
39 change IsClosed ({(1 : G)} : Set G)
40 exact isClosed_singleton }⟩
42/--
43The image of a closed subgroup under a continuous homomorphism from a compact domain into a
44Hausdorff codomain.
45-/
46noncomputable def map [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
47 (φ : G →* K) (hφ : Continuous φ) : ClosedSubgroup K where
48 toSubgroup := (H : Subgroup G).map φ
49 isClosed' := by
50 let f : H → K := fun x => φ x
51 have hcont : Continuous f := hφ.comp continuous_subtype_val
52 have hcompact : IsCompact (Set.range f) := isCompact_range hcont
53 have hEq : Set.range f = ((H : Subgroup G).map φ : Set K) := by
54 ext y
55 constructor
56 · rintro ⟨x, rfl⟩
57 exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
58 · intro hy
59 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
60 exact ⟨⟨x, hx⟩, rfl⟩
61 change IsClosed (((H : Subgroup G).map φ : Subgroup K) : Set K)
62 rw [← hEq]
63 exact hcompact.isClosed
65omit [IsTopologicalGroup K] in
66/-- The underlying subgroup of the image closed subgroup is the image of the underlying subgroup. -/
67@[simp, norm_cast]
68theorem toSubgroup_map [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
69 (φ : G →* K) (hφ : Continuous φ) :
70 ((map H φ hφ : ClosedSubgroup K) : Subgroup K) = (H : Subgroup G).map φ :=
71 rfl
73omit [IsTopologicalGroup K] in
74/-- Membership in the image closed subgroup is membership in the subgroup map. -/
75theorem mem_map [CompactSpace G] [T2Space K] {H : ClosedSubgroup G}
76 {φ : G →* K} (hφ : Continuous φ) {y : K} :
77 y ∈ map H φ hφ ↔ ∃ x ∈ (H : Subgroup G), φ x = y := by
78 rfl
80/-- Mapping a closed subgroup along the identity homomorphism gives the same closed subgroup. -/
81@[simp]
82theorem map_id [CompactSpace G] [T2Space G] (H : ClosedSubgroup G) :
83 map H (MonoidHom.id G) continuous_id = H := by
84 apply ClosedSubgroup.toSubgroup_injective
85 ext x
86 constructor
87 · rintro ⟨y, hy, rfl⟩
88 exact hy
89 · intro hx
90 exact ⟨x, hx, rfl⟩
92omit [IsTopologicalGroup K] in
93/-- Images of closed subgroups compose under composition of continuous homomorphisms. -/
94theorem map_comp
95 {L : Type w} [Group L] [TopologicalSpace L]
96 [CompactSpace G] [T2Space K] [CompactSpace K] [T2Space L]
97 (H : ClosedSubgroup G) (φ : G →* K) (hφ : Continuous φ)
98 (ψ : K →* L) (hψ : Continuous ψ) :
99 map (map H φ hφ) ψ hψ = map H (ψ.comp φ) (hψ.comp hφ) := by
100 apply ClosedSubgroup.toSubgroup_injective
101 ext z
102 constructor
103 · rintro ⟨y, hy, rfl⟩
104 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
105 exact ⟨x, hx, rfl⟩
106 · rintro ⟨x, hx, rfl⟩
107 exact ⟨φ x, (Subgroup.mem_map).2 ⟨x, hx, rfl⟩, rfl⟩
109omit [IsTopologicalGroup K] in
110/-- The image construction on closed subgroups is monotone. -/
111theorem map_mono [CompactSpace G] [T2Space K] {H H' : ClosedSubgroup G}
112 (hHH' : (H : Subgroup G) ≤ (H' : Subgroup G))
113 (φ : G →* K) (hφ : Continuous φ) :
114 ((map H φ hφ : ClosedSubgroup K) : Subgroup K) ≤
115 ((map H' φ hφ : ClosedSubgroup K) : Subgroup K) :=
116 Subgroup.map_mono hHH'
118omit [IsTopologicalGroup K] in
119/-- The image of the bottom closed subgroup is the bottom closed subgroup. -/
120@[simp]
121theorem map_bot [CompactSpace G] [T1Space G] [T2Space K]
122 (φ : G →* K) (hφ : Continuous φ) :
123 map (⊥ : ClosedSubgroup G) φ hφ = (⊥ : ClosedSubgroup K) := by
124 apply ClosedSubgroup.toSubgroup_injective
125 ext y
126 constructor
127 · rintro ⟨x, hx, rfl⟩
128 change x ∈ (⊥ : Subgroup G) at hx
129 change φ x ∈ (⊥ : Subgroup K)
130 rw [Subgroup.mem_bot] at hx ⊢
131 simp [hx]
132 · intro hy
133 change y ∈ (⊥ : Subgroup K) at hy
134 refine ⟨1, by simp only [SetLike.mem_coe, one_mem], ?_⟩
135 rw [Subgroup.mem_bot] at hy
136 simp [hy]
138omit [IsTopologicalGroup K] in
139/-- The image of the top closed subgroup under a surjective homomorphism is top. -/
140theorem map_eq_top_of_surjective [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
141 (φ : G →* K) (hφ : Continuous φ)
142 (hφH : ∀ y : K, ∃ x ∈ (H : Subgroup G), φ x = y) :
143 map H φ hφ = (⊤ : ClosedSubgroup K) := by
144 apply ClosedSubgroup.toSubgroup_injective
145 ext y
146 constructor
147 · intro _
148 trivial
149 · intro _
150 exact hφH y
152omit [IsTopologicalGroup K] in
153/-- Image containment for closed subgroups is equivalent to containment in the comap. -/
154theorem map_le_iff_le_comap [CompactSpace G] [T2Space K]
155 {H : ClosedSubgroup G} {L : ClosedSubgroup K}
156 {φ : G →* K} (hφ : Continuous φ) :
157 ((map H φ hφ : ClosedSubgroup K) : Subgroup K) ≤ (L : Subgroup K) ↔
158 (H : Subgroup G) ≤ Subgroup.comap φ (L : Subgroup K) := by
159 constructor
160 · intro h x hx
161 exact h ((Subgroup.mem_map).2 ⟨x, hx, rfl⟩)
162 · intro h y hy
163 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
164 exact h hx
166end ClosedSubgroup
168/-- The surjectivity hypothesis for transition maps in a group-valued inverse system. -/
169def IsSurjectiveInverseSystem {I : Type v} [Preorder I]
171 ∀ ⦃i j : I⦄ (hij : i ≤ j), Function.Surjective (S.map hij)
173/-- The image of a closed subgroup under a projection from a group-valued inverse limit. -/
174noncomputable def inverseLimitProjectionImage
175 {I : Type v} [Preorder I]
177 [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
178 [∀ i, TopologicalSpace (S.X i)] [∀ i, T2Space (S.X i)]
179 [CompactSpace S.inverseLimit]
180 (H : ClosedSubgroup S.inverseLimit) (i : I) : ClosedSubgroup (S.X i) :=
181 let πi : S.inverseLimit →* S.X i := {
182 toFun := fun x => S.projection i x
183 map_one' := rfl
184 map_mul' := by
185 intro x y
186 rfl
187 }
188 have hπi : Continuous (fun x : S.inverseLimit => S.projection i x) := by
189 exact (continuous_apply i).comp continuous_subtype_val
190 ClosedSubgroup.map H πi hπi
192section FiniteQuotientImages
194variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
196/-- The image of a closed subgroup in an open-normal finite quotient. -/
197noncomputable def quotientImage [CompactSpace G] (H : ClosedSubgroup G)
198 (U : OpenNormalSubgroup G) : ClosedSubgroup (G ⧸ (U : Subgroup G)) :=
199 ClosedSubgroup.map H (QuotientGroup.mk' (U : Subgroup G)) continuous_quotient_mk'
201/-- The subgroup underlying a quotient image is the image of the closed subgroup in the quotient. -/
202@[simp, norm_cast]
203theorem toSubgroup_quotientImage [CompactSpace G] (H : ClosedSubgroup G)
204 (U : OpenNormalSubgroup G) :
205 ((quotientImage (G := G) H U : ClosedSubgroup (G ⧸ (U : Subgroup G))) :
206 Subgroup (G ⧸ (U : Subgroup G))) =
207 (H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G)) :=
208 rfl
210/-- Membership in a quotient image is membership in the image of the underlying closed subgroup. -/
211@[simp]
212theorem mem_quotientImage [CompactSpace G] {H : ClosedSubgroup G}
213 {U : OpenNormalSubgroup G} {y : G ⧸ (U : Subgroup G)} :
214 y ∈ quotientImage (G := G) H U ↔
215 ∃ x ∈ (H : Subgroup G), QuotientGroup.mk' (U : Subgroup G) x = y := by
216 rfl
218/--
219Membership in a closed subgroup of a profinite group can be checked after all open-normal finite
220quotients.
221-/
222theorem mem_closedSubgroup_iff_forall_quotientImage_mem
223 [CompactSpace G] [TotallyDisconnectedSpace G]
224 {H : ClosedSubgroup G} {x : G} :
225 x ∈ H ↔
226 ∀ U : OpenNormalSubgroup G,
227 OpenNormalSubgroup.quotientProj U x ∈
228 (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) := by
229 constructor
230 · intro hx U
231 exact (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
232 · intro hx
233 have hxOpen :
234 ∀ N : Subgroup G, IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N → x ∈ N := by
235 intro N hN
236 let V : OpenSubgroup G := ⟨N, hN.1⟩
237 rcases exists_openNormalSubgroup_mul_subset_openSubgroup (G := G) H V hN.2 with
238 ⟨U, hHU⟩
239 have hxImg :
240 QuotientGroup.mk' (U : Subgroup G) x ∈
241 (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) := by
242 have hxU := hx U
243 change QuotientGroup.mk' (U : Subgroup G) x ∈
244 (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) at hxU
245 exact hxU
246 have hxSup : x ∈ (H : Subgroup G) ⊔ (U : Subgroup G) := by
247 have hEq :
248 (H : Subgroup G) ⊔ (U : Subgroup G) =
249 Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
250 ((quotientImage (G := G) H U :
251 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
252 Subgroup (G ⧸ (U : Subgroup G))) := by
253 calc
254 (H : Subgroup G) ⊔ (U : Subgroup G) =
255 (H : Subgroup G) ⊔ (QuotientGroup.mk' (U : Subgroup G)).ker := by
256 rw [QuotientGroup.ker_mk']
257 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
258 (((H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))) :
259 Subgroup (G ⧸ (U : Subgroup G))) := by
260 rw [← Subgroup.comap_map_eq]
261 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
262 ((quotientImage (G := G) H U :
263 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
264 Subgroup (G ⧸ (U : Subgroup G))) := by
265 rfl
266 rw [hEq]
267 exact hxImg
268 rcases
269 (Subgroup.mem_sup_of_normal_right (s := (H : Subgroup G)) (t := (U : Subgroup G))).1
270 hxSup with
271 ⟨h, hhH, u, huU, hhu⟩
272 have hxV : x ∈ (V : Set G) := hHU ⟨h, hhH, u, huU, hhu⟩
273 change x ∈ N at hxV
274 exact hxV
275 have hxInf :
276 x ∈ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N} := by
277 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
278 intro N hN
279 exact hxOpen N hN
280 change x ∈ (H : Subgroup G)
281 exact (closedSubgroup_eq_sInf_open (G := G) H).symm ▸ hxInf
283/--
284Inclusion of closed subgroups of a profinite group can be checked on all open-normal finite
285quotients.
286-/
287theorem closedSubgroup_le_iff_forall_quotientImages_le
288 [CompactSpace G] [TotallyDisconnectedSpace G]
289 {H K : ClosedSubgroup G} :
290 (H : Subgroup G) ≤ (K : Subgroup G) ↔
291 ∀ U : OpenNormalSubgroup G,
292 (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) ≤
293 (quotientImage (G := G) K U : Subgroup (G ⧸ (U : Subgroup G))) := by
294 constructor
295 · intro hHK U y hy
296 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
297 exact (Subgroup.mem_map).2 ⟨x, hHK hx, rfl⟩
298 · intro hHK x hx
299 exact (mem_closedSubgroup_iff_forall_quotientImage_mem (G := G) (H := K)).2 (by
300 intro U
301 exact hHK U ((Subgroup.mem_map).2 ⟨x, hx, rfl⟩))
303/-- Two closed subgroups are equal if their images agree in every finite quotient. -/
304theorem closedSubgroup_eq_of_quotientImages_eq
305 [CompactSpace G] [TotallyDisconnectedSpace G]
306 {H K : ClosedSubgroup G}
307 (hHK : ∀ U : OpenNormalSubgroup G,
308 quotientImage (G := G) H U = quotientImage (G := G) K U) :
309 H = K := by
310 have hle :
311 ∀ {A B : ClosedSubgroup G},
312 (∀ U : OpenNormalSubgroup G,
313 quotientImage (G := G) A U = quotientImage (G := G) B U) →
314 (A : Subgroup G) ≤ B := by
315 intro A B hAB x hxA
316 have hxOpen :
317 ∀ N : Subgroup G, IsOpen (N : Set G) ∧ (B : Subgroup G) ≤ N → x ∈ N := by
318 intro N hN
319 let V : OpenSubgroup G := ⟨N, hN.1⟩
320 rcases exists_openNormalSubgroup_mul_subset_openSubgroup (G := G) B V hN.2 with
321 ⟨U, hBU⟩
322 have hxImgA :
323 QuotientGroup.mk' (U : Subgroup G) x ∈ (quotientImage (G := G) A U : Subgroup _) := by
324 exact (Subgroup.mem_map).2 ⟨x, hxA, rfl⟩
325 have hxImgB :
326 QuotientGroup.mk' (U : Subgroup G) x ∈ (quotientImage (G := G) B U : Subgroup _) := by
327 rw [← hAB U]
328 exact hxImgA
329 have hxSup : x ∈ (B : Subgroup G) ⊔ (U : Subgroup G) := by
330 have hEq :
331 (B : Subgroup G) ⊔ (U : Subgroup G) =
332 Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
333 ((quotientImage (G := G) B U :
334 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
335 Subgroup (G ⧸ (U : Subgroup G))) := by
336 calc
337 (B : Subgroup G) ⊔ (U : Subgroup G) =
338 (B : Subgroup G) ⊔ (QuotientGroup.mk' (U : Subgroup G)).ker := by
339 rw [QuotientGroup.ker_mk']
340 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
341 (((B : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))) :
342 Subgroup (G ⧸ (U : Subgroup G))) := by
343 rw [← Subgroup.comap_map_eq]
344 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
345 ((quotientImage (G := G) B U :
346 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
347 Subgroup (G ⧸ (U : Subgroup G))) := by
348 rfl
349 rw [hEq]
350 exact hxImgB
351 rcases
352 (Subgroup.mem_sup_of_normal_right (s := (B : Subgroup G)) (t := (U : Subgroup G))).1
353 hxSup with
354 ⟨b, hbB, u, huU, hbu⟩
355 have hxV : x ∈ (V : Set G) := hBU ⟨b, hbB, u, huU, hbu⟩
356 change x ∈ N at hxV
357 exact hxV
358 have hxB :
359 x ∈ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (B : Subgroup G) ≤ N} := by
360 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
361 intro N hN
362 exact hxOpen N hN
363 exact (closedSubgroup_eq_sInf_open (G := G) B).symm ▸ hxB
364 exact le_antisymm (hle hHK) (hle (fun U => (hHK U).symm))
366end FiniteQuotientImages
368variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
370section CompatibleClosedSubgroupFamilies
373variable {I : Type v} [Preorder I]
375variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
376variable [∀ i, IsTopologicalGroup (S.X i)]
377variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
379/-- The transition map of a group-valued inverse system, viewed as a homomorphism. -/
380def inverseSystemStageHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
381 toFun := S.map hij
382 map_one' := ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
383 map_mul' := ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij
385omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)]
386 [∀ i, T2Space (S.X i)] in
387/-- The stage homomorphism associated to a group-valued inverse system is continuous. -/
388theorem inverseSystemStageHom_continuous {i j : I} (hij : i ≤ j) :
389 Continuous (inverseSystemStageHom (S := S) hij) := by
390 simpa [inverseSystemStageHom] using (S.continuous_map hij :
391 Continuous (fun x : S.X j => S.map hij x))
393/--
394The inverse system obtained by restricting an ambient inverse system to a compatible family of
395closed subgroups.
396-/
397def compatibleClosedSubgroupSystem
398 (L : ∀ i, ClosedSubgroup (S.X i))
399 (hcompat : ∀ {i j : I} (hij : i ≤ j),
400 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
401 (inverseSystemStageHom_continuous (S := S) hij) :
402 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
403 (L i : Subgroup (S.X i))) :
405 X := fun i => L i
406 topologicalSpace := fun i => inferInstance
407 map := fun {i j} hij x =>
408 ⟨S.map hij x.1, by
409 have hx :
410 S.map hij x.1 ∈
411 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
412 (inverseSystemStageHom_continuous (S := S) hij) :
413 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
414 exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
415 rw [hcompat hij] at hx
416 exact hx⟩
417 continuous_map := fun {i j} hij =>
418 Continuous.subtype_mk
419 ((inverseSystemStageHom_continuous (S := S) hij).comp continuous_subtype_val) (fun x => by
420 have hx :
421 S.map hij x.1 ∈
422 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
423 (inverseSystemStageHom_continuous (S := S) hij) :
424 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
425 exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
426 rw [hcompat hij] at hx
427 exact hx)
428 map_id := fun i => by
429 funext x
430 apply Subtype.ext
431 simp only [InverseSystem.map_id_apply, id_eq]
432 map_comp := fun {i j k} hij hjk => by
433 funext x
434 apply Subtype.ext
435 simp only [Function.comp_apply, InverseSystem.map_comp_apply]
437/-- Each stage of a compatible closed-subgroup system is a group. -/
438instance compatibleClosedSubgroupSystem_group
439 (L : ∀ i, ClosedSubgroup (S.X i))
440 (hcompat : ∀ {i j : I} (hij : i ≤ j),
441 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
442 (inverseSystemStageHom_continuous (S := S) hij) :
443 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
444 (L i : Subgroup (S.X i)))
445 (i : I) :
446 Group ((compatibleClosedSubgroupSystem (S := S) L hcompat).X i) := by
447 dsimp [compatibleClosedSubgroupSystem]
448 infer_instance
450/-- A compatible closed-subgroup system is a group-valued inverse system. -/
451instance compatibleClosedSubgroupSystem_isGroupSystem
452 (L : ∀ i, ClosedSubgroup (S.X i))
453 (hcompat : ∀ {i j : I} (hij : i ≤ j),
454 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
455 (inverseSystemStageHom_continuous (S := S) hij) :
456 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
457 (L i : Subgroup (S.X i))) :
458 ProCGroups.InverseSystems.IsGroupSystem (compatibleClosedSubgroupSystem (S := S) L hcompat)
459 where
460 map_one := by
461 intro i j hij
462 apply Subtype.ext
463 change S.map hij (1 : S.X j) = 1
464 exact ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
465 map_mul := by
466 intro i j hij x y
467 apply Subtype.ext
468 change S.map hij (x.1 * y.1) = S.map hij x.1 * S.map hij y.1
469 exact ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij x.1 y.1
470 map_inv := by
471 intro i j hij x
472 apply Subtype.ext
473 change S.map hij x.1⁻¹ = (S.map hij x.1)⁻¹
474 exact ProCGroups.InverseSystems.IsGroupSystem.map_inv (S := S) hij x.1
476/--
477The canonical coordinatewise inclusion of a compatible subgroup system into the ambient system.
478-/
479def compatibleClosedSubgroupInclusion
480 (L : ∀ i, ClosedSubgroup (S.X i))
481 (hcompat : ∀ {i j : I} (hij : i ≤ j),
482 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
483 (inverseSystemStageHom_continuous (S := S) hij) :
484 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
485 (L i : Subgroup (S.X i))) :
486 (compatibleClosedSubgroupSystem (S := S) L hcompat).Morphism S where
487 map := fun i => Subtype.val
488 continuous_map := fun i => by
489 dsimp [compatibleClosedSubgroupSystem]
490 exact continuous_subtype_val
491 comm := fun {i j} hij => by
492 funext x
493 rfl
495/--
496The induced homomorphism from the inverse limit of a compatible subgroup family into the ambient
497inverse limit.
498-/
499noncomputable def compatibleClosedSubgroupLimHom
500 (L : ∀ i, ClosedSubgroup (S.X i))
501 (hcompat : ∀ {i j : I} (hij : i ≤ j),
502 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
503 (inverseSystemStageHom_continuous (S := S) hij) :
504 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
505 (L i : Subgroup (S.X i))) :
506 (compatibleClosedSubgroupSystem (S := S) L hcompat).inverseLimit →* S.inverseLimit where
507 toFun :=
508 (compatibleClosedSubgroupSystem (S := S) L hcompat).limMap
509 (compatibleClosedSubgroupInclusion (S := S) L hcompat)
510 map_one' := by
511 apply S.ext
512 intro i
513 rfl
514 map_mul' := by
515 intro x y
516 apply S.ext
517 intro i
518 rfl
520/--
521Closed subgroup of the ambient inverse limit obtained from a compatible family of closed
522subgroups with surjective transition maps.
523-/
524noncomputable def closedSubgroupFromCompatibleFamily
525 (L : ∀ i, ClosedSubgroup (S.X i))
526 (hcompat : ∀ {i j : I} (hij : i ≤ j),
527 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
528 (inverseSystemStageHom_continuous (S := S) hij) :
529 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
530 (L i : Subgroup (S.X i))) :
531 ClosedSubgroup S.inverseLimit where
532 toSubgroup := (compatibleClosedSubgroupLimHom (S := S) L hcompat).range
533 isClosed' := by
534 let T := compatibleClosedSubgroupSystem (S := S) L hcompat
535 letI : ∀ i, CompactSpace (T.X i) := fun i => by
536 change CompactSpace (L i)
537 exact (L i).isClosed'.isClosedEmbedding_subtypeVal.compactSpace
538 letI : ∀ i, T2Space (T.X i) := fun i => by
539 change T2Space (L i)
540 infer_instance
541 letI : CompactSpace T.inverseLimit := inferInstance
542 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
543 let φ := compatibleClosedSubgroupLimHom (S := S) L hcompat
544 have hφcont :
545 Continuous (φ : T.inverseLimit → S.inverseLimit) := by
546 change Continuous (T.limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat))
547 exact T.continuous_limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat)
548 change IsClosed (Set.range (φ : T.inverseLimit → S.inverseLimit))
549 exact (isCompact_range hφcont).isClosed
551omit [∀ i, IsTopologicalGroup (S.X i)] in
552/--
553Projection images of a closed subgroup recovered from a compatible family match the given
554family.
555-/
556theorem inverseLimitProjectionImage_closedSubgroupFromCompatibleFamily
557 [CompactSpace S.inverseLimit]
558 (hdir : Directed (· ≤ ·) (id : I → I))
559 (L : ∀ i, ClosedSubgroup (S.X i))
560 (hcompat : ∀ {i j : I} (hij : i ≤ j),
561 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
562 (inverseSystemStageHom_continuous (S := S) hij) :
563 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
564 (L i : Subgroup (S.X i))) (i : I) :
565 inverseLimitProjectionImage S (closedSubgroupFromCompatibleFamily (S := S) L hcompat) i =
566 L i := by
567 let T := compatibleClosedSubgroupSystem (S := S) L hcompat
568 let incl := compatibleClosedSubgroupInclusion (S := S) L hcompat
569 let φ := compatibleClosedSubgroupLimHom (S := S) L hcompat
570 have hTsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (T.map hij) := by
571 intro i j hij y
572 have hy :
573 y.1 ∈
574 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
575 (inverseSystemStageHom_continuous (S := S) hij) :
576 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
577 exact (hcompat hij).symm ▸ (show y.1 ∈ (L i : Subgroup (S.X i)) from y.2)
578 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, hxy⟩
579 refine ⟨⟨x, hx⟩, ?_⟩
580 apply Subtype.ext
581 change S.map hij x = y.1
582 change S.map hij x = y.1 at hxy
583 exact hxy
584 letI : ∀ i, CompactSpace (T.X i) := fun i => by
585 change CompactSpace (L i)
586 exact (L i).isClosed'.isClosedEmbedding_subtypeVal.compactSpace
587 letI : ∀ i, T2Space (T.X i) := fun i => by
588 change T2Space (L i)
589 infer_instance
590 letI : CompactSpace T.inverseLimit := inferInstance
591 letI : T2Space T.inverseLimit := T.t2Space_inverseLimit
592 ext y
593 constructor
594 · intro hy
595 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, hxy⟩
596 rcases hx with ⟨z, rfl⟩
597 have hcoord :
598 S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) = (T.projection i z).1 := by
599 rfl
600 have hmem : (T.projection i z).1 ∈ (L i : Subgroup (S.X i)) := by
601 exact (T.projection i z).2
602 have hmem' : S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) ∈ (L i : Subgroup
603 (S.X i)) := by
604 exact hcoord ▸ hmem
605 exact hxy ▸ hmem'
606 · intro hy
607 have hπsurj : Function.Surjective (T.projection i) := T.surjective_π hdir hTsurj i
608 rcases hπsurj ⟨y, hy⟩ with ⟨z, hz⟩
609 refine (Subgroup.mem_map).2 ?_
610 refine ⟨φ z, ⟨z, rfl⟩, ?_⟩
611 have hcoord :
612 S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) = y := by
613 calc
614 S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) =
615 (T.projection i z).1 := by rfl
616 _ = y := congrArg Subtype.val hz
617 exact hcoord
619omit [∀ i, IsTopologicalGroup (S.X i)] in
620/--
621Projection images commute with mapping a closed subgroup along a compatible inverse-limit
622morphism.
623-/
624theorem map_inverseLimitProjectionImage
625 [CompactSpace S.inverseLimit]
626 (H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
627 ((ClosedSubgroup.map (inverseLimitProjectionImage S H j) (inverseSystemStageHom (S := S) hij)
628 (inverseSystemStageHom_continuous (S := S) hij) :
629 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
630 (inverseLimitProjectionImage S H i : Subgroup (S.X i)) := by
631 ext x
632 constructor
633 · intro hx
634 rcases (Subgroup.mem_map).1 hx with ⟨y, hy, hxy⟩
635 rcases (Subgroup.mem_map).1 hy with ⟨z, hz, hzy⟩
636 refine (Subgroup.mem_map).2 ⟨z, hz, ?_⟩
637 calc
638 S.projection i z = S.map hij (S.projection j z) := by
639 symm
640 simpa using z.2 i j hij
641 _ = S.map hij y := by simpa using congrArg (S.map hij) hzy
642 _ = x := hxy
643 · intro hx
644 rcases (Subgroup.mem_map).1 hx with ⟨z, hz, hzx⟩
645 refine (Subgroup.mem_map).2 ⟨S.projection j z, ?_, ?_⟩
646 · exact (Subgroup.mem_map).2 ⟨z, hz, rfl⟩
647 · calc
648 S.map hij (S.projection j z) = S.projection i z := by
649 simpa using z.2 i j hij
650 _ = x := hzx
652omit [∀ i, IsTopologicalGroup (S.X i)] in
653/--
654The stage-transition compatibility of projection images, repackaged as an equality of closed
655subgroups.
656-/
657theorem map_inverseLimitProjectionImage_closed
658 [CompactSpace S.inverseLimit]
659 (H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
660 ClosedSubgroup.map (inverseLimitProjectionImage S H j)
661 (inverseSystemStageHom (S := S) hij)
662 (inverseSystemStageHom_continuous (S := S) hij) =
663 inverseLimitProjectionImage S H i := by
664 ext x
665 simpa using congrArg (fun K : Subgroup (S.X i) => x ∈ K)
666 (map_inverseLimitProjectionImage (S := S) H hij)
668omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)] in
669/-- The projection image of the trivial closed subgroup is trivial. -/
670theorem inverseLimitProjectionImage_bot
671 [CompactSpace S.inverseLimit] (i : I) :
672 inverseLimitProjectionImage S (⊥ : ClosedSubgroup S.inverseLimit) i = ⊥ := by
673 ext x
674 constructor
675 · intro hx
676 rcases (Subgroup.mem_map).1 hx with ⟨y, hy, hyx⟩
677 change y ∈ (⊥ : Subgroup S.inverseLimit) at hy
678 have hy1 : y = 1 := (Subgroup.mem_bot).1 hy
679 cases hy1
680 change x ∈ (⊥ : Subgroup (S.X i))
681 rw [Subgroup.mem_bot]
682 calc
683 x = S.projection i (1 : S.inverseLimit) := hyx.symm
684 _ = 1 := projection_one (S := S) i
685 · intro hx
686 change x ∈ (⊥ : Subgroup (S.X i)) at hx
687 have hx1 : x = 1 := (Subgroup.mem_bot).1 hx
688 refine (Subgroup.mem_map).2 ⟨1, by simp only [one_mem], ?_⟩
689 rw [hx1]
690 rfl
692omit [∀ i, IsTopologicalGroup (S.X i)] in
693/--
694Under surjective transition maps, the projection image of the whole inverse limit is the whole
695stage group.
696-/
697theorem inverseLimitProjectionImage_top
698 [CompactSpace S.inverseLimit]
699 (hdir : Directed (· ≤ ·) (id : I → I))
700 (hsurj : IsSurjectiveInverseSystem S) (i : I) :
701 inverseLimitProjectionImage S (⊤ : ClosedSubgroup S.inverseLimit) i = ⊤ := by
702 ext x
703 constructor
704 · intro _
705 change x ∈ (⊤ : Subgroup (S.X i))
706 simp only [Subgroup.mem_top]
707 · intro _
708 have hπsurj : Function.Surjective (S.projection i) :=
709 S.surjective_π hdir (fun {i j} hij => hsurj hij) i
710 rcases hπsurj x with ⟨y, hy⟩
711 refine (Subgroup.mem_map).2 ⟨y, ?_, hy⟩
712 change y ∈ (⊤ : Subgroup S.inverseLimit)
713 simp only [Subgroup.mem_top]
715omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)] in
716/-- Projection images are monotone in the closed subgroup argument. -/
717theorem inverseLimitProjectionImage_mono
718 [CompactSpace S.inverseLimit]
719 {H K : ClosedSubgroup S.inverseLimit}
720 (hHK : (H : Subgroup S.inverseLimit) ≤ K) (i : I) :
721 (inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
722 (inverseLimitProjectionImage S K i : Subgroup (S.X i)) := by
723 intro x hx
724 rcases (Subgroup.mem_map).1 hx with ⟨y, hy, rfl⟩
725 exact (Subgroup.mem_map).2 ⟨y, hHK hy, rfl⟩
727/-- Closed subgroups of an inverse limit are determined by their stagewise projection images. -/
728theorem closedSubgroup_le_of_projectionImages_le
729 [Nonempty I] [CompactSpace S.inverseLimit]
730 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
731 [∀ i, TotallyDisconnectedSpace (S.X i)]
732 (hdir : Directed (· ≤ ·) (id : I → I))
733 (H K : ClosedSubgroup S.inverseLimit)
734 (hproj : ∀ i,
735 (inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
736 (inverseLimitProjectionImage S K i : Subgroup (S.X i))) :
737 (H : Subgroup S.inverseLimit) ≤ (K : Subgroup S.inverseLimit) := by
738 intro x hx
739 have hx' :
740 x ∈ sInf {N : Subgroup S.inverseLimit |
741 IsOpen (N : Set S.inverseLimit) ∧ (K : Subgroup S.inverseLimit) ≤ N} := by
742 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
743 intro N hN
744 let V : OpenSubgroup S.inverseLimit := ⟨N, hN.1⟩
745 rcases exists_openNormalSubgroup_mul_subset_openSubgroup (G := S.inverseLimit) K V hN.2 with
746 ⟨U, hKU⟩
747 letI : Finite (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
748 openNormalSubgroup_finiteQuotient (G := S.inverseLimit) U
749 letI : DiscreteTopology (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
750 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := S.inverseLimit) U)
751 let β : S.inverseLimit →* S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) :=
752 QuotientGroup.mk' (U : Subgroup S.inverseLimit)
754 (S := S) hdir β continuous_quotient_mk' with ⟨k, βk, hβkcont, hβfac⟩
755 have hxk : S.projection k x ∈ (inverseLimitProjectionImage S H k : Subgroup (S.X k)) := by
756 exact (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
757 have hxkK : S.projection k x ∈ (inverseLimitProjectionImage S K k : Subgroup (S.X k)) :=
758 hproj k hxk
759 rcases (Subgroup.mem_map).1 hxkK with ⟨z, hzK, hzxk⟩
760 have hβz : β z = βk (S.projection k z) := by
761 simpa [Function.comp] using
762 congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
763 f z) hβfac
764 have hβx : β x = βk (S.projection k x) := by
765 simpa [Function.comp] using
766 congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
767 f x) hβfac
768 have hzxu : z⁻¹ * x ∈ (U : Subgroup S.inverseLimit) := by
769 apply (QuotientGroup.eq_one_iff (N := (U : Subgroup S.inverseLimit)) (z⁻¹ * x)).1
770 have hβeq : β z = β x := by
771 calc
772 β z = βk (S.projection k z) := hβz
773 _ = βk (S.projection k x) := by simpa using congrArg βk hzxk
774 _ = β x := hβx.symm
775 calc
776 β (z⁻¹ * x) = (β z)⁻¹ * β x := by simp only [QuotientGroup.mk'_apply,
777 QuotientGroup.mk_mul, QuotientGroup.mk_inv, β]
778 _ = 1 := by simp only [hβeq, inv_mul_cancel]
779 have hxKU : x ∈ (((K : Subgroup S.inverseLimit) : Set S.inverseLimit) *
780 (((U : Subgroup S.inverseLimit) : Set S.inverseLimit))) := by
781 refine ⟨z, hzK, z⁻¹ * x, hzxu, ?_⟩
782 simp only [mul_inv_cancel_left]
783 exact hKU hxKU
784 exact (closedSubgroup_eq_sInf_open (G := S.inverseLimit) K).symm ▸ hx'
786/-- Stagewise equality of projection images determines a closed subgroup of an inverse limit. -/
787theorem closedSubgroup_eq_of_projectionImages_eq
788 [Nonempty I] [CompactSpace S.inverseLimit]
789 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
790 [∀ i, TotallyDisconnectedSpace (S.X i)]
791 (hdir : Directed (· ≤ ·) (id : I → I))
792 (H K : ClosedSubgroup S.inverseLimit)
793 (hproj : ∀ i, inverseLimitProjectionImage S H i = inverseLimitProjectionImage S K i) :
794 H = K := by
795 have hHK : (H : Subgroup S.inverseLimit) ≤ (K : Subgroup S.inverseLimit) :=
796 closedSubgroup_le_of_projectionImages_le (S := S) hdir H K (fun i => by
797 exact
798 le_of_eq <|
799 congrArg (fun (L : ClosedSubgroup (S.X i)) => (L : Subgroup (S.X i))) (hproj i))
800 have hKH : (K : Subgroup S.inverseLimit) ≤ (H : Subgroup S.inverseLimit) :=
801 closedSubgroup_le_of_projectionImages_le (S := S) hdir K H (fun i => by
802 exact
803 le_of_eq <|
804 congrArg (fun (L : ClosedSubgroup (S.X i)) => (L : Subgroup (S.X i))) (hproj i).symm)
805 apply SetLike.ext'
806 exact Set.ext fun x => ⟨fun hx => hHK hx, fun hx => hKH hx⟩
808/-- If every stagewise projection image is trivial, then the closed subgroup itself is trivial. -/
809theorem closedSubgroup_eq_bot_of_projectionImages_eq_bot
810 [Nonempty I] [CompactSpace S.inverseLimit]
811 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
812 [∀ i, TotallyDisconnectedSpace (S.X i)]
813 (hdir : Directed (· ≤ ·) (id : I → I))
814 (H : ClosedSubgroup S.inverseLimit)
815 (hproj : ∀ i, inverseLimitProjectionImage S H i = ⊥) :
816 H = ⊥ := by
817 apply closedSubgroup_eq_of_projectionImages_eq (S := S) hdir H ⊥
818 intro i
819 rw [hproj i, inverseLimitProjectionImage_bot (S := S) (i := i)]
821/--
822If every stagewise projection image is the whole stage group, then the closed subgroup itself is
823the whole inverse limit.
824-/
825theorem closedSubgroup_eq_top_of_projectionImages_eq_top
826 [Nonempty I] [CompactSpace S.inverseLimit]
827 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
828 [∀ i, TotallyDisconnectedSpace (S.X i)]
829 (hdir : Directed (· ≤ ·) (id : I → I))
830 (hsurj : IsSurjectiveInverseSystem S)
831 (H : ClosedSubgroup S.inverseLimit)
832 (hproj : ∀ i, inverseLimitProjectionImage S H i = ⊤) :
833 H = ⊤ := by
834 apply closedSubgroup_eq_of_projectionImages_eq (S := S) hdir H ⊤
835 intro i
836 rw [hproj i, inverseLimitProjectionImage_top (S := S) hdir hsurj i]
839end CompatibleClosedSubgroupFamilies
841end ProCGroups.Order