Module

CyclotomicTeichmullerCharacter.lean

Nyll.ValuedFieldTheory.LocalField.Padic.CyclotomicTeichmullerCharacter

4 declarations indexed from sourceView source ↗

Module documentation

The p-adic character of a finite p-th cyclotomic extension

The action on the p-th roots of unity lifts by Teichmüller representatives to p-adic units. It recovers the action on every p-power root present in the extension, without assuming that all p-power roots are present.

Imports3

Imported by3

def

primeCyclotomicTeichmullerCharacter

L28 ↗

LocalFieldTheory.DiscreteValuationField.primeCyclotomicTeichmullerCharacter

Documentation

The Teichmüller lift of the actual action on the p-th roots of unity.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
open ValuationTheory.DiscreteValuationField
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
  (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K L]

Lean source · statement

def primeCyclotomicTeichmullerCharacter : (L ≃ₐ[K] L) →* ℤ_[p]ˣ

theorem

primeCyclotomicTeichmullerCharacter_pow

L32 ↗

LocalFieldTheory.DiscreteValuationField.primeCyclotomicTeichmullerCharacter_pow

Documentation

The values of the finite cyclotomic character have order dividing p - 1.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
open ValuationTheory.DiscreteValuationField
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
  (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K L]

Lean source · statement

theorem primeCyclotomicTeichmullerCharacter_pow (σ : L ≃ₐ[K] L) :
    primeCyclotomicTeichmullerCharacter K L p σ ^ (p - 1) = 1

theorem

toZModPow_primeCyclotomicTeichmullerCharacter

L38 ↗

LocalFieldTheory.DiscreteValuationField.toZModPow_primeCyclotomicTeichmullerCharacter

Documentation

At every positive prime-power level present in the field, the lifted character agrees with the actual cyclotomic exponent.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
open ValuationTheory.DiscreteValuationField
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
  (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K L]

Lean source · statement

theorem toZModPow_primeCyclotomicTeichmullerCharacter (s : ℕ)
    {ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ (s + 1))) (σ : L ≃ₐ[K] L) :
    Units.map (PadicInt.toZModPow (s + 1)).toMonoidHom
      (primeCyclotomicTeichmullerCharacter K L p σ) = hζ.autToPow K σ

theorem

primeCyclotomicTeichmullerCharacter_spec

L55 ↗

LocalFieldTheory.DiscreteValuationField.primeCyclotomicTeichmullerCharacter_spec

Documentation

The lifted character gives the automorphism's action on every primitive prime-power root contained in the extension.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
open ValuationTheory.DiscreteValuationField
variable (K L : Type*) [Field K] [Field L] [Algebra K L]
  (p : ℕ) [Fact p.Prime] [IsCyclotomicExtension {p} K L]

Lean source · statement

theorem primeCyclotomicTeichmullerCharacter_spec (s : ℕ)
    {ζ : L} (hζ : IsPrimitiveRoot ζ (p ^ (s + 1))) (σ : L ≃ₐ[K] L) :
    ζ ^ (PadicInt.toZModPow (s + 1)
      (primeCyclotomicTeichmullerCharacter K L p σ : ℤ_[p])).val = σ ζ

Module documentation

The p-adic character of a finite p-th cyclotomic extension

Declarations

primeCyclotomicTeichmullerCharacter

primeCyclotomicTeichmullerCharacter_pow

toZModPow_primeCyclotomicTeichmullerCharacter

primeCyclotomicTeichmullerCharacter_spec