Module

ChangedUniformizer.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.ChangedUniformizer

17 declarations indexed from sourceView source ↗

Module documentation

Unit changes of a standard Lubin--Tate uniformizer

For a local field F, a chosen uniformizer π, and a valuation-ring unit u, the product uπ is again a uniformizer. Consequently all of the standard finite-level Lubin--Tate constructions are available for uπ.

This file packages that elementary, characteristic-independent part of the changed-uniformizer norm argument. In particular, the negative primitive generator at the changed level has norm uπ. It also records the cancellation step saying that, inside the norm subgroup of the original π-level, membership of uπ is equivalent to membership of u, since π is already a norm.

The remaining comparison between the π-level and the uπ-level requires an actual finite-level intertwining equivalence; no such equivalence is assumed here.

Imports12

Imported by7

def

standardLubinTateChangedUniformizer

L52 ↗

LubinTate.standardLubinTateChangedUniformizer

Documentation

The unit change uπ of a chosen integral uniformizer.

Source context 5 commands

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

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

Lean source · statement

def standardLubinTateChangedUniformizer
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    (u : F.valuationSubringˣ) :
    F.valuationSubring

theorem

standardLubinTateChangedUniformizer_eq_unit_mul

L60 ↗

LubinTate.standardLubinTateChangedUniformizer_eq_unit_mul

Documentation

The changed parameter is literally the unit factor times the original uniformizer.

Source context 5 commands

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

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

Lean source · statement

theorem standardLubinTateChangedUniformizer_eq_unit_mul
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    (u : F.valuationSubringˣ) :
    standardLubinTateChangedUniformizer F π u =
      (u : F.valuationSubring) * π

theorem

standardLubinTateChangedUniformizer_isUniformizer

L69 ↗

LubinTate.standardLubinTateChangedUniformizer_isUniformizer

Documentation

Multiplication by a valuation-ring unit preserves the uniformizer property.

Source context 5 commands

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

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

Lean source · statement

theorem standardLubinTateChangedUniformizer_isUniformizer
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) :
    F.toCompleteDVF.valuation.IsUniformizer
      (standardLubinTateChangedUniformizer F π u : K)

abbrev

standardLubinTateChangedLevelField

L80 ↗

LubinTate.standardLubinTateChangedLevelField

Documentation

The standard finite Lubin--Tate level attached to the changed uniformizer uπ.

Source context 5 commands

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

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

Lean source · statement

abbrev standardLubinTateChangedLevelField
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)

abbrev

standardLubinTateChangedLevelGenerator

L88 ↗

LubinTate.standardLubinTateChangedLevelGenerator

Documentation

The chosen primitive generator of the changed standard level.

Source context 5 commands

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

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

Lean source · statement

abbrev standardLubinTateChangedLevelGenerator
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    standardLubinTateChangedLevelField hπ u n

def

standardLubinTateChangedNormSubgroup

L97 ↗

LubinTate.standardLubinTateChangedNormSubgroup

Documentation

The local norm subgroup of the changed standard level.

Source context 5 commands

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

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

Lean source · statement

def standardLubinTateChangedNormSubgroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    Subgroup Kˣ

def

standardLubinTateUnitFactorFieldUnit

L106 ↗

LubinTate.standardLubinTateUnitFactorFieldUnit

Documentation

A valuation-ring unit regarded as a unit of the base field.

Source context 5 commands

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

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

Lean source · statement

def standardLubinTateUnitFactorFieldUnit
    (F : LocalField.{u, v} K) (u : F.valuationSubringˣ) :
    Kˣ

theorem

standardLubinTateUnitFactorFieldUnit_coe

L113 ↗

LubinTate.standardLubinTateUnitFactorFieldUnit_coe

Documentation

The unit-factor inclusion has the expected underlying field element.

Source context 5 commands

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

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

Lean source · statement

theorem standardLubinTateUnitFactorFieldUnit_coe
    (F : LocalField.{u, v} K) (u : F.valuationSubringˣ) :
    (standardLubinTateUnitFactorFieldUnit F u : K) =
      (u : F.valuationSubring)

def

standardLubinTateChangedUniformizerUnit

L121 ↗

LubinTate.standardLubinTateChangedUniformizerUnit

Documentation

The changed uniformizer, regarded as a nonzero base-field unit.

Source context 5 commands

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

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

Lean source · statement

def standardLubinTateChangedUniformizerUnit
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) :
    Kˣ

theorem

standardLubinTateChangedUniformizerUnit_coe

L131 ↗

LubinTate.standardLubinTateChangedUniformizerUnit_coe

Documentation

The changed uniformizer unit has underlying field element uπ.

Source context 5 commands

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

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

Lean source · statement

