NYLL
Module

ScalarCompatibility.lean

Nyll.ClassFieldTheory.LubinTate.Padic.ChangedUniformizerIntertwiner.ScalarCompatibility
2 declarations indexed from sourceView source ↗

Module documentation

Changed-uniformizer scalar compatibility

This module proves that the changed-uniformizer intertwiner commutes with every scalar endomorphism and identifies its coefficientwise Frobenius twist.

Imports1
Imported by3

Declarations

theorem

padicChangedUniformizerIntertwiner_endomorphism

L29 ↗
LubinTate.padicChangedUniformizerIntertwiner_endomorphism
Documentation

The semilinear changed-uniformizer comparison intertwines every scalar endomorphism. This is the formal-series compatibility used in the cyclotomic action formula for the Lubin--Tate character.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer
Lean source · statement
theorem padicChangedUniformizerIntertwiner_endomorphism
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.subst
        (padicCompletedMultiplicativeScalarEndomorphism p a)
        (padicChangedUniformizerIntertwiner p u) =
      PowerSeries.subst
        (padicChangedUniformizerIntertwiner p u)
        (padicCompletedChangedStandardScalarEndomorphism p u a)
theorem

padicChangedUniformizerIntertwiner_frobenius

L216 ↗
LubinTate.padicChangedUniformizerIntertwiner_frobenius
Documentation

Witt-vector Frobenius on the coefficients of the changed-uniformizer intertwiner is substitution by the multiplicative endomorphism attached to the unit changing the uniformizer.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer
Lean source · statement
theorem padicChangedUniformizerIntertwiner_frobenius
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.map WittVector.frobenius
        (padicChangedUniformizerIntertwiner p u) =
      PowerSeries.subst
        (padicCompletedMultiplicativeScalarEndomorphism p
          (u : (padicLocalField p).valuationSubring))
        (padicChangedUniformizerIntertwiner p u)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.