Nyll.AnabelianGeometry.CuspidalInertia.AbelianDetection

Module documentation

Detecting elements in relative open-subgroup abelianizations

A nonidentity element of a closed abelian subgroup disjoint from a compact family away from the identity survives in the abelianization of some open overgroup, even after killing the compact family. The proof constructs a continuous finite character and therefore also separates from the closed relation subgroup, not only from its abstract group-theoretic closure.

theorem

exists_openSubgroup_relative_abelianization_detects

L29 ↗

AnabelianGeometry.CuspidalInertia.exists_openSubgroup_relative_abelianization_detects

Documentation

An element in a closed abelian subgroup can be detected by an open relative abelianization when the compact family meets that subgroup only at one.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AnabelianGeometry.CuspidalInertia
universe u
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem exists_openSubgroup_relative_abelianization_detects
    (H : ClosedSubgroup G) (hcomm : ∀ x y : H, x * y = y * x)
    {S : Set G} (hS : IsCompact S)
    (hinter : ∀ h : H, (h : G) ∈ S → h = 1)
    (w : H) (hw : w ≠ 1) :
    ∃ (V : OpenSubgroup G) (hwV : (w : G) ∈ V),
      (⟨w, hwV⟩ : V) ∉
        (Subgroup.closure {s : (V : Subgroup G) | (s : G) ∈ S} ⊔
          commutator (V : Subgroup G)).topologicalClosure

Module documentation

Detecting elements in relative open-subgroup abelianizations

Declarations

exists_openSubgroup_relative_abelianization_detects