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

ProCGroups/Profinite/Basic.lean

1import ProCGroups.Profinite.OpenSubgroups
2import ProCGroups.InverseSystems.ProfiniteSpace
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Profinite/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Profinite group basics
15Basic profinite group predicates, finite quotient facts, and standard closure properties used throughout the pro-C library.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ProCGroups
23universe u v
25section Predicate
27variable {G : Type u} [Group G] [TopologicalSpace G]
29/-- An unbundled profinite group is a compact Hausdorff totally disconnected topological group. -/
30def IsProfiniteGroup (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
31 IsTopologicalGroup G ∧ CompactSpace G ∧ T2Space G ∧ TotallyDisconnectedSpace G
35/-- The topological group component of a profinite group. -/
36theorem isTopologicalGroup (hG : IsProfiniteGroup G) : IsTopologicalGroup G :=
37 hG.1
39/-- The compactness component of a profinite group. -/
40theorem compactSpace (hG : IsProfiniteGroup G) : CompactSpace G :=
41 hG.2.1
43/-- The Hausdorff component of a profinite group. -/
44theorem t2Space (hG : IsProfiniteGroup G) : T2Space G :=
45 hG.2.2.1
47/-- The `T1` component of a profinite group. -/
48theorem t1Space (hG : IsProfiniteGroup G) : T1Space G := by
49 letI : T2Space G := hG.t2Space
50 infer_instance
52/-- The totally disconnected component of a profinite group. -/
53theorem totallyDisconnectedSpace (hG : IsProfiniteGroup G) : TotallyDisconnectedSpace G :=
54 hG.2.2.2
56/-- A topological group whose underlying topological space is profinite is a profinite group. -/
57theorem of_isProfiniteSpace [IsTopologicalGroup G]
58 (hG : InverseSystems.IsProfiniteSpace G) : IsProfiniteGroup G :=
59 ⟨inferInstance, hG.1, hG.2.1, hG.2.2⟩
63end Predicate
65section Permanence
67variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
69omit [IsTopologicalGroup G] in
70/-- Repackage a permanence theorem stated for `ClosedSubgroup`s into the ordinary subgroup form. -/
72 {P : Subgroup G → Prop}
73 (h : ∀ H : ClosedSubgroup G, P (H : Subgroup G))
74 (H : Subgroup G) (hH : IsClosed (H : Set G)) :
75 P H := by
76 let HC : ClosedSubgroup G := ⟨H, hH⟩
77 simpa using h HC
81omit [IsTopologicalGroup G] in
82/-- Any finite discrete topological group is profinite. -/
83theorem of_finite_discrete (G : Type u) [Group G] [TopologicalSpace G]
84 [Finite G] [DiscreteTopology G] : IsProfiniteGroup G := by
85 letI : Fintype G := Fintype.ofFinite G
86 letI : CompactSpace G := by infer_instance
87 letI : T2Space G := by infer_instance
88 letI : TotallyDisconnectedSpace G := by infer_instance
89 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
91/-- A quotient of a profinite group by an open normal subgroup is profinite. -/
92theorem quotient_openNormalSubgroup (hG : IsProfiniteGroup G) (U : OpenNormalSubgroup G) :
93 IsProfiniteGroup (G ⧸ (U : Subgroup G)) := by
94 letI : CompactSpace G := hG.compactSpace
95 letI : T2Space G := hG.t2Space
96 letI : Finite (G ⧸ (U : Subgroup G)) := openNormalSubgroup_finiteQuotient (G := G) U
97 letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
98 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
99 exact of_finite_discrete (G := G ⧸ (U : Subgroup G))
101/-- Closed-subgroup permanence for profinite groups. -/
102theorem of_closedSubgroup (hG : IsProfiniteGroup G) (H : ClosedSubgroup G) :
103 IsProfiniteGroup ↥(H : Subgroup G) := by
104 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
105 letI : T2Space G := IsProfiniteGroup.t2Space hG
106 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
107 letI : CompactSpace H := inferInstance
108 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
110/-- Closed-subgroup permanence using an ordinary subgroup together with a closedness proof. -/
111theorem of_isClosed_subgroup (hG : IsProfiniteGroup G) (H : Subgroup G)
112 (hH : IsClosed (H : Set G)) : IsProfiniteGroup ↥H := by
114 (G := G) (P := fun H => IsProfiniteGroup ↥H) (of_closedSubgroup (G := G) hG) H hH
116/-- Arbitrary product permanence for profinite groups. -/
117theorem pi {α : Type v} {β : α → Type u}
118 [∀ a, Group (β a)] [∀ a, TopologicalSpace (β a)] [∀ a, IsTopologicalGroup (β a)]
119 (hβ : ∀ a, IsProfiniteGroup (β a)) :
120 IsProfiniteGroup ((a : α) → β a) := by
121 letI : ∀ a, CompactSpace (β a) := fun a => IsProfiniteGroup.compactSpace (hβ a)
122 letI : ∀ a, T2Space (β a) := fun a => IsProfiniteGroup.t2Space (hβ a)
123 letI : ∀ a, TotallyDisconnectedSpace (β a) := fun a =>
124 IsProfiniteGroup.totallyDisconnectedSpace (hβ a)
125 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
127/-- Binary-product case of `IsProfiniteGroup.pi`. -/
128theorem prod {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v}
129 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
131 IsProfiniteGroup (G × H) := by
132 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
133 letI : CompactSpace H := IsProfiniteGroup.compactSpace hH
134 letI : T2Space G := IsProfiniteGroup.t2Space hG
135 letI : T2Space H := IsProfiniteGroup.t2Space hH
136 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
137 letI : TotallyDisconnectedSpace H := IsProfiniteGroup.totallyDisconnectedSpace hH
138 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
140/-- In a profinite group, an element lying in every open normal subgroup must be `1`. -/
142 [TotallyDisconnectedSpace G] {x : G}
143 (hx : ∀ U : OpenNormalSubgroup G, x ∈ (U : Subgroup G)) : x = 1 := by
144 by_contra hxne
145 let W : Set G := ({x} : Set G)ᶜ
146 have hW : IsOpen W := by
147 simp only [isOpen_compl_iff, finite_singleton, Finite.isClosed, W]
148 have h1W : (1 : G) ∈ W := by
149 have hx1 : (1 : G) ≠ x := by
150 intro h1x
151 exact hxne h1x.symm
152 simp only [mem_compl_iff, mem_singleton_iff, hx1, not_false_eq_true, W]
153 rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
154 (G := G) hW h1W with ⟨U, hUW⟩
155 have hxU : x ∈ (U : Subgroup G) := hx U
156 have hxW : x ∈ W := hUW hxU
157 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hxW
161end Permanence
163end ProCGroups