Module

FiniteInvariantCharacter.lean

Nyll.ProCGroups.Cohomology.FiniteInvariantCharacter

3 declarations indexed from sourceView source ↗

Module documentation

Conjugation-invariant characters of finite p-groups

This file constructs nontrivial ZMod p-valued multiplicative characters on nontrivial normal subgroups of finite p-groups. Averaging is replaced by the fixed-point theorem for finite p-group actions, so the resulting character is invariant under ambient conjugation.

The relative form additionally makes the character vanish on a prescribed proper normal subgroup. It is the finite quotient input for relative pro-p Nakayama arguments.

Imports3

Nyll.ProCGroups.ProP.FinitePGroupMaximal
Mathlib.Algebra.Group.Hom.Instances
Mathlib.GroupTheory.GroupAction.DomAct.Basic

Imported by3

theorem

exists_nontrivial_character_of_finite_pGroup

L30 ↗

ClassFieldTower.ProP.exists_nontrivial_character_of_finite_pGroup

Source context 4 commands

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

open MulAction
namespace ClassFieldTower.ProP
noncomputable section
universe u

Lean source · statement

theorem exists_nontrivial_character_of_finite_pGroup
    {p : Nat} [Fact p.Prime]
    {N : Type u} [Group N] [Finite N] [Nontrivial N]
    (hN : IsPGroup p N) :
    ∃ χ : N →* Multiplicative (ZMod p), χ ≠ 1

theorem

exists_nontrivial_conjugationInvariant_character_finite

L64 ↗

ClassFieldTower.ProP.exists_nontrivial_conjugationInvariant_character_finite

Documentation

A nontrivial normal subgroup of a finite p-group admits a nontrivial character to Multiplicative (ZMod p) that is invariant under conjugation by the ambient group.

Source context 4 commands

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

open MulAction
namespace ClassFieldTower.ProP
noncomputable section
universe u

Lean source · statement

theorem exists_nontrivial_conjugationInvariant_character_finite
    {p : Nat} [Fact p.Prime]
    {P : Type u} [Group P] [Finite P]
    (hP : IsPGroup p P)
    (N : Subgroup P) [N.Normal] (hN : N ≠ (⊥ : Subgroup P)) :
    ∃ χ : N →* Multiplicative (ZMod p),
      χ ≠ 1 ∧ ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n

theorem

exists_conjugationInvariant_character_killing_of_lt_finite

L119 ↗

ClassFieldTower.ProP.exists_conjugationInvariant_character_killing_of_lt_finite

Documentation

If K < N are normal subgroups of a finite p-group, there is a nontrivial ambient conjugation-invariant character of N that vanishes on K.

Source context 4 commands

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

open MulAction
namespace ClassFieldTower.ProP
noncomputable section
universe u

Lean source · statement

theorem exists_conjugationInvariant_character_killing_of_lt_finite
    {p : Nat} [Fact p.Prime]
    {P : Type u} [Group P] [Finite P]
    (hP : IsPGroup p P)
    (K N : Subgroup P) [K.Normal] [N.Normal] (hKN : K < N) :
    ∃ χ : N →* Multiplicative (ZMod p),
      χ ≠ 1 ∧
        (∀ k : K, χ ⟨k, hKN.le k.2⟩ = 1) ∧
        ∀ (g : P) (n : N), χ (MulAut.conjNormal g n) = χ n

Module documentation

Conjugation-invariant characters of finite p-groups

Declarations

exists_nontrivial_character_of_finite_pGroup

exists_nontrivial_conjugationInvariant_character_finite

exists_conjugationInvariant_character_killing_of_lt_finite