ProCGroups.ProfiniteGrp.exists_ne_one_mem_center_of_quotient_central_lifts
Central elements in every finite quotient, each surviving a fixed open quotient, yield a nonidentity element of the actual profinite center.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.ProfiniteGrp
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [TotallyDisconnectedSpace G]Lean source · statement
theorem exists_ne_one_mem_center_of_quotient_central_lifts
(M : OpenNormalSubgroup G)
(hlift : ∀ N : OpenNormalSubgroup G, ∃ z : G, z ∉ (M : Subgroup G) ∧
∀ g : G, (g * z) * (z * g)⁻¹ ∈ (N : Subgroup G)) :
∃ z : G, z ∈ Subgroup.center G ∧ z ≠ 1