Module

NormalBasisSubgroupCharacterVector.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.NormalBasisSubgroupCharacterVector

6 declarations indexed from sourceView source ↗

Module documentation

Subgroup character vectors with a prescribed failure of the full action

As in the normal-basis character eigenvector construction, inverse-character coefficients weight the actual canonical normal basis. Here the coefficients are supported only on a subgroup. This vector transforms by the character on that subgroup, while an automorphism outside it moves the support away from the identity. Its identity coordinate distinguishes the two vectors. Neither a characteristic restriction nor normality of the subgroup is needed.

Imports7

Mathlib.FieldTheory.Galois.NormalBasis
Mathlib.LinearAlgebra.Basis.Defs
Mathlib.Algebra.Notation.Indicator
Mathlib.Algebra.Group.Basic
Mathlib.Algebra.Group.Subgroup.Defs
Mathlib.Algebra.BigOperators.Finsupp.Basic
Mathlib.Algebra.BigOperators.Group.Finset.Basic

Imported by2

def

normalBasisSubgroupCharacterVector

L36 ↗

LocalFieldTheory.DiscreteValuationField.normalBasisSubgroupCharacterVector

Documentation

The inverse-character weighted normal-basis sum supported on Δ.

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 normalBasisSubgroupCharacterVector (Δ : Subgroup Gal(L/K))
    (χ : Gal(L/K) →* Kˣ) : L

theorem

normalBasisSubgroupCharacterVector_repr

L44 ↗

LocalFieldTheory.DiscreteValuationField.normalBasisSubgroupCharacterVector_repr

Documentation

The coefficients are exactly the inverse character on the subgroup and zero outside it.

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 · full declaration

theorem normalBasisSubgroupCharacterVector_repr (Δ : Subgroup Gal(L/K))
    (χ : Gal(L/K) →* Kˣ) (δ : Gal(L/K)) :
    (IsGalois.normalBasis K L).repr (normalBasisSubgroupCharacterVector Δ χ) δ =
      (Δ : Set Gal(L/K)).indicator (fun τ => (((χ τ)⁻¹ : Kˣ) : K)) δ := by
  classical
  exact congrFun ((IsGalois.normalBasis K L).repr_sum_self
    ((Δ : Set Gal(L/K)).indicator (fun τ => (((χ τ)⁻¹ : Kˣ) : K)))) δ

theorem

map_normalBasisSubgroupCharacterVector

L52 ↗

LocalFieldTheory.DiscreteValuationField.map_normalBasisSubgroupCharacterVector

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 · full declaration

theorem map_normalBasisSubgroupCharacterVector (Δ : Subgroup Gal(L/K))
    (χ : Gal(L/K) →* Kˣ) (σ : Gal(L/K)) :
    σ (normalBasisSubgroupCharacterVector Δ χ) =
      ∑ δ : Gal(L/K),
        (Δ : Set Gal(L/K)).indicator (fun τ => (((χ τ)⁻¹ : Kˣ) : K)) δ •
          IsGalois.normalBasis K L (σ * δ) := by
  classical
  unfold normalBasisSubgroupCharacterVector
  rw [map_sum]
  apply Finset.sum_congr rfl
  intro δ _hδ
  rw [map_smul, IsGalois.normalBasis_apply δ,
    IsGalois.normalBasis_apply (σ * δ), AlgEquiv.mul_apply]

theorem

normalBasisSubgroupCharacterVector_eigen

L68 ↗

LocalFieldTheory.DiscreteValuationField.normalBasisSubgroupCharacterVector_eigen

Documentation

Left translation by a subgroup element multiplies the supported vector by the restricted character.

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 normalBasisSubgroupCharacterVector_eigen (Δ : Subgroup Gal(L/K))
    (χ : Gal(L/K) →* Kˣ) (σ : Δ) :
    (σ : Gal(L/K)) (normalBasisSubgroupCharacterVector Δ χ) =
      (χ (σ : Gal(L/K)) : K) • normalBasisSubgroupCharacterVector Δ χ

theorem

normalBasisSubgroupCharacterVector_not_eigen

L109 ↗

LocalFieldTheory.DiscreteValuationField.normalBasisSubgroupCharacterVector_not_eigen

Documentation

An automorphism outside the subgroup cannot have the prescribed character action on this vector: the identity coordinate becomes zero.

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 normalBasisSubgroupCharacterVector_not_eigen (Δ : Subgroup Gal(L/K))
    (χ : Gal(L/K) →* Kˣ) (g : Gal(L/K)) (hg : g ∉ Δ) :
    g (normalBasisSubgroupCharacterVector Δ χ) ≠
      (χ g : K) • normalBasisSubgroupCharacterVector Δ χ

theorem

exists_nonzero_subgroupCharacterEigenvector_not_eigen

L140 ↗

LocalFieldTheory.DiscreteValuationField.exists_nonzero_subgroupCharacterEigenvector_not_eigen

Documentation

The actual canonical normal basis supplies a nonzero restricted-character eigenvector on which any specified automorphism outside the subgroup fails to act by the full character.

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_subgroupCharacterEigenvector_not_eigen
    (Δ : Subgroup Gal(L/K)) (χ : Gal(L/K) →* Kˣ)
    (g : Gal(L/K)) (hg : g ∉ Δ) :
    ∃ b : L, b ≠ 0 ∧
      (∀ δ : Δ, (δ : Gal(L/K)) b = (χ (δ : Gal(L/K)) : K) • b) ∧
      g b ≠ (χ g : K) • b

Module documentation

Subgroup character vectors with a prescribed failure of the full action

Declarations

normalBasisSubgroupCharacterVector

normalBasisSubgroupCharacterVector_repr

map_normalBasisSubgroupCharacterVector

normalBasisSubgroupCharacterVector_eigen

normalBasisSubgroupCharacterVector_not_eigen

exists_nonzero_subgroupCharacterEigenvector_not_eigen