Module

RepresentationCharacterTwist.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.RepresentationCharacterTwist

2 declarations indexed from sourceView source ↗

Module documentation

Inverse-character twists and their actual invariant submodules

Character eigenvectors are fixed points of the representation twisted by the inverse character. The same construction is shared by averaging and by restriction to invariant submodules.

Imports1

Mathlib.RepresentationTheory.Invariants

Imported by3

def

inverseCharacterTwist

L23 ↗

LocalFieldTheory.DiscreteValuationField.inverseCharacterTwist

Documentation

Multiply the given action by the inverse of the given character.

Source context 2 commands

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

namespace LocalFieldTheory.DiscreteValuationField
variable {R Δ A : Type*} [CommRing R] [Group Δ]
  [AddCommGroup A] [Module R A]

Lean source · full declaration

def inverseCharacterTwist (χ : Δ →* Rˣ) (ρ : Representation R Δ A) :
    Representation R Δ A where
  toFun g := (((χ g)⁻¹ : Rˣ) : R) • ρ g
  map_one' := by
    simp only [map_one, inv_one, Units.val_one, one_smul]
  map_mul' g h := by
    ext a
    simp only [map_mul, mul_inv_rev, Units.val_mul, LinearMap.smul_apply,
      Module.End.mul_apply, map_smul, smul_smul]

theorem

inverseCharacterTwist_mem_invariants_iff

L34 ↗

LocalFieldTheory.DiscreteValuationField.inverseCharacterTwist_mem_invariants_iff