Centralizer lemmas and closed-cyclic-subgroup results used by the profinite applications.
The centralizer of a set of elements.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]abbrev centralizer (S : Set G) : Subgroup GThe centralizer of a single element.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]abbrev centralizerOf (g : G) : Subgroup GMembership in the centralizer is equivalent to the displayed commutation condition.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem mem_centralizer_iff {S : Set G} {g : G} :
g ∈ centralizer S ↔ ∀ h ∈ S, h * g = g * hMembership in the centralizer of a subset is equivalent to the displayed commutation condition.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem mem_centralizerOf_iff {x g : G} :
x ∈ centralizerOf g ↔ x * g = g * xCentralizing an element implies centralizing each of its natural powers.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem mem_centralizerOf_pow_of_mem {x y : G} (hy : y ∈ centralizerOf x) (n : ℕ) :
y ∈ centralizerOf (x ^ n)Membership of an inverse in the centralizer of a subset is equivalent to the displayed commutation condition.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem mem_centralizerOf_inv_iff {x y : G} :
y ∈ centralizerOf x⁻¹ ↔ y ∈ centralizerOf xReplacing a nonzero integer power by its positive absolute value does not change the centralizer.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem centralizerOf_zpow_eq_natAbs (x : G) {n : ℤ} (_hn : n ≠ 0) :
centralizerOf (x ^ n) = centralizerOf (x ^ (n.natAbs : ℤ))Centralizing a nonzero integer power is equivalent, for membership purposes, to centralizing the corresponding positive absolute power.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem mem_centralizerOf_zpow_natAbs_of_mem_zpow {x y : G} {n : ℤ} (hn : n ≠ 0)
(hy : y ∈ centralizerOf (x ^ n)) :
y ∈ centralizerOf (x ^ (n.natAbs : ℤ))If c and \(c * d\) centralize x, then d centralizes x.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem right_factor_mem_centralizerOf_of_mul_mem_and_left_mem {x c d : G}
(hc : c ∈ centralizerOf x) (hcd : c * d ∈ centralizerOf x) :
d ∈ centralizerOf xIn a Hausdorff topological group, the centralizer of one element is closed.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem centralizerOf_isClosed
[TopologicalSpace G] [ContinuousMul G] [T2Space G] (g : G) :
IsClosed ((centralizerOf g : Subgroup G) : Set G)Topological generation preserves containment in a closed centralizer.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem closedSubgroupGenerated_le_centralizer_of_subset
[TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
{S T : Set G} (hS : S ⊆ (centralizer T : Set G)) :
(ProCGroups.Generation.closedSubgroupGenerated (G := G) S : Subgroup G) ≤ centralizer TA subgroup and its topological closure have the same centralizer.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem centralizer_eq_centralizer_topologicalClosure
[TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (S : Subgroup G) :
centralizer ((S.topologicalClosure : Subgroup G) : Set G) = centralizer (S : Set G)The closed subgroup topologically generated by \(g\) centralizes every integer power of \(g\).
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem closedSubgroupGenerated_singleton_le_centralizerOf_zpow
[TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
(g : G) (n : ℤ) :
(ProCGroups.Generation.closedSubgroupGenerated (G := G) ({g} : Set G) : Subgroup G) ≤
centralizerOf (g ^ n)Every element in the closed subgroup topologically generated by \(x\) centralizes each integer power of \(x\).
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem mem_centralizerOf_zpow_of_mem_closedSubgroupGenerated
[TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
{x c : G} (n : ℤ)
(hc : c ∈ (ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) :
Subgroup G)) :
c ∈ centralizerOf (x ^ n)If a single element topologically generates the group, the centralizer of any of its powers is the corresponding closed cyclic subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Pointwise
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]theorem centralizerOf_zpow_eq_closedSubgroupGenerated_of_topologicallyGenerates
[TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
(x : G) (n : ℤ)
(hgen : ProCGroups.Generation.TopologicallyGenerates (G := G) ({x} : Set G)) :
centralizerOf (x ^ n) =
(ProCGroups.Generation.closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G)