Module

PrimitiveRootTeichmullerCharacter.lean

Nyll.ValuedFieldTheory.LocalField.Padic.PrimitiveRootTeichmullerCharacter

5 declarations indexed from sourceView source ↗

Module documentation

Teichmüller characters from a specified primitive root

A primitive p-th root in a domain defines a p-adic character of its algebra automorphisms over any base ring. Its reduction records the actual action on that root. Restricting scalars preserves this character because it preserves the underlying automorphism and the specified root.

The ambient algebra need not be a cyclotomic extension. No finiteness, normality, characteristic-zero, or prime-to-p group-order assumption is required. A scalar tower is supplied once; no local instances are installed.

Imports6

Nyll.ValuedFieldTheory.LocalField.Padic.Teichmuller
Mathlib.Algebra.Algebra.Tower
Mathlib.NumberTheory.Padics.PadicIntegers
Mathlib.NumberTheory.Padics.RingHoms
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by2

theorem

primitiveRoot_autToPow_restrictScalars

L40 ↗

LocalFieldTheory.DiscreteValuationField.primitiveRoot_autToPow_restrictScalars

Documentation

The exponent on the same primitive root is unchanged by restriction of scalars.

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
universe u v w
section Restriction
variable (F : Type u) {M : Type v} {E : Type w}
    [CommRing F] [CommRing M] [CommRing E] [IsDomain E]
    [Algebra F M] [Algebra F E] [Algebra M E] [IsScalarTower F M E]

Lean source · statement

theorem primitiveRoot_autToPow_restrictScalars
    {n : ℕ} [NeZero n] {ζ : E} (hζ : IsPrimitiveRoot ζ n) (σ : E ≃ₐ[M] E) :
    hζ.autToPow F (σ.restrictScalars F) = hζ.autToPow M σ

def

primitiveRootTeichmullerCharacter

L58 ↗

LocalFieldTheory.DiscreteValuationField.primitiveRootTeichmullerCharacter

Documentation

The Teichmüller lift of the action on a specified primitive p-th root.

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
universe u v w
section Character
variable (F : Type u) {E : Type w}
    [CommRing F] [CommRing E] [IsDomain E] [Algebra F E]
    (p : ℕ) [Fact p.Prime] {ζ : E}

Lean source · statement

def primitiveRootTeichmullerCharacter (hζ : IsPrimitiveRoot ζ p) :
    (E ≃ₐ[F] E) →* ℤ_[p]ˣ

theorem

primitiveRootTeichmullerCharacter_spec

L63 ↗

LocalFieldTheory.DiscreteValuationField.primitiveRootTeichmullerCharacter_spec

Documentation

Reduction modulo p gives the actual action on the specified primitive root.

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
universe u v w
section Character
variable (F : Type u) {E : Type w}
    [CommRing F] [CommRing E] [IsDomain E] [Algebra F E]
    (p : ℕ) [Fact p.Prime] {ζ : E}

Lean source · statement

theorem primitiveRootTeichmullerCharacter_spec
    (hζ : IsPrimitiveRoot ζ p) (σ : E ≃ₐ[F] E) :
    ζ ^ (PadicInt.toZMod (primitiveRootTeichmullerCharacter F p hζ σ : ℤ_[p])).val =
      σ ζ

theorem

exists_primitiveRootTeichmullerCharacter_sub_natCast_eq_prime_mul

L76 ↗

LocalFieldTheory.DiscreteValuationField.exists_primitiveRootTeichmullerCharacter_sub_natCast_eq_prime_mul

Documentation

A specified exponent for the actual root action differs from the Teichmüller character by an actual multiple of p in the p-adic integers.

Source context 5 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
universe u v w
section Character
variable (F : Type u) {E : Type w}
    [CommRing F] [CommRing E] [IsDomain E] [Algebra F E]
    (p : ℕ) [Fact p.Prime] {ζ : E}

Lean source · statement

theorem exists_primitiveRootTeichmullerCharacter_sub_natCast_eq_prime_mul
    (hζ : IsPrimitiveRoot ζ p) (σ : E ≃ₐ[F] E)
    (a : ℕ) (ha : a < p) (hact : σ ζ = ζ ^ a) :
    ∃ c : ℤ_[p], (primitiveRootTeichmullerCharacter F p hζ σ : ℤ_[p]) -
      (a : ℤ_[p]) = (p : ℤ_[p]) * c

theorem

primitiveRootTeichmullerCharacter_comp_restrictScalars

L103 ↗

LocalFieldTheory.DiscreteValuationField.primitiveRootTeichmullerCharacter_comp_restrictScalars

Documentation

The actual characters agree along the inclusion of automorphisms obtained by restricting scalars through a single scalar tower.

Source context 3 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open Examples.Qp
universe u v w

Lean source · statement

theorem primitiveRootTeichmullerCharacter_comp_restrictScalars
    (F : Type u) {M : Type v} {E : Type w}
    [CommRing F] [CommRing M] [CommRing E] [IsDomain E]
    [Algebra F M] [Algebra F E] [Algebra M E] [IsScalarTower F M E]
    (p : ℕ) [Fact p.Prime] {ζ : E} (hζ : IsPrimitiveRoot ζ p) :
    (primitiveRootTeichmullerCharacter F p hζ).comp
        (AlgEquiv.restrictScalarsHom F : (E ≃ₐ[M] E) →* (E ≃ₐ[F] E)) =
      primitiveRootTeichmullerCharacter M p hζ

Module documentation

Teichmüller characters from a specified primitive root

Declarations

primitiveRoot_autToPow_restrictScalars

primitiveRootTeichmullerCharacter

primitiveRootTeichmullerCharacter_spec

exists_primitiveRootTeichmullerCharacter_sub_natCast_eq_prime_mul

primitiveRootTeichmullerCharacter_comp_restrictScalars