ProCGroups.quotient_eq_one_of_relative_fixedPoints
An element centralizing an open subgroup modulo a quotient kernel is trivial when relative fixed points vanish and open supergroups detect centralizers.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped commutatorElement
namespace ProCGroups
universe u vLean source · statement
theorem quotient_eq_one_of_relative_fixedPoints
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [TotallyDisconnectedSpace G]
{Q : Type v} [Group Q]
(q : G →* Q) (hq : Function.Surjective q)
(D : Subgroup G) [D.Normal] (hD : IsClosed (D : Set G))
(hfaith : ∀ N : OpenNormalSubgroup G, D ≤ (N : Subgroup G) →
∀ x : G, q x ∈ Subgroup.centralizer ((N : Subgroup G).map q : Set Q) →
x ∈ (N : Subgroup G))
(hfixed : ∀ U : OpenSubgroup G, ∀ x ∈ D,
q x ∈ Subgroup.centralizer ((U : Subgroup G).map q : Set Q) → q x = 1)
(U : OpenSubgroup G) (x : G)
(hx : q x ∈ Subgroup.centralizer ((U : Subgroup G).map q : Set Q)) :
q x = 1