Module

NormalBasisCharacterEigenvector.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.NormalBasisCharacterEigenvector

4 declarations indexed from sourceView source ↗

Module documentation

Nonzero character eigenvectors from a normal basis

An inverse-character weighted sum of the normal basis transforms by the character. Its coordinate at the identity automorphism is one, so the sum is nonzero, without any assumption on the characteristic or group order.

Imports1

Mathlib.FieldTheory.Galois.NormalBasis

Imported by2

def

normalBasisCharacterEigenvector

L27 ↗

LocalFieldTheory.DiscreteValuationField.normalBasisCharacterEigenvector

Documentation

The inverse-character weighted sum of the canonical normal basis.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def normalBasisCharacterEigenvector (χ : (L ≃ₐ[K] L) →* Kˣ) : L

theorem

normalBasisCharacterEigenvector_eigen

L31 ↗

LocalFieldTheory.DiscreteValuationField.normalBasisCharacterEigenvector_eigen

Documentation

Left translation of the normal basis gives the prescribed character action.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem normalBasisCharacterEigenvector_eigen (χ : (L ≃ₐ[K] L) →* Kˣ)
    (σ : L ≃ₐ[K] L) :
    σ (normalBasisCharacterEigenvector χ) =
      (χ σ : K) • normalBasisCharacterEigenvector χ

theorem

normalBasisCharacterEigenvector_ne_zero

L63 ↗

LocalFieldTheory.DiscreteValuationField.normalBasisCharacterEigenvector_ne_zero

Documentation

The identity coordinate of the weighted sum is one.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem normalBasisCharacterEigenvector_ne_zero (χ : (L ≃ₐ[K] L) →* Kˣ) :
    normalBasisCharacterEigenvector χ ≠ 0

theorem

exists_nonzero_characterEigenvector

L76 ↗

LocalFieldTheory.DiscreteValuationField.exists_nonzero_characterEigenvector

Documentation

Every base-field-valued character of a finite Galois group occurs in the field.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

theorem exists_nonzero_characterEigenvector (χ : (L ≃ₐ[K] L) →* Kˣ) :
    ∃ b : L, b ≠ 0 ∧ ∀ σ : L ≃ₐ[K] L, σ b = (χ σ : K) • b

Module documentation

Nonzero character eigenvectors from a normal basis

Declarations

normalBasisCharacterEigenvector

normalBasisCharacterEigenvector_eigen

normalBasisCharacterEigenvector_ne_zero

exists_nonzero_characterEigenvector