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

ProCGroups/Order/Basic.lean

1import ProCGroups.InverseSystems.FiniteStageFactorization
2import ProCGroups.ProC.OpenNormalSubgroups.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies
4import ProCGroups.Profinite.Basic
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/Order/Basic.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Order-theoretic infrastructure
17Order and lattice lemmas for subgroups, finite intersections, and inverse-system indexing.
18-/
20open Set
21open scoped Topology Pointwise BigOperators
23namespace ProCGroups.Order
25universe u v w
27open ProCGroups.InverseSystems
28open ProCGroups.ProC
30namespace ClosedSubgroup
32variable {G : Type u} [Group G] [TopologicalSpace G]
33variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
35/-- Closed subgroups have a top element. -/
36instance instTopClosedSubgroup : Top (ClosedSubgroup G) :=
37 ⟨{ toSubgroup := ⊤, isClosed' := isClosed_univ }⟩
39/-- Closed subgroups have a bottom element. -/
40instance instBotClosedSubgroup [T1Space G] : Bot (ClosedSubgroup G) :=
41 ⟨{ toSubgroup := ⊥
42 isClosed' := by
43 change IsClosed ({(1 : G)} : Set G)
44 exact isClosed_singleton }⟩
46/-- The image of a closed subgroup under a continuous homomorphism from a compact domain into a
47Hausdorff codomain. -/
48noncomputable def map [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
49 (φ : G →* K) (hφ : Continuous φ) : ClosedSubgroup K where
50 toSubgroup := (H : Subgroup G).map φ
51 isClosed' := by
52 let f : H → K := fun x => φ x
53 have hcont : Continuous f := hφ.comp continuous_subtype_val
54 have hcompact : IsCompact (Set.range f) := isCompact_range hcont
55 have hEq : Set.range f = ((H : Subgroup G).map φ : Set K) := by
56 ext y
57 constructor
58 · rintro ⟨x, rfl⟩
59 exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
60 · intro hy
61 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
62 exact ⟨⟨x, hx⟩, rfl⟩
63 simpa [hEq] using hcompact.isClosed
65omit [IsTopologicalGroup K] in
66/-- The underlying subgroup of the image closed subgroup is the subgroup map 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 bottom. -/
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 simpa using congrArg φ (show x = 1 from by simpa using hx)
129 · intro hy
130 refine ⟨1, by simp only [SetLike.mem_coe, one_mem], ?_⟩
131 simpa using (show y = 1 from by simpa using hy).symm
133omit [IsTopologicalGroup K] in
134/-- The image of the top closed subgroup under a surjective homomorphism is top. -/
135theorem map_eq_top_of_surjective [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
136 (φ : G →* K) (hφ : Continuous φ)
137 (hφH : ∀ y : K, ∃ x ∈ (H : Subgroup G), φ x = y) :
138 map H φ hφ = (⊤ : ClosedSubgroup K) := by
139 apply ClosedSubgroup.toSubgroup_injective
140 ext y
141 constructor
142 · intro _
143 trivial
144 · intro _
145 exact hφH y
147omit [IsTopologicalGroup K] in
148/-- Image containment for closed subgroups is equivalent to containment in the comap. -/
149theorem map_le_iff_le_comap [CompactSpace G] [T2Space K]
150 {H : ClosedSubgroup G} {L : ClosedSubgroup K}
151 {φ : G →* K} (hφ : Continuous φ) :
152 ((map H φ hφ : ClosedSubgroup K) : Subgroup K) ≤ (L : Subgroup K) ↔
153 (H : Subgroup G) ≤ Subgroup.comap φ (L : Subgroup K) := by
154 constructor
155 · intro h x hx
156 exact h ((Subgroup.mem_map).2 ⟨x, hx, rfl⟩)
157 · intro h y hy
158 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
159 exact h hx
161end ClosedSubgroup
163/-- The surjectivity hypothesis for transition maps in a group-valued inverse system. -/
164def IsSurjectiveInverseSystem {I : Type v} [Preorder I]
166 ∀ ⦃i j : I⦄ (hij : i ≤ j), Function.Surjective (S.map hij)
168/-- The image of a closed subgroup under a projection from a group-valued inverse limit. -/
170 {I : Type v} [Preorder I]
172 [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
173 [∀ i, TopologicalSpace (S.X i)] [∀ i, T2Space (S.X i)]
174 [CompactSpace S.inverseLimit]
175 (H : ClosedSubgroup S.inverseLimit) (i : I) : ClosedSubgroup (S.X i) :=
176 let πi : S.inverseLimit →* S.X i := {
177 toFun := fun x => S.projection i x
178 map_one' := rfl
179 map_mul' := by
180 intro x y
181 rfl
182 }
183 have hπi : Continuous (fun x : S.inverseLimit => S.projection i x) := by
184 exact (continuous_apply i).comp continuous_subtype_val
185 ClosedSubgroup.map H πi hπi
187section FiniteQuotientImages
189variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
191/-- The image of a closed subgroup in an open-normal finite quotient. -/
192noncomputable def quotientImage [CompactSpace G] (H : ClosedSubgroup G)
193 (U : OpenNormalSubgroup G) : ClosedSubgroup (G ⧸ (U : Subgroup G)) :=
194 ClosedSubgroup.map H (QuotientGroup.mk' (U : Subgroup G)) continuous_quotient_mk'
196/-- The subgroup underlying a quotient image is the image of the closed subgroup in the quotient. -/
197@[simp, norm_cast]
198theorem toSubgroup_quotientImage [CompactSpace G] (H : ClosedSubgroup G)
199 (U : OpenNormalSubgroup G) :
200 ((quotientImage (G := G) H U : ClosedSubgroup (G ⧸ (U : Subgroup G))) :
201 Subgroup (G ⧸ (U : Subgroup G))) =
202 (H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G)) :=
203 rfl
205/-- Membership in a quotient image is membership in the image of the underlying closed subgroup. -/
206@[simp]
207theorem mem_quotientImage [CompactSpace G] {H : ClosedSubgroup G}
208 {U : OpenNormalSubgroup G} {y : G ⧸ (U : Subgroup G)} :
209 y ∈ quotientImage (G := G) H U ↔
210 ∃ x ∈ (H : Subgroup G), QuotientGroup.mk' (U : Subgroup G) x = y := by
211 rfl
213/-- Membership in a closed subgroup of a profinite group can be checked after all open-normal
214finite quotients. -/
216 (hG : IsProfiniteGroup G) {H : ClosedSubgroup G} {x : G} :
217 x ∈ H ↔
218 ∀ U : OpenNormalSubgroup G,
219 OpenNormalSubgroup.quotientProj U x ∈
220 (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) := by
221 constructor
222 · intro hx U
223 exact (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
224 · intro hx
225 letI : T2Space G := IsProfiniteGroup.t2Space hG
226 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
227 have hxOpen :
228 ∀ N : Subgroup G, IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N → x ∈ N := by
229 intro N hN
230 let V : OpenSubgroup G := ⟨N, hN.1⟩
232 ⟨U, hHU⟩
233 have hxImg :
234 QuotientGroup.mk' (U : Subgroup G) x ∈
235 (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) := by
236 simpa [OpenNormalSubgroup.quotientProj] using hx U
237 have hxSup : x ∈ (H : Subgroup G) ⊔ (U : Subgroup G) := by
238 have hEq :
239 (H : Subgroup G) ⊔ (U : Subgroup G) =
240 Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
241 ((quotientImage (G := G) H U :
242 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
243 Subgroup (G ⧸ (U : Subgroup G))) := by
244 calc
245 (H : Subgroup G) ⊔ (U : Subgroup G) =
246 (H : Subgroup G) ⊔ (QuotientGroup.mk' (U : Subgroup G)).ker := by
247 rw [QuotientGroup.ker_mk']
248 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
249 (((H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))) :
250 Subgroup (G ⧸ (U : Subgroup G))) := by
251 rw [← Subgroup.comap_map_eq]
252 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
253 ((quotientImage (G := G) H U :
254 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
255 Subgroup (G ⧸ (U : Subgroup G))) := by
256 rfl
257 rw [hEq]
258 exact hxImg
259 rcases
260 (Subgroup.mem_sup_of_normal_right (s := (H : Subgroup G)) (t := (U : Subgroup G))).1
261 hxSup with
262 ⟨h, hhH, u, huU, hhu⟩
263 have hxV : x ∈ (V : Set G) := hHU ⟨h, hhH, u, huU, hhu⟩
264 simpa [V] using hxV
265 have hxInf :
266 x ∈ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N} := by
267 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
268 intro N hN
269 exact hxOpen N hN
270 change x ∈ (H : Subgroup G)
271 exact (closedSubgroup_eq_sInf_open (G := G) H).symm ▸ hxInf
273/-- Inclusion of closed subgroups of a profinite group can be checked on all open-normal finite
274quotients. -/
276 (hG : IsProfiniteGroup G) {H K : ClosedSubgroup G} :
277 (H : Subgroup G) ≤ (K : Subgroup G) ↔
278 ∀ U : OpenNormalSubgroup G,
279 (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) ≤
280 (quotientImage (G := G) K U : Subgroup (G ⧸ (U : Subgroup G))) := by
281 constructor
282 · intro hHK U y hy
283 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
284 exact (Subgroup.mem_map).2 ⟨x, hHK hx, rfl⟩
285 · intro hHK x hx
286 exact (mem_closedSubgroup_iff_forall_quotientImage_mem (G := G) hG (H := K)).2 (by
287 intro U
288 exact hHK U ((Subgroup.mem_map).2 ⟨x, hx, rfl⟩))
290/-- Closed subgroups of a profinite group are determined by their images in all open-normal
291finite quotients. -/
293 (hG : IsProfiniteGroup G) {H K : ClosedSubgroup G}
294 (hHK : ∀ U : OpenNormalSubgroup G,
295 quotientImage (G := G) H U = quotientImage (G := G) K U) :
296 H = K := by
297 letI : T2Space G := IsProfiniteGroup.t2Space hG
298 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
299 have hle :
300 ∀ {A B : ClosedSubgroup G},
301 (∀ U : OpenNormalSubgroup G,
302 quotientImage (G := G) A U = quotientImage (G := G) B U) →
303 (A : Subgroup G) ≤ B := by
304 intro A B hAB x hxA
305 have hxOpen :
306 ∀ N : Subgroup G, IsOpen (N : Set G) ∧ (B : Subgroup G) ≤ N → x ∈ N := by
307 intro N hN
308 let V : OpenSubgroup G := ⟨N, hN.1⟩
310 ⟨U, hBU⟩
311 have hxImgA :
312 QuotientGroup.mk' (U : Subgroup G) x ∈ (quotientImage (G := G) A U : Subgroup _) := by
313 exact (Subgroup.mem_map).2 ⟨x, hxA, rfl⟩
314 have hxImgB :
315 QuotientGroup.mk' (U : Subgroup G) x ∈ (quotientImage (G := G) B U : Subgroup _) := by
316 rw [← hAB U]
317 exact hxImgA
318 have hxSup : x ∈ (B : Subgroup G) ⊔ (U : Subgroup G) := by
319 have hEq :
320 (B : Subgroup G) ⊔ (U : Subgroup G) =
321 Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
322 ((quotientImage (G := G) B U :
323 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
324 Subgroup (G ⧸ (U : Subgroup G))) := by
325 calc
326 (B : Subgroup G) ⊔ (U : Subgroup G) =
327 (B : Subgroup G) ⊔ (QuotientGroup.mk' (U : Subgroup G)).ker := by
328 rw [QuotientGroup.ker_mk']
329 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
330 (((B : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))) :
331 Subgroup (G ⧸ (U : Subgroup G))) := by
332 rw [← Subgroup.comap_map_eq]
333 _ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
334 ((quotientImage (G := G) B U :
335 ClosedSubgroup (G ⧸ (U : Subgroup G))) :
336 Subgroup (G ⧸ (U : Subgroup G))) := by
337 rfl
338 rw [hEq]
339 exact hxImgB
340 rcases
341 (Subgroup.mem_sup_of_normal_right (s := (B : Subgroup G)) (t := (U : Subgroup G))).1
342 hxSup with
343 ⟨b, hbB, u, huU, hbu⟩
344 have hxV : x ∈ (V : Set G) := hBU ⟨b, hbB, u, huU, hbu⟩
345 simpa [V] using hxV
346 have hxB :
347 x ∈ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (B : Subgroup G) ≤ N} := by
348 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
349 intro N hN
350 exact hxOpen N hN
351 exact (closedSubgroup_eq_sInf_open (G := G) B).symm ▸ hxB
352 exact le_antisymm (hle hHK) (hle (fun U => (hHK U).symm))
354end FiniteQuotientImages
356variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
358section CompatibleClosedSubgroupFamilies
361variable {I : Type v} [Preorder I]
363variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
364variable [∀ i, IsTopologicalGroup (S.X i)]
365variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
368 TopologicalSpace (S.X i) :=
369 S.topologicalSpace i
371 ∀ i, TopologicalSpace (S.X i) :=
372 S.topologicalSpace
373instance instCompactSpaceXCompatFun : ∀ i, CompactSpace (S.X i) := by
374 intro i
375 infer_instance
376instance instT2SpaceXCompatFun : ∀ i, T2Space (S.X i) := by
377 intro i
378 infer_instance
380/-- The transition map of a group-valued inverse system, viewed as a homomorphism. -/
381def inverseSystemStageHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
382 toFun := S.map hij
383 map_one' := ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
384 map_mul' := ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij
386omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)]
387 [∀ i, T2Space (S.X i)] in
388/-- The stage homomorphism associated to a group-valued inverse system is continuous. -/
389theorem inverseSystemStageHom_continuous {i j : I} (hij : i ≤ j) :
390 Continuous (inverseSystemStageHom (S := S) hij) := by
391 simpa [inverseSystemStageHom] using (S.continuous_map hij :
392 Continuous (fun x : S.X j => S.map hij x))
394/-- The inverse system obtained by restricting an ambient inverse system to a compatible family of
395closed subgroups. -/
397 (L : ∀ i, ClosedSubgroup (S.X i))
398 (hcompat : ∀ {i j : I} (hij : i ≤ j),
399 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
401 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
402 (L i : Subgroup (S.X i))) :
404 X := fun i => L i
405 topologicalSpace := fun i => inferInstance
406 map := fun {i j} hij x =>
407 ⟨S.map hij x.1, by
408 have hx :
409 S.map hij x.1 ∈
410 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
412 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
413 exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
414 rw [hcompat hij] at hx
415 exact hx⟩
416 continuous_map := fun {i j} hij =>
417 Continuous.subtype_mk
418 ((inverseSystemStageHom_continuous (S := S) hij).comp continuous_subtype_val) (fun x => by
419 have hx :
420 S.map hij x.1 ∈
421 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
423 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
424 exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
425 rw [hcompat hij] at hx
426 exact hx)
427 map_id := fun i => by
428 funext x
429 apply Subtype.ext
430 simp only [InverseSystem.map_id_apply, id_eq]
431 map_comp := fun {i j k} hij hjk => by
432 funext x
433 apply Subtype.ext
434 simp only [Function.comp_apply, InverseSystem.map_comp_apply]
436/-- Each stage of a compatible closed-subgroup system is a group. -/
438 (L : ∀ i, ClosedSubgroup (S.X i))
439 (hcompat : ∀ {i j : I} (hij : i ≤ j),
440 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
442 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
443 (L i : Subgroup (S.X i)))
444 (i : I) :
445 Group ((compatibleClosedSubgroupSystem (S := S) L hcompat).X i) := by
447 infer_instance
449/-- A compatible closed-subgroup system is a group-valued inverse system. -/
451 (L : ∀ i, ClosedSubgroup (S.X i))
452 (hcompat : ∀ {i j : I} (hij : i ≤ j),
453 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
455 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
456 (L i : Subgroup (S.X i))) :
458 map_one := by
459 intro i j hij
460 apply Subtype.ext
462 (ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij)
463 map_mul := by
464 intro i j hij x y
465 apply Subtype.ext
467 (ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij x.1 y.1)
468 map_inv := by
469 intro i j hij x
470 apply Subtype.ext
472 (ProCGroups.InverseSystems.IsGroupSystem.map_inv (S := S) hij x.1)
474/--
475The canonical coordinatewise inclusion of a compatible subgroup system into the ambient system.
476-/
478 (L : ∀ i, ClosedSubgroup (S.X i))
479 (hcompat : ∀ {i j : I} (hij : i ≤ j),
480 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
482 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
483 (L i : Subgroup (S.X i))) :
484 (compatibleClosedSubgroupSystem (S := S) L hcompat).Morphism S where
485 map := fun i => Subtype.val
486 continuous_map := fun i => by
488 exact continuous_subtype_val
489 comm := fun {i j} hij => by
490 funext x
491 rfl
493/-- The induced homomorphism from the inverse limit of a compatible subgroup family into the
494ambient inverse limit. -/
496 (L : ∀ i, ClosedSubgroup (S.X i))
497 (hcompat : ∀ {i j : I} (hij : i ≤ j),
498 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
500 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
501 (L i : Subgroup (S.X i))) :
502 (compatibleClosedSubgroupSystem (S := S) L hcompat).inverseLimit →* S.inverseLimit where
503 toFun :=
506 map_one' := by
507 apply S.ext
508 intro i
509 rfl
510 map_mul' := by
511 intro x y
512 apply S.ext
513 intro i
514 rfl
516/-- Closed subgroup of the ambient inverse limit obtained from a compatible family of closed
517subgroups with surjective transition maps. -/
519 (L : ∀ i, ClosedSubgroup (S.X i))
520 (hcompat : ∀ {i j : I} (hij : i ≤ j),
521 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
523 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
524 (L i : Subgroup (S.X i))) :
525 ClosedSubgroup S.inverseLimit where
526 toSubgroup := (compatibleClosedSubgroupLimHom (S := S) L hcompat).range
527 isClosed' := by
528 let T := compatibleClosedSubgroupSystem (S := S) L hcompat
529 letI : ∀ i, TopologicalSpace (S.X i) := S.topologicalSpace
530 letI : ∀ i, T2Space (S.X i) := instT2SpaceXCompatFun (S := S)
531 letI : ∀ i, CompactSpace (T.X i) := fun i => by
533 infer_instance
534 letI : ∀ i, T2Space (T.X i) := fun i => by
536 infer_instance
537 letI : CompactSpace T.inverseLimit := inferInstance
538 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
539 let φ := compatibleClosedSubgroupLimHom (S := S) L hcompat
540 have hφcont :
541 Continuous (φ : T.inverseLimit → S.inverseLimit) := by
542 change Continuous (T.limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat))
543 exact T.continuous_limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat)
544 simpa [φ] using (isCompact_range hφcont).isClosed
546omit [∀ i, IsTopologicalGroup (S.X i)] in
547/-- Projection images of a closed subgroup recovered from a compatible family match the given family. -/
549 [CompactSpace S.inverseLimit]
550 (hdir : Directed (· ≤ ·) (id : I → I))
551 (L : ∀ i, ClosedSubgroup (S.X i))
552 (hcompat : ∀ {i j : I} (hij : i ≤ j),
553 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
555 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
556 (L i : Subgroup (S.X i))) (i : I) :
558 L i := by
559 let T := compatibleClosedSubgroupSystem (S := S) L hcompat
560 let incl := compatibleClosedSubgroupInclusion (S := S) L hcompat
561 let φ := compatibleClosedSubgroupLimHom (S := S) L hcompat
562 have hTsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (T.map hij) := by
563 intro i j hij y
564 have hy :
565 y.1 ∈
566 ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
568 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
569 exact (hcompat hij).symm ▸ (show y.1 ∈ (L i : Subgroup (S.X i)) from y.2)
570 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, hxy⟩
571 refine ⟨⟨x, hx⟩, ?_⟩
572 apply Subtype.ext
573 simpa [T, compatibleClosedSubgroupSystem] using hxy
574 letI : ∀ i, CompactSpace (T.X i) := fun i => by
576 infer_instance
577 letI : ∀ i, T2Space (T.X i) := fun i => by
579 infer_instance
580 letI : CompactSpace T.inverseLimit := inferInstance
581 letI : T2Space T.inverseLimit := T.t2Space_inverseLimit
582 ext y
583 constructor
584 · intro hy
585 rcases (Subgroup.mem_map).1 hy with ⟨x, hx, hxy⟩
586 rcases hx with ⟨z, rfl⟩
587 have hcoord :
588 S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) = (T.projection i z).1 := by
589 simpa [φ, compatibleClosedSubgroupInclusion] using congrFun (T.π_comp_limMap (Θ := incl) i) z
590 have hmem : (T.projection i z).1 ∈ (L i : Subgroup (S.X i)) := by
591 exact (T.projection i z).2
592 have hmem' : S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) ∈ (L i : Subgroup (S.X i)) := by
593 exact hcoord ▸ hmem
594 exact hxy ▸ hmem'
595 · intro hy
596 have hπsurj : Function.Surjective (T.projection i) := T.surjective_π hdir hTsurj i
597 rcases hπsurj ⟨y, hy⟩ with ⟨z, hz⟩
598 refine (Subgroup.mem_map).2 ?_
599 refine ⟨φ z, ⟨z, rfl⟩, ?_⟩
600 have hcoord :
601 S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) = y := by
603 compatibleClosedSubgroupSystem] using congrArg Subtype.val hz
604 exact hcoord
606omit [∀ i, IsTopologicalGroup (S.X i)] in
607/-- Projection images commute with mapping a closed subgroup along a compatible inverse-limit morphism. -/
609 [CompactSpace S.inverseLimit]
610 (H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
611 ((ClosedSubgroup.map (inverseLimitProjectionImage S H j) (inverseSystemStageHom (S := S) hij)
613 ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
614 (inverseLimitProjectionImage S H i : Subgroup (S.X i)) := by
615 ext x
616 constructor
617 · intro hx
618 rcases (Subgroup.mem_map).1 hx with ⟨y, hy, hxy⟩
619 rcases (Subgroup.mem_map).1 hy with ⟨z, hz, hzy⟩
620 refine (Subgroup.mem_map).2 ⟨z, hz, ?_⟩
621 calc
622 S.projection i z = S.map hij (S.projection j z) := by
623 symm
624 simpa using z.2 i j hij
625 _ = S.map hij y := by simpa using congrArg (S.map hij) hzy
626 _ = x := hxy
627 · intro hx
628 rcases (Subgroup.mem_map).1 hx with ⟨z, hz, hzx⟩
629 refine (Subgroup.mem_map).2 ⟨S.projection j z, ?_, ?_⟩
630 · exact (Subgroup.mem_map).2 ⟨z, hz, rfl⟩
631 · calc
632 S.map hij (S.projection j z) = S.projection i z := by
633 simpa using z.2 i j hij
634 _ = x := hzx
636omit [∀ i, IsTopologicalGroup (S.X i)] in
637/-- The stage-transition compatibility of projection images, repackaged as an equality of closed
638subgroups. -/
640 [CompactSpace S.inverseLimit]
641 (H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
642 ClosedSubgroup.map (inverseLimitProjectionImage S H j)
643 (inverseSystemStageHom (S := S) hij)
646 ext x
647 simpa using congrArg (fun K : Subgroup (S.X i) => x ∈ K)
650omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)] in
651/-- The projection image of the trivial closed subgroup is trivial. -/
653 [CompactSpace S.inverseLimit] (i : I) :
654 inverseLimitProjectionImage S (⊥ : ClosedSubgroup S.inverseLimit) i = ⊥ := by
655 ext x
656 constructor
657 · intro hx
658 rcases (Subgroup.mem_map).1 hx with ⟨y, hy, hyx⟩
659 have hy1 : y = 1 := by simpa using hy
660 cases hy1
661 simpa using hyx.symm
662 · intro hx
663 have hx1 : x = 1 := by simpa using hx
664 refine (Subgroup.mem_map).2 ⟨1, by simp only [one_mem], ?_⟩
665 rw [hx1]
666 rfl
668omit [∀ i, IsTopologicalGroup (S.X i)] in
669/-- Under surjective transition maps, the projection image of the whole inverse limit is the whole
670stage group. -/
672 [CompactSpace S.inverseLimit]
673 (hdir : Directed (· ≤ ·) (id : I → I))
674 (hsurj : IsSurjectiveInverseSystem S) (i : I) :
675 inverseLimitProjectionImage S (⊤ : ClosedSubgroup S.inverseLimit) i = ⊤ := by
676 ext x
677 constructor
678 · intro _
679 change x ∈ (⊤ : Subgroup (S.X i))
680 simp only [Subgroup.mem_top]
681 · intro _
682 have hπsurj : Function.Surjective (S.projection i) :=
683 S.surjective_π hdir (fun {i j} hij => hsurj hij) i
684 rcases hπsurj x with ⟨y, hy⟩
685 refine (Subgroup.mem_map).2 ⟨y, ?_, hy⟩
686 change y ∈ (⊤ : Subgroup S.inverseLimit)
687 simp only [Subgroup.mem_top]
689omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)] in
690/-- Projection images are monotone in the closed subgroup argument. -/
692 [CompactSpace S.inverseLimit]
693 {H K : ClosedSubgroup S.inverseLimit}
694 (hHK : (H : Subgroup S.inverseLimit) ≤ K) (i : I) :
695 (inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
696 (inverseLimitProjectionImage S K i : Subgroup (S.X i)) := by
697 intro x hx
698 rcases (Subgroup.mem_map).1 hx with ⟨y, hy, rfl⟩
699 exact (Subgroup.mem_map).2 ⟨y, hHK hy, rfl⟩
701/-- Closed subgroups of an inverse limit are determined by their stagewise projection images. -/
703 [Nonempty I] [CompactSpace S.inverseLimit]
704 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
705 [∀ i, TotallyDisconnectedSpace (S.X i)]
706 (hdir : Directed (· ≤ ·) (id : I → I))
707 (H K : ClosedSubgroup S.inverseLimit)
708 (hproj : ∀ i,
709 (inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
710 (inverseLimitProjectionImage S K i : Subgroup (S.X i))) :
711 (H : Subgroup S.inverseLimit) ≤ (K : Subgroup S.inverseLimit) := by
712 intro x hx
713 have hx' :
714 x ∈ sInf {N : Subgroup S.inverseLimit |
715 IsOpen (N : Set S.inverseLimit) ∧ (K : Subgroup S.inverseLimit) ≤ N} := by
716 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
717 intro N hN
718 let V : OpenSubgroup S.inverseLimit := ⟨N, hN.1⟩
719 rcases exists_openNormalSubgroup_mul_subset_openSubgroup (G := S.inverseLimit) K V hN.2 with
720 ⟨U, hKU⟩
721 letI : Finite (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
722 openNormalSubgroup_finiteQuotient (G := S.inverseLimit) U
723 letI : DiscreteTopology (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
724 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := S.inverseLimit) U)
725 let β : S.inverseLimit →* S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) :=
726 QuotientGroup.mk' (U : Subgroup S.inverseLimit)
728 (S := S) hdir β continuous_quotient_mk' with ⟨k, βk, hβkcont, hβfac⟩
729 have hxk : S.projection k x ∈ (inverseLimitProjectionImage S H k : Subgroup (S.X k)) := by
730 exact (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
731 have hxkK : S.projection k x ∈ (inverseLimitProjectionImage S K k : Subgroup (S.X k)) := hproj k hxk
732 rcases (Subgroup.mem_map).1 hxkK with ⟨z, hzK, hzxk⟩
733 have hβz : β z = βk (S.projection k z) := by
734 simpa [Function.comp] using
735 congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
736 f z) hβfac
737 have hβx : β x = βk (S.projection k x) := by
738 simpa [Function.comp] using
739 congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
740 f x) hβfac
741 have hzxu : z⁻¹ * x ∈ (U : Subgroup S.inverseLimit) := by
742 apply (QuotientGroup.eq_one_iff (N := (U : Subgroup S.inverseLimit)) (z⁻¹ * x)).1
743 have hβeq : β z = β x := by
744 calc
745 β z = βk (S.projection k z) := hβz
746 _ = βk (S.projection k x) := by simpa using congrArg βk hzxk
747 _ = β x := hβx.symm
748 calc
749 β (z⁻¹ * x) = (β z)⁻¹ * β x := by simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_mul, QuotientGroup.mk_inv, β]
750 _ = 1 := by simp only [hβeq, inv_mul_cancel]
751 have hxKU : x ∈ (((K : Subgroup S.inverseLimit) : Set S.inverseLimit) *
752 (((U : Subgroup S.inverseLimit) : Set S.inverseLimit))) := by
753 refine ⟨z, hzK, z⁻¹ * x, hzxu, ?_⟩
754 simp only [mul_inv_cancel_left]
755 exact hKU hxKU
756 exact (closedSubgroup_eq_sInf_open (G := S.inverseLimit) K).symm ▸ hx'
758/-- Stagewise equality of projection images determines a closed subgroup of an inverse limit. -/
760 [Nonempty I] [CompactSpace S.inverseLimit]
761 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
762 [∀ i, TotallyDisconnectedSpace (S.X i)]
763 (hdir : Directed (· ≤ ·) (id : I → I))
764 (H K : ClosedSubgroup S.inverseLimit)
766 H = K := by
767 have hHK : (H : Subgroup S.inverseLimit) ≤ (K : Subgroup S.inverseLimit) :=
768 closedSubgroup_le_of_projectionImages_le (S := S) hdir H K (fun i => by
769 exact
770 le_of_eq <|
771 congrArg (fun (L : ClosedSubgroup (S.X i)) => (L : Subgroup (S.X i))) (hproj i))
772 have hKH : (K : Subgroup S.inverseLimit) ≤ (H : Subgroup S.inverseLimit) :=
773 closedSubgroup_le_of_projectionImages_le (S := S) hdir K H (fun i => by
774 exact
775 le_of_eq <|
776 congrArg (fun (L : ClosedSubgroup (S.X i)) => (L : Subgroup (S.X i))) (hproj i).symm)
777 apply SetLike.ext'
778 exact Set.ext fun x => ⟨fun hx => hHK hx, fun hx => hKH hx⟩
780/-- If every stagewise projection image is trivial, then the closed subgroup itself is trivial. -/
782 [Nonempty I] [CompactSpace S.inverseLimit]
783 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
784 [∀ i, TotallyDisconnectedSpace (S.X i)]
785 (hdir : Directed (· ≤ ·) (id : I → I))
786 (H : ClosedSubgroup S.inverseLimit)
787 (hproj : ∀ i, inverseLimitProjectionImage S H i = ⊥) :
788 H = ⊥ := by
790 intro i
791 rw [hproj i, inverseLimitProjectionImage_bot (S := S) (i := i)]
793/-- If every stagewise projection image is the whole stage group, then the closed subgroup itself
794is the whole inverse limit. -/
796 [Nonempty I] [CompactSpace S.inverseLimit]
797 [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
798 [∀ i, TotallyDisconnectedSpace (S.X i)]
799 (hdir : Directed (· ≤ ·) (id : I → I))
801 (H : ClosedSubgroup S.inverseLimit)
802 (hproj : ∀ i, inverseLimitProjectionImage S H i = ⊤) :
803 H = ⊤ := by
805 intro i
806 rw [hproj i, inverseLimitProjectionImage_top (S := S) hdir hsurj i]
809end CompatibleClosedSubgroupFamilies
811end ProCGroups.Order