NYLL
Module

OpenSubgroupAvoidance.lean

Nyll.AnabelianGeometry.CuspidalInertia.OpenSubgroupAvoidance
2 declarations indexed from sourceView source ↗

Module documentation

Open subgroups avoiding compact families

Uniform noncommutation in a finite quotient gives an open subgroup containing one prescribed element and avoiding a whole compact family. Applying this to a conjugacy-saturated family makes the avoidance stable under conjugation.

Imports2
Imported by1

Declarations

theorem

exists_openSubgroup_mem_and_disjoint

L27 ↗
AnabelianGeometry.CuspidalInertia.exists_openSubgroup_mem_and_disjoint
Documentation

A compact family not commuting with z can be avoided by one open subgroup containing z.

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_mem_and_disjoint (z : G) {S : Set G}
    (hS : IsCompact S) (h : ∀ s ∈ S, z * s ≠ s * z) :
    ∃ H : OpenSubgroup G, z ∈ H ∧ Disjoint (H : Set G) S
theorem

exists_openSubgroup_mem_and_avoids_conjugates

L53 ↗
AnabelianGeometry.CuspidalInertia.exists_openSubgroup_mem_and_avoids_conjugates
Documentation

The subgroup can avoid every conjugate of every element of the family at once, while retaining the prescribed element.

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_mem_and_avoids_conjugates (z : G) {S : Set G}
    (hS : IsCompact S)
    (h : ∀ g : G, ∀ s ∈ S, z * (g * s * g⁻¹) ≠ (g * s * g⁻¹) * z) :
    ∃ H : OpenSubgroup G, z ∈ H ∧ ∀ g : G, ∀ s ∈ S, g * s * g⁻¹ ∉ H

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.