Module

AbsoluteCharacterAverage.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteCharacterAverage

4 declarations indexed from sourceView source ↗

Module documentation

Averaging absolute Galois characters

Average cyclic absolute characters over a finite relative Galois group. The average is invariant under the relative action and preserves a common orbit value when the group order is coprime to the character modulus.

Imports5

Nyll.GaloisCohomology.Topology.AbsoluteGaloisMap
Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteRestrictionConjugation
Mathlib.Data.ZMod.Basic
Mathlib.Topology.Instances.ZMod
Mathlib.Topology.Algebra.Ring.Basic

Imported by2

def

absoluteCharacterAverage

L28 ↗

KummerTheory.absoluteCharacterAverage

Documentation

Average a cyclic absolute character over the finite relative Galois group.

Source context 2 commands

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

namespace KummerTheory
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  [Fintype Gal(E/K)]

Lean source · statement

def absoluteCharacterAverage (n : ℕ)
    (χ : Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n)) :
    Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n)

theorem

absoluteCharacterAverage_map

L52 ↗

KummerTheory.absoluteCharacterAverage_map

Documentation

Averaging is invariant under every relative field automorphism.

Source context 2 commands

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

namespace KummerTheory
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  [Fintype Gal(E/K)]

Lean source · statement

theorem absoluteCharacterAverage_map (n : ℕ)
    (χ : Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n))
    (τ : Gal(E/K)) (σ : Gal(AlgebraicClosure E/E)) :
    absoluteCharacterAverage (K := K) n χ (Field.absoluteGaloisGroup.map τ.toRingHom σ) =
      absoluteCharacterAverage (K := K) n χ σ

theorem

absoluteCharacterAverage_conjugate

L75 ↗

KummerTheory.absoluteCharacterAverage_conjugate

Documentation

Averaging is invariant for the concrete conjugation action.

Source context 2 commands

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

namespace KummerTheory
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  [Fintype Gal(E/K)]

Lean source · statement

theorem absoluteCharacterAverage_conjugate (n : ℕ)
    (χ : Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n))
    (τ : Gal(E/K)) (σ : Gal(AlgebraicClosure E/E)) :
    absoluteCharacterAverage (K := K) n χ (absoluteGaloisConjugate τ.toRingEquiv σ) =
      absoluteCharacterAverage (K := K) n χ σ

theorem

absoluteCharacterAverage_eq_of_forall

L85 ↗

KummerTheory.absoluteCharacterAverage_eq_of_forall

Documentation

A common value on an orbit is preserved when the group order is invertible.

Source context 2 commands

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

namespace KummerTheory
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
  [Fintype Gal(E/K)]

Lean source · statement

theorem absoluteCharacterAverage_eq_of_forall (n : ℕ)
    (hn : (Fintype.card Gal(E/K)).Coprime n)
    (χ : Gal(AlgebraicClosure E/E) →ₜ* Multiplicative (ZMod n))
    (σ : Gal(AlgebraicClosure E/E)) (a : Multiplicative (ZMod n))
    (ha : ∀ δ : Gal(E/K), χ (Field.absoluteGaloisGroup.map δ.toRingHom σ) = a) :
    absoluteCharacterAverage (K := K) n χ σ = a

Module documentation

Averaging absolute Galois characters

Declarations

absoluteCharacterAverage

absoluteCharacterAverage_map

absoluteCharacterAverage_conjugate

absoluteCharacterAverage_eq_of_forall