theorem standardLubinTateChangedUniformizerUnit_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) :
    (standardLubinTateChangedUniformizerUnit hπ u : K) =
      (standardLubinTateChangedUniformizer F π u : K)

theorem

standardLubinTateChangedUniformizerUnit_eq_unit_mul

L142 ↗

LubinTate.standardLubinTateChangedUniformizerUnit_eq_unit_mul

Documentation

In the base-field unit group, the changed uniformizer is the product of the included valuation-ring unit and the original uniformizer.

Source context 5 commands

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

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

Lean source · statement

theorem standardLubinTateChangedUniformizerUnit_eq_unit_mul
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) :
    standardLubinTateChangedUniformizerUnit hπ u =
      standardLubinTateUnitFactorFieldUnit F u *
        standardLubinTateBaseUniformizerUnit hπ

theorem

standardLubinTateUnitFactorFieldUnit_eq_changed_mul_uniformizer_inv

L154 ↗

LubinTate.standardLubinTateUnitFactorFieldUnit_eq_changed_mul_uniformizer_inv

Documentation

Equivalently, the unit factor is the quotient of the changed and original uniformizers.

Source context 5 commands

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

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

Lean source · statement

theorem standardLubinTateUnitFactorFieldUnit_eq_changed_mul_uniformizer_inv
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) :
    standardLubinTateUnitFactorFieldUnit F u =
      standardLubinTateChangedUniformizerUnit hπ u *
        (standardLubinTateBaseUniformizerUnit hπ)⁻¹

theorem

standardLubinTateChanged_norm_neg_levelGenerator

L165 ↗

LubinTate.standardLubinTateChanged_norm_neg_levelGenerator

Documentation

The negative primitive generator at the changed level has norm uπ.

Source context 5 commands

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

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

Lean source · statement

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

theorem

standardLubinTateChangedUniformizerUnit_mem_changedNormSubgroup

L177 ↗

LubinTate.standardLubinTateChangedUniformizerUnit_mem_changedNormSubgroup

Documentation

The changed uniformizer is an actual norm from its own standard finite level.

Source context 5 commands

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

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

Lean source · statement

theorem standardLubinTateChangedUniformizerUnit_mem_changedNormSubgroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    standardLubinTateChangedUniformizerUnit hπ u ∈
      standardLubinTateChangedNormSubgroup hπ u n

theorem

standardLubinTateChangedUniformizerUnit_mem_standardNormSubgroup_iff

L190 ↗

LubinTate.standardLubinTateChangedUniformizerUnit_mem_standardNormSubgroup_iff

Documentation

Inside the original level's norm subgroup, the changed uniformizer belongs exactly when its unit factor belongs. This is the cancellation step used after transporting the changed-level norm through a future finite-level intertwining equivalence.

Source context 5 commands

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

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

Lean source · statement

theorem
    standardLubinTateChangedUniformizerUnit_mem_standardNormSubgroup_iff
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    standardLubinTateChangedUniformizerUnit hπ u ∈
        standardLubinTateNormSubgroup hπ n ↔
      standardLubinTateUnitFactorFieldUnit F u ∈
        standardLubinTateNormSubgroup hπ n

theorem

standardLubinTateChangedUniformizerUnit_inv_mem_standardNormSubgroup_iff

L217 ↗

LubinTate.standardLubinTateChangedUniformizerUnit_inv_mem_standardNormSubgroup_iff

Documentation

The inverse changed uniformizer gives the same norm-membership test.

Source context 5 commands

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

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

Lean source · statement

theorem
    standardLubinTateChangedUniformizerUnit_inv_mem_standardNormSubgroup_iff
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateChangedUniformizerUnit hπ u)⁻¹ ∈
        standardLubinTateNormSubgroup hπ n ↔
      standardLubinTateUnitFactorFieldUnit F u ∈
        standardLubinTateNormSubgroup hπ n

theorem

standardLubinTateUnitFactorFieldUnit_mem_standardNormSubgroup_of_algEquiv

L243 ↗

LubinTate.standardLubinTateUnitFactorFieldUnit_mem_standardNormSubgroup_of_algEquiv

Documentation

An actual equivalence from the changed level to the original level transports the changed prime-element norm and therefore makes the unit factor a norm from the original level. This is the characteristic-free terminal step of a changed-uniformizer comparison; constructing e is the remaining substantive input.

Source context 5 commands

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

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

Lean source · statement

theorem
    standardLubinTateUnitFactorFieldUnit_mem_standardNormSubgroup_of_algEquiv
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (e : standardLubinTateChangedLevelField hπ u n ≃ₐ[K]
      standardLubinTateLevelField hπ n) :
    standardLubinTateUnitFactorFieldUnit F u ∈
      standardLubinTateNormSubgroup hπ n

Module documentation

Unit changes of a standard Lubin--Tate uniformizer

Declarations