Yamaguchi Lean 4 Library
ProCGroups/GroupTheory/CentralizerNormalizerCommensurator.lean
ProCGroups/GroupTheory/CentralizerNormalizerCommensurator/Source

ProCGroups/GroupTheory/CentralizerNormalizerCommensurator.lean

1import Mathlib.GroupTheory.Commensurable
2import ProCGroups.Generation.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/GroupTheory/CentralizerNormalizerCommensurator.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Centralizers, normalizers, and commensurators
15This file collects the subgroup centralizer, normalizer, and commensurator API used by
16profinite-group applications. The definitions are the mathlib definitions, exposed under the
17`ProCGroups.GroupTheory` namespace so downstream files can use one focused PCG import. It also
18records closure and topological-closure facts that are repeatedly useful for profinite groups.
19-/
21open scoped Pointwise
23namespace ProCGroups.GroupTheory
25universe u
27variable {G : Type u} [Group G]
29/-- The centralizer of a set of elements. -/
30abbrev centralizer (S : Set G) : Subgroup G :=
31 Subgroup.centralizer S
33/-- The centralizer of a single element. -/
34abbrev centralizerOf (g : G) : Subgroup G :=
35 centralizer ({g} : Set G)
37/-- The normalizer of a subgroup. -/
38abbrev normalizer (H : Subgroup G) : Subgroup G :=
39 H.normalizer
41/-- The commensurator of a subgroup. -/
42abbrev commensurator (H : Subgroup G) : Subgroup G :=
43 Subgroup.Commensurable.commensurator H
45/-- Membership in the centralizer means commuting with every element of the set. -/
46@[simp] theorem mem_centralizer_iff {S : Set G} {g : G} :
47 g ∈ centralizer S ↔ ∀ h ∈ S, h * g = g * h :=
48 Iff.rfl
50/-- Membership in the centralizer, written as a vanishing commutator. -/
51@[simp] theorem mem_centralizer_iff_commutator_eq_one {S : Set G} {g : G} :
52 g ∈ centralizer S ↔ ∀ h ∈ S, h * g * h⁻¹ * g⁻¹ = 1 := by
53 simpa [centralizer] using
54 (Subgroup.mem_centralizer_iff_commutator_eq_one (g := g) (s := S))
56/-- Membership in the centralizer of one element is commutation with that element. -/
57@[simp] theorem mem_centralizerOf_iff {x g : G} :
58 x ∈ centralizerOf g ↔ x * g = g * x := by
60 (Subgroup.mem_centralizer_singleton_iff (g := g) (k := x))
62/-- Centralizing an element implies centralizing each of its natural powers. -/
63theorem mem_centralizerOf_pow_of_mem {x y : G} (hy : y ∈ centralizerOf x) (n : ℕ) :
64 y ∈ centralizerOf (x ^ n) := by
65 rw [mem_centralizerOf_iff] at hy ⊢
66 induction n with
67 | zero =>
68 simp only [pow_zero, mul_one, one_mul]
69 | succ n ih =>
70 calc
71 y * x ^ (n + 1) = (y * x ^ n) * x := by rw [pow_succ, mul_assoc]
72 _ = (x ^ n * y) * x := by rw [ih]
73 _ = x ^ n * (y * x) := by rw [mul_assoc]
74 _ = x ^ n * (x * y) := by rw [hy]
75 _ = x ^ (n + 1) * y := by rw [pow_succ, mul_assoc]
77/-- Centralizing an inverse is the same as centralizing the element. -/
78theorem mem_centralizerOf_inv_iff {x y : G} :
79 y ∈ centralizerOf x⁻¹ ↔ y ∈ centralizerOf x := by
81 constructor
82 · intro h
83 have h' := congrArg (fun z => x * z * x) h
84 simpa [mul_assoc] using h'.symm
85 · intro h
86 have h' := congrArg (fun z => x⁻¹ * z * x⁻¹) h
87 simpa [mul_assoc] using h'.symm
89/-- Replacing a nonzero integer power by its positive absolute value does not change the
90centralizer. -/
91theorem centralizerOf_zpow_eq_natAbs (x : G) {n : ℤ} (_hn : n ≠ 0) :
92 centralizerOf (x ^ n) = centralizerOf (x ^ (n.natAbs : ℤ)) := by
93 cases n with
94 | ofNat k =>
95 simp only [Int.ofNat_eq_natCast, zpow_natCast, Int.natAbs_natCast]
96 | negSucc k =>
97 ext y
98 simp only [Int.natAbs, zpow_negSucc, zpow_natCast]
101/-- Membership form of `centralizerOf_zpow_eq_natAbs`. -/
102theorem mem_centralizerOf_zpow_natAbs_of_mem_zpow {x y : G} {n : ℤ} (hn : n ≠ 0)
103 (hy : y ∈ centralizerOf (x ^ n)) :
104 y ∈ centralizerOf (x ^ (n.natAbs : ℤ)) := by
107/-- If an integer power is nontrivial, so is the corresponding positive absolute power. -/
108theorem zpow_natAbs_ne_one_of_zpow_ne_one {x : G} {n : ℤ}
109 (h : x ^ n ≠ 1) :
110 x ^ (n.natAbs : ℤ) ≠ 1 := by
111 cases n with
112 | ofNat k =>
113 simpa using h
114 | negSucc k =>
115 intro hpos
116 have hposZ : x ^ (((k + 1 : ℕ) : ℤ)) = 1 := by
117 simpa [Int.natAbs, Nat.cast_add, Nat.cast_one] using hpos
118 have hpos' : x ^ (k + 1) = 1 := by
119 rw [← zpow_natCast (a := x) (n := k + 1)]
120 exact hposZ
121 exact h (by simp [zpow_negSucc, hpos'])
123/-- If `c` and `c * d` centralize `x`, then `d` centralizes `x`. -/
125 (hc : c ∈ centralizerOf x) (hcd : c * d ∈ centralizerOf x) :
126 d ∈ centralizerOf x := by
127 rw [mem_centralizerOf_iff] at hc hcd ⊢
128 calc
129 d * x = c⁻¹ * (c * d * x) := by simp [mul_assoc]
130 _ = c⁻¹ * (x * (c * d)) := by rw [hcd]
131 _ = c⁻¹ * ((x * c) * d) := by simp [mul_assoc]
132 _ = c⁻¹ * ((c * x) * d) := by rw [← hc]
133 _ = x * d := by simp [mul_assoc]
135/-- An element centralizes itself. -/
136theorem centralizerOf_self_mem (g : G) :
137 g ∈ centralizerOf g := by
138 simp only [centralizerOf, mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]
140/-- Centralizers are antitone in the set being centralized. -/
141theorem centralizer_le {S T : Set G} (hST : S ⊆ T) :
143 simpa [centralizer] using Subgroup.centralizer_le (G := G) hST
145/-- Two subgroups centralize each other symmetrically. -/
146theorem le_centralizer_iff {H K : Subgroup G} :
147 H ≤ centralizer (K : Set G) ↔ K ≤ centralizer (H : Set G) := by
148 simpa [centralizer] using (Subgroup.le_centralizer_iff (H := H) (K := K))
150/-- A set has full centralizer exactly when it lies in the center. -/
151theorem centralizer_eq_top_iff_subset {S : Set G} :
152 centralizer S = ⊤ ↔ S ⊆ (Subgroup.center G : Set G) := by
153 simp only [centralizer, Subgroup.centralizer_eq_top_iff_subset]
155/-- The centralizer of a normal subgroup is normal. -/
156instance centralizer_normal (H : Subgroup G) [H.Normal] :
157 (centralizer (H : Set G)).Normal := by
159 infer_instance
161/-- The centralizer of a characteristic subgroup is characteristic. -/
162instance centralizer_characteristic (H : Subgroup G) [H.Characteristic] :
163 (centralizer (H : Set G)).Characteristic := by
165 infer_instance
167/-- In a Hausdorff topological group, the centralizer of one element is closed. -/
169 [TopologicalSpace G] [ContinuousMul G] [T2Space G] (g : G) :
170 IsClosed ((centralizerOf g : Subgroup G) : Set G) := by
172 Set.isClosed_centralizer (M := G) ({g} : Set G)
174/-- For fixed `g`, the set of elements commuting with `g` is closed. -/
176 [TopologicalSpace G] [ContinuousMul G] [T2Space G] (g : G) :
177 IsClosed {x : G | x * g = g * x} := by
178 have hset :
179 ((centralizerOf g : Subgroup G) : Set G) = {x : G | x * g = g * x} := by
180 ext x
182 rw [← hset]
183 exact centralizerOf_isClosed (G := G) g
185/-- Topological generation preserves containment in a closed centralizer. -/
187 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
188 {S T : Set G} (hS : S ⊆ (centralizer T : Set G)) :
189 (ProCGroups.Generation.closedSubgroupGenerated (G := G) S : Subgroup G) ≤ centralizer T := by
190 have hclosure : Subgroup.closure S ≤ centralizer T := by
191 rw [Subgroup.closure_le]
192 exact hS
193 exact
194 Subgroup.topologicalClosure_minimal
195 _
196 hclosure
197 (by simpa [centralizer] using Set.isClosed_centralizer (M := G) T)
199/-- A subgroup and its topological closure have the same centralizer. -/
201 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (S : Subgroup G) :
202 centralizer ((S.topologicalClosure : Subgroup G) : Set G) = centralizer (S : Set G) := by
203 apply le_antisymm
204 · exact centralizer_le (Subgroup.le_topologicalClosure (s := S))
205 · intro g hg
206 rw [mem_centralizer_iff] at hg ⊢
207 have hclosure : (S.topologicalClosure : Subgroup G) ≤ centralizerOf g := by
208 exact
209 Subgroup.topologicalClosure_minimal
210 S
211 (by
212 intro x hx
213 exact mem_centralizerOf_iff.mpr (hg x hx))
215 intro x hx
216 exact mem_centralizerOf_iff.mp (hclosure hx)
218/-- The closed subgroup topologically generated by `g` centralizes every integer power of `g`. -/
220 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
221 (g : G) (n : ℤ) :
222 (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({g} : Set G) : Subgroup G) ≤
223 centralizerOf (g ^ n) := by
224 have hclosure :
225 Subgroup.closure ({g} : Set G) ≤ centralizerOf (g ^ n) := by
226 rw [Subgroup.closure_le]
227 intro y hy
228 rw [Set.mem_singleton_iff] at hy
229 subst y
230 exact mem_centralizerOf_iff.mpr
231 (by simpa using (Commute.zpow_zpow_self g (1 : ℤ) n).eq)
232 exact
233 Subgroup.topologicalClosure_minimal
234 _
235 hclosure
236 (centralizerOf_isClosed (G := G) (g ^ n))
238/-- Membership form of `closedSubgroupGenerated_singleton_le_centralizerOf_zpow`. -/
240 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
241 {x c : G} (n : ℤ)
242 (hc : c ∈ (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) :
243 Subgroup G)) :
244 c ∈ centralizerOf (x ^ n) :=
247/-- If a single element topologically generates the group, the centralizer of any of its powers is
248the corresponding closed cyclic subgroup. -/
250 [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
251 (x : G) (n : ℤ)
252 (hgen : ProCGroups.Generation.TopologicallyGenerates (G := G) ({x} : Set G)) :
253 centralizerOf (x ^ n) =
254 (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G) := by
255 have hcyc :
256 (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G) =
257 ⊤ := by
260 have hcent_top : centralizerOf (x ^ n) = ⊤ := by
261 apply top_unique
262 rw [← hcyc]
264 simpa [hcyc] using hcent_top
266/-- Membership in the normalizer, stated by invariance under conjugation by the element. -/
267@[simp] theorem mem_normalizer_iff {H : Subgroup G} {g : G} :
268 g ∈ normalizer H ↔ ∀ h : G, h ∈ H ↔ g * h * g⁻¹ ∈ H := by
269 simpa [normalizer] using (Subgroup.mem_normalizer_iff (H := H) (g := g))
271/-- The centralizer of a subgroup is contained in its normalizer. -/
272theorem centralizer_le_normalizer (H : Subgroup G) :
273 centralizer (H : Set G) ≤ normalizer H := by
274 intro g hg
276 intro h
277 constructor
278 · intro hh
279 have hcomm : h * g = g * h := (mem_centralizer_iff.mp hg) h hh
280 simpa [← hcomm, mul_assoc] using hh
281 · intro hh
282 let k : G := g * h * g⁻¹
283 have hk : k ∈ H := hh
284 have hcomm : k * g = g * k := (mem_centralizer_iff.mp hg) k hk
285 have h_eq_k : h = k := by
286 calc
287 h = g⁻¹ * (k * g) := by
288 simp only [mul_assoc, inv_mul_cancel, mul_one, inv_mul_cancel_left, k]
289 _ = g⁻¹ * (g * k) := by rw [hcomm]
290 _ = k := by simp only [inv_mul_cancel_left]
291 simpa [h_eq_k] using hk
293/-- Membership in the commensurator, stated in terms of the conjugation action. -/
294@[simp] theorem mem_commensurator_iff {H : Subgroup G} {g : G} :
295 g ∈ commensurator H ↔
296 Subgroup.Commensurable (ConjAct.toConjAct g • H) H := by
297 rfl
299/-- The normalizer of a subgroup is contained in its commensurator. -/
300theorem normalizer_le_commensurator (H : Subgroup G) :
302 intro g hg
304 have hsmul : ConjAct.toConjAct g • H = H :=
305 Subgroup.conjAct_pointwise_smul_eq_self (H := H) (g := g) (by
306 simpa [normalizer] using hg)
307 simpa [hsmul] using (Subgroup.Commensurable.refl H)
309/-- An element of the normalizer is an element of the commensurator. -/
310theorem mem_commensurator_of_mem_normalizer {H : Subgroup G} {g : G}
311 (hg : g ∈ normalizer H) :
312 g ∈ commensurator H :=
315/-- The centralizer of a subgroup is contained in its commensurator. -/
316theorem centralizer_le_commensurator (H : Subgroup G) :
317 centralizer (H : Set G) ≤ commensurator H :=
320/-- Commensurable subgroups have the same commensurator. -/
321theorem commensurator_eq_of_commensurable {H K : Subgroup G}
322 (hHK : Subgroup.Commensurable H K) :
324 simpa [commensurator] using Subgroup.Commensurable.eq hHK
326/-- Membership in the commensurator is invariant under replacing by a commensurable subgroup. -/
328 (hHK : Subgroup.Commensurable H K) {g : G} :
329 g ∈ commensurator H ↔ g ∈ commensurator K := by
332/-- Transport commensurator membership across commensurable subgroups. -/
333theorem mem_commensurator_of_commensurable {H K : Subgroup G}
334 (hHK : Subgroup.Commensurable H K) {g : G}
335 (hg : g ∈ commensurator H) :
336 g ∈ commensurator K :=
339end ProCGroups.GroupTheory