NYLL
Module

NormUniformizer.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.NormUniformizer
5 declarations indexed from sourceView source ↗

Module documentation

The uniformizer norm identity: the uniformizer norm in the equal-characteristic level field

For a primitive level-n+1 division point λ, its Eisenstein minimal polynomial has constant coefficient T. The power-basis norm formula therefore gives the norm identity N(-λ) = T.

Imports2
Imported by6

Declarations

theorem

equalCharacteristicLubinTatePrimitivePolynomial_coeff_zero

L36 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_coeff_zero
Documentation

The constant coefficient of the primitive division polynomial is the Laurent-series uniformizer T.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePolynomial_coeff_zero
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePolynomial F n).coeff 0 =
      equalCharacteristicLaurentUniformizer F
def

equalCharacteristicLubinTateLevelGenerator

L47 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelGenerator
Documentation

The chosen primitive point, regarded as the generator of its level field.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateLevelGenerator
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) : equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicLubinTateLevelGenerator_eq_powerBasis_gen

L55 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelGenerator_eq_powerBasis_gen
Documentation

States the theorem equalCharacteristicLubinTateLevelGenerator_eq_powerBasis_gen.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelGenerator_eq_powerBasis_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateLevelGenerator F n =
      (IntermediateField.adjoin.powerBasis
        (chosenEqualCharacteristicLubinTatePrimitiveRoot_isIntegral F n)).gen
theorem

algebraNorm_neg

L69 ↗
LubinTate.EqualCharacteristic.algebraNorm_neg
Documentation

The norm of a negative element, isolated from the large concrete Lubin--Tate level-field expression.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
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

equalCharacteristicLubinTate_norm_neg_levelGenerator

L77 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTate_norm_neg_levelGenerator
Documentation

The uniformizer norm identity, uniformizer part: the norm of the negative primitive division point is exactly T.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTate_norm_neg_levelGenerator
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Algebra.norm F.residueField⸨X⸩
        (-equalCharacteristicLubinTateLevelGenerator F n) =
      equalCharacteristicLaurentUniformizer F

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