NYLL
Module

LaurentUniformizerNormalization.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Existence.LaurentUniformizerNormalization
7 declarations indexed from sourceView source ↗

Module documentation

normalization of the equal-characteristic parameter

The Laurent-series valuation sends T to exp (-1). The power-series description of its integer ring makes T a genuine prime element, so the canonical normalized additive valuation sends T⁻¹ to 1.

Imports3
Imported by7

Declarations

theorem

equalCharacteristicLaurentUniformizer_laurentValuation

L35 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizer_laurentValuation
Documentation

The explicit Laurent parameter has Laurent-series value exp (-1).

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLaurentUniformizer_laurentValuation
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation F.residueField⸨X⸩ ℤᵐ⁰)
        (equalCharacteristicLaurentUniformizer F) =
      WithZero.exp (-1 : ℤ)
def

equalCharacteristicLaurentUniformizerInteger

L47 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizerInteger
Documentation

The Laurent parameter in the canonical integer ring determined by the native Laurent valuation.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
Lean source · full declaration
def equalCharacteristicLaurentUniformizerInteger
    (F : LocalField.{u, v} K) :
    letI := equalCharacteristicLaurentValuativeRel F
    (ValuativeRel.valuation F.residueField⸨X⸩).integer := by
  letI : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  exact powerSeriesEquivLaurentValuativeInteger F.residueField
    (PowerSeries.X : F.residueField⟦X⟧)
theorem

equalCharacteristicLaurentUniformizerInteger_coe

L58 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizerInteger_coe
Documentation

States the theorem equalCharacteristicLaurentUniformizerInteger_coe.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
Lean source · full declaration
theorem equalCharacteristicLaurentUniformizerInteger_coe
    (F : LocalField.{u, v} K) :
    letI := equalCharacteristicLaurentValuativeRel F
    (equalCharacteristicLaurentUniformizerInteger F).1 =
      equalCharacteristicLaurentUniformizer F := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  rfl
theorem

equalCharacteristicLaurentUniformizerInteger_irreducible

L69 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizerInteger_irreducible
Documentation

The explicit Laurent parameter is a prime element of the canonical integer ring.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
Lean source · full declaration
theorem equalCharacteristicLaurentUniformizerInteger_irreducible
    (F : LocalField.{u, v} K) :
    letI := equalCharacteristicLaurentValuativeRel F
    Irreducible (equalCharacteristicLaurentUniformizerInteger F) := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  change Irreducible
    (powerSeriesEquivLaurentValuativeInteger F.residueField
      (PowerSeries.X : F.residueField⟦X⟧))
  exact PowerSeries.X_irreducible.map
    (powerSeriesEquivLaurentValuativeInteger F.residueField)
def

equalCharacteristicLaurentUniformizerUnit

L82 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizerUnit
Documentation

The Laurent parameter as a nonzero field unit.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLaurentUniformizerUnit
    (F : LocalField.{u, v} K) : F.residueField⸨X⸩ˣ
theorem

equalCharacteristicLaurentUniformizerUnit_coe

L92 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizerUnit_coe
Documentation

States the theorem equalCharacteristicLaurentUniformizerUnit_coe.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLaurentUniformizerUnit_coe
    (F : LocalField.{u, v} K) :
    (equalCharacteristicLaurentUniformizerUnit F).1 =
      equalCharacteristicLaurentUniformizer F
theorem

equalCharacteristicLaurentUniformizerUnit_inv_valuationMap

L100 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizerUnit_inv_valuationMap
Documentation

In the normalized additive convention used here, the inverse Laurent parameter has value one.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
Lean source · full declaration
theorem equalCharacteristicLaurentUniformizerUnit_inv_valuationMap
    (F : LocalField.{u, v} K) :
    letI := equalCharacteristicLaurentValuativeRel F
    letI := equalCharacteristicLaurentIsNonarchimedeanLocalField F
    LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap F.residueField⸨X⸩
      (Additive.ofMul (equalCharacteristicLaurentUniformizerUnit F)⁻¹) = 1 := by
  let L := F.residueField⸨X⸩
  let : ValuativeRel L := equalCharacteristicLaurentValuativeRel F
  let : IsNonarchimedeanLocalField L :=
    equalCharacteristicLaurentIsNonarchimedeanLocalField F
  rw [LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap_apply]
  exact LocalFieldTheory.v_integerRingIrreducibleFieldUnit_inv L
    (equalCharacteristicLaurentUniformizerInteger F)
    (equalCharacteristicLaurentUniformizerInteger_irreducible F)
    (equalCharacteristicLaurentUniformizerUnit F) (by
      change equalCharacteristicLaurentUniformizer F =
        equalCharacteristicLaurentUniformizer F
      rfl)

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