NYLL
Module

ChangedUniformizerNormalization.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ChangedUniformizerNormalization
6 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: normalization of a changed Laurent uniformizer

The parameter aT, with a a power-series unit, is a prime element of the canonical Laurent integer ring. Consequently its inverse has normalized additive value one. This is the concrete prime certificate used in the changed-level norm argument.

Imports2
Imported by4

Declarations

def

equalCharacteristicChangedLaurentUniformizerInteger

L35 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerInteger
Documentation

The changed Laurent parameter in 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
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · full declaration
def equalCharacteristicChangedLaurentUniformizerInteger
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    letI := equalCharacteristicLaurentValuativeRel F
    (ValuativeRel.valuation F.residueField⸨X⸩).integer := by
  letI : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  exact powerSeriesEquivLaurentValuativeInteger F.residueField
    (equalCharacteristicChangedIntegralUniformizer F a)
theorem

equalCharacteristicChangedLaurentUniformizerInteger_coe

L46 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerInteger_coe
Documentation

States the theorem equalCharacteristicChangedLaurentUniformizerInteger_coe.

Source context 7 commands

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

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

equalCharacteristicChangedLaurentUniformizerInteger_irreducible

L57 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerInteger_irreducible
Documentation

Multiplying T by a power-series unit preserves primality in the canonical Laurent integer ring.

Source context 7 commands

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

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

equalCharacteristicChangedLaurentUniformizerUnit

L73 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerUnit
Documentation

The changed 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
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicChangedLaurentUniformizerUnit
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    F.residueField⸨X⸩ˣ
theorem

equalCharacteristicChangedLaurentUniformizerUnit_coe

L81 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerUnit_coe
Documentation

States the theorem equalCharacteristicChangedLaurentUniformizerUnit_coe.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries ValuativeRel WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicChangedLaurentUniformizerUnit_coe
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedLaurentUniformizerUnit F a).1 =
      equalCharacteristicChangedLaurentUniformizer F a
theorem

equalCharacteristicChangedLaurentUniformizerUnit_inv_valuationMap

L88 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerUnit_inv_valuationMap
Documentation

In the normalized additive convention, (aT)⁻¹ 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
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · full declaration
theorem equalCharacteristicChangedLaurentUniformizerUnit_inv_valuationMap
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    letI := equalCharacteristicLaurentValuativeRel F
    letI := equalCharacteristicLaurentIsNonarchimedeanLocalField F
    LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap F.residueField⸨X⸩
      (Additive.ofMul
        (equalCharacteristicChangedLaurentUniformizerUnit F a)⁻¹) = 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
    (equalCharacteristicChangedLaurentUniformizerInteger F a)
    (equalCharacteristicChangedLaurentUniformizerInteger_irreducible F a)
    (equalCharacteristicChangedLaurentUniformizerUnit F a) (by
      change equalCharacteristicChangedLaurentUniformizer F a =
        equalCharacteristicChangedLaurentUniformizer F a
      rfl)

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