Module

FiniteQuotientSeparation.lean

Nyll.AnabelianGeometry.CuspidalInertia.FiniteQuotientSeparation

4 declarations indexed from sourceView source ↗

Module documentation

Uniform finite-quotient separation of boundary generators

A fixed element that commutes with no member of a compact set still commutes with none of their images in one finite quotient. The quotient is chosen uniformly for the whole compact set, rather than separately for each generator. This is the compactness step used in the recognition of cuspidal inertia by open-subgroup abelianizations.

Imports2

Nyll.ProCGroups.ProC.OpenNormalSubgroups.Separation
Mathlib.Tactic.Push

Imported by4

def

conjugacySaturation

L28 ↗

AnabelianGeometry.CuspidalInertia.conjugacySaturation

Documentation

The union of the conjugates of a subset of a group.

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

def conjugacySaturation (S : Set G) : Set G

theorem

isCompact_conjugacySaturation

L33 ↗

AnabelianGeometry.CuspidalInertia.isCompact_conjugacySaturation

Documentation

Conjugating a compact subset through a compact group gives a compact subset.

Source context 4 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]
omit [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem isCompact_conjugacySaturation {S : Set G} (hS : IsCompact S) :
    IsCompact (conjugacySaturation S)

theorem

exists_openNormal_noncommuting

L50 ↗

AnabelianGeometry.CuspidalInertia.exists_openNormal_noncommuting

Documentation

A compact family of elements not commuting with z remains uniformly noncommuting in a single finite open-normal quotient.

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_openNormal_noncommuting (z : G) {S : Set G}
    (hS : IsCompact S) (h : ∀ s ∈ S, z * s ≠ s * z) :
    ∃ U : OpenNormalSubgroup G, ∀ s ∈ S,
      QuotientGroup.mk' (U : Subgroup G) z * QuotientGroup.mk' (U : Subgroup G) s ≠
        QuotientGroup.mk' (U : Subgroup G) s * QuotientGroup.mk' (U : Subgroup G) z

theorem

exists_openNormal_noncommuting_conjugates

L79 ↗

AnabelianGeometry.CuspidalInertia.exists_openNormal_noncommuting_conjugates

Documentation

A compact conjugacy-saturated family can be separated from commutation with z uniformly in a finite quotient.

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_openNormal_noncommuting_conjugates (z : G) {S : Set G}
    (hS : IsCompact S)
    (h : ∀ g : G, ∀ s ∈ S, z * (g * s * g⁻¹) ≠ (g * s * g⁻¹) * z) :
    ∃ U : OpenNormalSubgroup G, ∀ g : G, ∀ s ∈ S,
      QuotientGroup.mk' (U : Subgroup G) z *
          QuotientGroup.mk' (U : Subgroup G) (g * s * g⁻¹) ≠
        QuotientGroup.mk' (U : Subgroup G) (g * s * g⁻¹) *
          QuotientGroup.mk' (U : Subgroup G) z

Module documentation

Uniform finite-quotient separation of boundary generators

Declarations

conjugacySaturation

isCompact_conjugacySaturation

exists_openNormal_noncommuting

exists_openNormal_noncommuting_conjugates