Source: ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation
1import Mathlib.Topology.Algebra.Group.Basic
3/-!
4# Quotient formations and their subgroup topology
6A quotient formation specifies admissible normal quotient kernels and their closure properties.
7This file defines the induced open subgroups, pro-\(C\) closure, closed subgroups, and residuality,
8and proves their basic lattice and separation characterizations.
9-/
11open Set
12open scoped Topology
14namespace ProCGroups.Topologies
16universe u
18/--
19A quotient formation records which quotient subgroups belong to the chosen class and the closure
20properties needed for the pro-\(C\) topology.
21-/
22structure QuotientFormation where
23 /-- The predicate selecting the subgroups that define admissible quotients. -/
24 contains : ∀ {G : Type u} [Group G], Subgroup G → Prop
25 /-- The whole group is an admissible quotient kernel. -/
26 top_mem : ∀ {G : Type u} [Group G], contains (G := G) (⊤ : Subgroup G)
27 /-- Every admissible quotient kernel is normal. -/
28 normal_of_mem : ∀ {G : Type u} [Group G] {N : Subgroup G}, contains (G := G) N → N.Normal
29 /--
30 An admissible kernel remains admissible when enlarged to a normal subgroup.
31 -/
32 upward_closed :
33 ∀ {G : Type u} [Group G] {N K : Subgroup G},
34 contains (G := G) N → N ≤ K → K.Normal → contains (G := G) K
35 /-- The intersection of two admissible quotient kernels is admissible. -/
36 inf_closed :
37 ∀ {G : Type u} [Group G] {N K : Subgroup G},
38 contains (G := G) N → contains (G := G) K → contains (G := G) (N ⊓ K)
40namespace QuotientFormation
42variable (C : QuotientFormation)
44/--
45A subgroup is open in the pro-\(C\) topology if and only if it contains one of the basic
46kernels.
47-/
48def IsOpenSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
49 ∃ N : Subgroup G, C.contains N ∧ N ≤ H
51/-- Algebraic closure operator attached to the pro-\(C\) topology. -/
52def proCClosure {G : Type u} [Group G] (H : Subgroup G) : Subgroup G :=
53 sInf {K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}
55/--
56A subgroup is closed in the algebraic pro-\(C\) topology exactly when it equals its pro-\(C\)
57closure.
58-/
59def IsClosedSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
60 C.proCClosure H = H
62/-- Residuality for the pro-\(C\) topology: the identity is separated by the basic open kernels. -/
63def IsResiduallyC {G : Type u} [Group G] : Prop :=
64 C.proCClosure (⊥ : Subgroup G) = ⊥
66variable {C}
67variable {G : Type u} [Group G]
69/-- The whole group is open for a quotient formation. -/
70@[simp] theorem isOpenSubgroup_top (C : QuotientFormation) :
71 C.IsOpenSubgroup (⊤ : Subgroup G) := by
72 exact ⟨⊤, C.top_mem, le_rfl⟩
74/--
75A subgroup containing an open subgroup for a quotient formation is open in the left-hand
76quotient-formation topology.
77-/
78theorem isOpenSubgroup_sup_left (C : QuotientFormation) {H K : Subgroup G}
79 (hH : C.IsOpenSubgroup H) :
80 C.IsOpenSubgroup (H ⊔ K) := by
81 rcases hH with ⟨N, hN, hNH⟩
82 exact ⟨N, hN, le_trans hNH le_sup_left⟩
84/--
85A subgroup containing an open subgroup for a quotient formation is open in the right-hand
86quotient-formation topology.
87-/
88theorem isOpenSubgroup_sup_right (C : QuotientFormation) {H K : Subgroup G}
89 (hK : C.IsOpenSubgroup K) :
90 C.IsOpenSubgroup (H ⊔ K) := by
91 simpa [sup_comm] using
92 (C.isOpenSubgroup_sup_left (H := K) (K := H) hK)
94/-- A subgroup is contained in its pro-\(C\) closure. -/
95theorem le_proCClosure (C : QuotientFormation) (H : Subgroup G) :
96 H ≤ C.proCClosure H := by
97 change H ≤ sInf {K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}
98 exact le_sInf fun K hK => hK.2
100/-- The pro-\(C\) closure operation is monotone. -/
101theorem proCClosure_mono (C : QuotientFormation) {H K : Subgroup G}
102 (hHK : H ≤ K) :
103 C.proCClosure H ≤ C.proCClosure K := by
104 change
105 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ H ≤ L} ≤
106 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ K ≤ L}
107 refine le_sInf ?_
108 intro L hL
109 exact sInf_le ⟨hL.1, hHK.trans hL.2⟩
111/-- The pro-\(C\) closure operation is idempotent. -/
112theorem proCClosure_idem (C : QuotientFormation) (H : Subgroup G) :
113 C.proCClosure (C.proCClosure H) = C.proCClosure H := by
114 refine le_antisymm ?_ (C.proCClosure_mono (C.le_proCClosure H))
115 change
116 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ C.proCClosure H ≤ L} ≤
117 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ H ≤ L}
118 refine le_sInf ?_
119 intro L hL
120 exact sInf_le ⟨hL.1, sInf_le hL⟩
122/--
123Closed subgroups for the quotient formation are exactly those containing the pro-\(C\) closure
124of every smaller subgroup.
125-/
126theorem isClosedSubgroup_iff_proCClosure_le {C : QuotientFormation} {H : Subgroup G} :
127 C.IsClosedSubgroup H ↔ C.proCClosure H ≤ H := by
128 constructor
129 · intro hH
130 rw [QuotientFormation.IsClosedSubgroup] at hH
131 rw [hH]
132 · intro hH
133 exact le_antisymm hH (C.le_proCClosure H)
135/--
136Residual \(C\)-ness is equivalent to the pro-\(C\) closure of the bottom subgroup being bottom.
137-/
138@[simp] theorem isResiduallyC_iff_proCClosure_bot_eq_bot {C : QuotientFormation} :
139 C.IsResiduallyC (G := G) ↔ C.proCClosure (⊥ : Subgroup G) = ⊥ :=
140 Iff.rfl
142/--
143An element outside the pro-\(C\) closure is separated by an open subgroup in the quotient
144formation.
145-/
146theorem exists_openSubgroup_not_mem_of_not_mem_proCClosure
147 (C : QuotientFormation) {H : Subgroup G} {x : G}
148 (hx : x ∉ C.proCClosure H) :
149 ∃ K : Subgroup G, C.IsOpenSubgroup K ∧ H ≤ K ∧ x ∉ K := by
150 rw [QuotientFormation.proCClosure, Subgroup.mem_sInf] at hx
151 push Not at hx
152 rcases hx with ⟨K, hK, hxK⟩
153 exact ⟨K, hK.1, hK.2, hxK⟩
155/--
156In a residually \(C\) group, a nontrivial element is excluded by some open subgroup in the
157quotient formation.
158-/
159theorem exists_openSubgroup_not_mem_of_isResiduallyC
160 (C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
161 {x : G} (hx : x ≠ 1) :
162 ∃ K : Subgroup G, C.IsOpenSubgroup K ∧ x ∉ K := by
163 have hxbot : x ∉ C.proCClosure (⊥ : Subgroup G) := by
164 rw [hC]
165 simpa using hx
166 rcases C.exists_openSubgroup_not_mem_of_not_mem_proCClosure
167 (H := (⊥ : Subgroup G)) hxbot with ⟨K, hKopen, _hbotK, hxK⟩
168 exact ⟨K, hKopen, hxK⟩
170/-- The normal core of an open subgroup again defines a quotient in the formation. -/
171theorem normalCore_mem_of_open (C : QuotientFormation) {H : Subgroup G}
172 (hH : C.IsOpenSubgroup H) :
173 C.contains H.normalCore := by
174 rcases hH with ⟨N, hN, hNH⟩
175 let _ : N.Normal := C.normal_of_mem hN
176 have hNcore : N ≤ H.normalCore := (Subgroup.normal_le_normalCore).2 hNH
177 exact C.upward_closed hN hNcore inferInstance
179/--
180In a residually \(C\) group, a nontrivial element is excluded by an open normal kernel in the
181quotient formation.
182-/
183theorem exists_openKernel_not_mem_of_isResiduallyC
184 (C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
185 {x : G} (hx : x ≠ 1) :
186 ∃ N : Subgroup G, C.contains N ∧ N.Normal ∧ x ∉ N := by
187 rcases C.exists_openSubgroup_not_mem_of_isResiduallyC (G := G) hC hx with
188 ⟨K, hKopen, hxK⟩
189 refine ⟨K.normalCore, C.normalCore_mem_of_open hKopen, ?_, ?_⟩
190 · exact C.normal_of_mem (C.normalCore_mem_of_open hKopen)
191 · intro hxcore
192 exact hxK (Subgroup.normalCore_le K hxcore)
194/-- Closed subgroups are exactly intersections of open subgroups. -/
195theorem isClosedSubgroup_iff_exists_sInf_openSubgroups
196 {C : QuotientFormation} {H : Subgroup G} :
197 C.IsClosedSubgroup H ↔
198 ∃ S : Set (Subgroup G), (∀ K ∈ S, C.IsOpenSubgroup K) ∧ H = sInf S := by
199 constructor
200 · intro hH
201 refine ⟨{K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}, ?_, ?_⟩
202 · intro K hK
203 exact hK.1
204 · simpa [QuotientFormation.IsClosedSubgroup, QuotientFormation.proCClosure] using hH.symm
205 · rintro ⟨S, hSopen, hEq⟩
206 rw [QuotientFormation.IsClosedSubgroup]
207 refine le_antisymm ?_ (C.le_proCClosure H)
208 calc
209 C.proCClosure H ≤ sInf S := by
210 refine le_sInf ?_
211 intro K hK
212 have hHK : H ≤ K := by
213 rw [hEq]
214 exact sInf_le hK
215 exact sInf_le ⟨hSopen K hK, hHK⟩
216 _ = H := hEq.symm
218end QuotientFormation
220end ProCGroups.Topologies