NYLL
Module

ClosedSubgroupSeparation.lean

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

Module documentation

Open neighborhoods of closed subgroups avoiding compact sets

A closed subgroup of a profinite group has an open overgroup avoiding any prescribed compact set disjoint from it. A single finite quotient separates the entire compact set, so the construction also handles all conjugates at once.

Imports1
Imported by1

Declarations

theorem

exists_openSubgroup_overgroup_disjoint

L25 ↗
AnabelianGeometry.CuspidalInertia.exists_openSubgroup_overgroup_disjoint
Documentation

Separate a closed subgroup and a disjoint compact set by an open overgroup.

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_overgroup_disjoint (H : ClosedSubgroup G) {S : Set G}
    (hS : IsCompact S) (hd : Disjoint (H : Set G) S) :
    ∃ V : OpenSubgroup G, (H : Subgroup G) ≤ (V : Subgroup G) ∧
      Disjoint (V : Set G) S
theorem

exists_openSubgroup_overgroup_avoids_conjugates

L64 ↗
AnabelianGeometry.CuspidalInertia.exists_openSubgroup_overgroup_avoids_conjugates
Documentation

An open overgroup can avoid an entire compact family of conjugacy classes.

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

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