Module

CharacterAveraging.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.CharacterAveraging

6 declarations indexed from sourceView source ↗

Module documentation

Lifting character eigenvectors by averaging

The inverse character twist turns character eigenvectors into invariants. The standard averaging projection commutes with an actual intertwining map, so every eigenvector in its image has an eigenvector preimage.

Imports2

Nyll.ValuedFieldTheory.LocalField.Analytic.RepresentationCharacterTwist
Mathlib.RepresentationTheory.Invariants

Imported by2

def

characterAverage

L30 ↗

LocalFieldTheory.DiscreteValuationField.characterAverage

Documentation

The averaging projection onto vectors transforming by χ.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {R Δ A B : Type*} [CommRing R] [Group Δ]
  [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B]
variable [Fintype Δ] [Invertible (Fintype.card Δ : R)]

Lean source · statement

def characterAverage (χ : Δ →* Rˣ) (ρ : Representation R Δ A) : A →ₗ[R] A

theorem

characterAverage_apply

L34 ↗

LocalFieldTheory.DiscreteValuationField.characterAverage_apply

Documentation

The character projection is the usual inverse-character weighted average.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {R Δ A B : Type*} [CommRing R] [Group Δ]
  [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B]
variable [Fintype Δ] [Invertible (Fintype.card Δ : R)]

Lean source · statement

theorem characterAverage_apply (χ : Δ →* Rˣ) (ρ : Representation R Δ A) (a : A) :
    characterAverage χ ρ a =
      ⅟(Fintype.card Δ : R) • ∑ g : Δ, (((χ g)⁻¹ : Rˣ) : R) • ρ g a

theorem

characterAverage_eigen

L42 ↗

LocalFieldTheory.DiscreteValuationField.characterAverage_eigen

Documentation

The weighted average transforms by the original character.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {R Δ A B : Type*} [CommRing R] [Group Δ]
  [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B]
variable [Fintype Δ] [Invertible (Fintype.card Δ : R)]

Lean source · statement

theorem characterAverage_eigen (χ : Δ →* Rˣ) (ρ : Representation R Δ A) (a : A)
    (g : Δ) :
    ρ g (characterAverage χ ρ a) = (χ g : R) • characterAverage χ ρ a

theorem

characterAverage_eq_self

L49 ↗

LocalFieldTheory.DiscreteValuationField.characterAverage_eq_self

Documentation

Averaging fixes every character eigenvector.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {R Δ A B : Type*} [CommRing R] [Group Δ]
  [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B]
variable [Fintype Δ] [Invertible (Fintype.card Δ : R)]

Lean source · statement

theorem characterAverage_eq_self (χ : Δ →* Rˣ) (ρ : Representation R Δ A) (a : A)
    (ha : ∀ g : Δ, ρ g a = (χ g : R) • a) :
    characterAverage χ ρ a = a

theorem

map_characterAverage

L56 ↗

LocalFieldTheory.DiscreteValuationField.map_characterAverage

Documentation

Intertwining maps commute with the character projection.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {R Δ A B : Type*} [CommRing R] [Group Δ]
  [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B]
variable [Fintype Δ] [Invertible (Fintype.card Δ : R)]

Lean source · statement

theorem map_characterAverage (χ : Δ →* Rˣ) {ρ : Representation R Δ A}
    {σ : Representation R Δ B} (f : Representation.IntertwiningMap ρ σ) (a : A) :
    f (characterAverage χ ρ a) = characterAverage χ σ (f a)

theorem

exists_eigen_preimage

L64 ↗

LocalFieldTheory.DiscreteValuationField.exists_eigen_preimage

Documentation

A character eigenvector in the image of an intertwining map has an eigenvector preimage, obtained by averaging any preimage.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {R Δ A B : Type*} [CommRing R] [Group Δ]
  [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B]
variable [Fintype Δ] [Invertible (Fintype.card Δ : R)]

Lean source · statement

theorem exists_eigen_preimage (χ : Δ →* Rˣ) {ρ : Representation R Δ A}
    {σ : Representation R Δ B} (f : Representation.IntertwiningMap ρ σ) (b : B)
    (hb : ∀ g : Δ, σ g b = (χ g : R) • b) (hrange : b ∈ Set.range f) :
    ∃ a : A, f a = b ∧ ∀ g : Δ, ρ g a = (χ g : R) • a

Module documentation

Lifting character eigenvectors by averaging

Declarations

characterAverage

characterAverage_apply

characterAverage_eigen

characterAverage_eq_self

map_characterAverage

exists_eigen_preimage