Nyll.ProCGroups.Cohomology.RelativeNakayama

Module documentation

Relative Nakayama characters for pro-p groups

A strict inclusion of closed ambient-normal subgroups of a pro-p group can be detected by a nonzero continuous ZMod p-valued character. The construction separates one element in a finite p-group quotient and applies the finite invariant-character theorem there.

theorem

relativeNakayama_character

L33 ↗

ClassFieldTower.ProP.relativeNakayama_character

Documentation

Relative pro-p Nakayama in character form: a strict inclusion of closed ambient-normal subgroups is detected by a nonzero continuous character which vanishes on the smaller subgroup and is invariant under conjugation by the ambient group.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC
noncomputable section
universe u

Lean source · statement

theorem relativeNakayama_character
    {p : ℕ} [Fact p.Prime]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (hF : HasPGroupOpenNormalBasis p F)
    (K R : ClosedSubgroup F) [K.Normal] [R.Normal] (hKR : K < R) :
    ∃ χ : R →ₜ* Multiplicative (ZMod p),
      χ ≠ 1 ∧
        (∀ k : K, χ ⟨k, hKR.le k.2⟩ = 1) ∧
        ∀ (f : F) (r : R), χ (MulAut.conjNormal f r) = χ r

Module documentation

Relative Nakayama characters for pro-p groups

Declarations

relativeNakayama_character