Nyll.AnabelianGeometry.CuspidalInertia.CharacterExtension

Module documentation

Extending characters with compact vanishing conditions

A continuous discrete-valued character of a closed subgroup extends to an open overgroup. If it vanishes on the intersection with a compact family, the extension can be chosen to vanish on that family's entire intersection with the open overgroup. This is the character separation step in the open-subgroup criterion for inertia.

theorem

exists_openSubgroup_character_extension

L29 ↗

AnabelianGeometry.CuspidalInertia.exists_openSubgroup_character_extension

Documentation

Extend a closed-subgroup character to an open overgroup, preserving vanishing on a prescribed compact family.

Source context 4 commands

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

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

Lean source · statement

theorem exists_openSubgroup_character_extension (H : ClosedSubgroup G)
    (χ : H →* A) (hχ : Continuous χ) {S : Set G} (hS : IsCompact S)
    (hvan : ∀ h : H, (h : G) ∈ S → χ h = 1) :
    ∃ (V : OpenSubgroup G) (hHV : (H : Subgroup G) ≤ (V : Subgroup G))
      (ψ : V →* A), Continuous ψ ∧
      (∀ h : H, ψ ⟨h, hHV h.property⟩ = χ h) ∧
      ∀ s : V, (s : G) ∈ S → ψ s = 1

Module documentation

Extending characters with compact vanishing conditions

Declarations

exists_openSubgroup_character_extension