Module

NormUniformizer.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.NormUniformizer

3 declarations indexed from sourceView source ↗

Module documentation

Norm of a primitive standard Lubin--Tate point

The minimal polynomial of the chosen primitive level generator is the standard Eisenstein polynomial, whose constant coefficient is the base uniformizer. The power-basis norm formula therefore gives N(-lambda) = pi.

Imports2

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveUniformizer
Mathlib.RingTheory.Norm.Basic

Imported by2

theorem

algebraNorm_neg

L33 ↗

LubinTate.algebraNorm_neg

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem algebraNorm_neg
    {R S : Type*} [Field R] [Field S] [Algebra R S] (x : S) :
    Algebra.norm R (-x) =
      (-1) ^ Module.finrank R S * Algebra.norm R x

theorem

standardLubinTatePrimitivePolynomialOverField_coeff_zero

L43 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_coeff_zero

Documentation

The standard primitive polynomial over the base field has constant coefficient pi.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTatePrimitivePolynomialOverField_coeff_zero
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePrimitivePolynomialOverField F π n).coeff 0 =
      (π : K)

theorem

standardLubinTate_norm_neg_levelGenerator

L51 ↗

LubinTate.standardLubinTate_norm_neg_levelGenerator

Documentation

The norm of the negative primitive level generator is exactly the chosen base uniformizer.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTate_norm_neg_levelGenerator
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.norm K (-standardLubinTateLevelGenerator hπ n) = (π : K)

Module documentation

Norm of a primitive standard Lubin--Tate point

Declarations

algebraNorm_neg

standardLubinTatePrimitivePolynomialOverField_coeff_zero

standardLubinTate_norm_neg_levelGenerator