Module

HigherUnitLevelEquiv.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.HigherUnitLevelEquiv

25 declarations indexed from sourceView source ↗

Module documentation

Stability of a standard Lubin--Tate level under a deep unit change

This file develops the quantitative inputs for comparing the standard level attached to a uniformizer π with the standard level attached to uπ, when u is a sufficiently deep principal unit.

ChangedPrimitiveEvaluation supplies the first input: at depth n + 1, the changed primitive polynomial evaluated at the old primitive point has additive valuation at least (n + 2) d.

The new input proved here is the exact additive valuation of the derivative of the primitive polynomial at the distinguished primitive point. If

d = (q - 1) q^n,

then that valuation is

n d + (q - 2) q^n = (n + 1) d - q^n.

Together these are the two numerical terms in the root-product/Krasner comparison: the evaluation estimate controls the changed polynomial at the old primitive point, and the derivative exponent controls the product of the other changed-root displacements.

Imports8

Imported by3

theorem

standardLubinTatePrimitivePolynomial_map_levelCoefficientHom_splits

L63 ↗

LubinTate.standardLubinTatePrimitivePolynomial_map_levelCoefficientHom_splits

Documentation

Every integral primitive polynomial splits already over the valuation ring of its standard level. The finite unit parameters give as many distinct integral roots as the degree of the polynomial.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTatePrimitivePolynomial_map_levelCoefficientHom_splits
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    ((standardLubinTatePrimitivePolynomial F π n).map
      (standardLubinTateLevelCoefficientHom hπ n)).Splits

theorem

standardLubinTatePolynomialIterate_derivative_eval₂_succ

L154 ↗

LubinTate.standardLubinTatePolynomialIterate_derivative_eval₂_succ

Documentation

Evaluation of the derivative of a successor iterate is the old derivative value multiplied by q y^(q-1) + π, where y is the old iterate value.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTatePolynomialIterate_derivative_eval₂_succ
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n i : ℕ) :
    Polynomial.eval₂
        (standardLubinTateLevelCoefficientHom hπ n)
        (standardLubinTatePrimitivePointInteger hπ n)
        (standardLubinTatePolynomialIterate F π (i + 1)).derivative =
      (standardLubinTateLevelCoefficientHom hπ n
            (Nat.card F.residueField : F.valuationSubring) *
          standardLubinTatePrimitivePointIterateInteger hπ n i ^
            (Nat.card F.residueField - 1) +
        standardLubinTateLevelCoefficientHom hπ n π) *
      Polynomial.eval₂
        (standardLubinTateLevelCoefficientHom hπ n)
        (standardLubinTatePrimitivePointInteger hπ n)
        (standardLubinTatePolynomialIterate F π i).derivative

theorem

standardLubinTate_iterate_derivative_factor_addVal

L183 ↗

LubinTate.standardLubinTate_iterate_derivative_factor_addVal

Documentation

The derivative factor q y^(q-1) + π occurring at every iterate has the same additive valuation as the image of the base uniformizer.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTate_iterate_derivative_factor_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n i : ℕ) (hi : i ≤ n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTateLevelCoefficientHom hπ n
              (Nat.card F.residueField : F.valuationSubring) *
            standardLubinTatePrimitivePointIterateInteger hπ n i ^
              (Nat.card F.residueField - 1) +
          standardLubinTateLevelCoefficientHom hπ n π) =
      (((Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n : ℕ) : ℕ∞)

theorem

standardLubinTatePolynomialIterate_derivative_eval₂_addVal

L268 ↗

LubinTate.standardLubinTatePolynomialIterate_derivative_eval₂_addVal

Documentation

The derivative of the i-fold standard iterate at the primitive point has additive valuation i * d, where d = (q - 1) q^n.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTatePolynomialIterate_derivative_eval₂_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n i : ℕ) (hi : i ≤ n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (Polynomial.eval₂
          (standardLubinTateLevelCoefficientHom hπ n)
          (standardLubinTatePrimitivePointInteger hπ n)
          (standardLubinTatePolynomialIterate F π i).derivative) =
      ((i * ((Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n) : ℕ) : ℕ∞)

theorem

standardLubinTatePrimitivePolynomial_derivative_eval₂_addVal

L302 ↗

LubinTate.standardLubinTatePrimitivePolynomial_derivative_eval₂_addVal

Documentation

Exact derivative valuation of the integral primitive polynomial at the distinguished primitive point.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTatePrimitivePolynomial_derivative_eval₂_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (Polynomial.eval₂
          (standardLubinTateLevelCoefficientHom hπ n)
          (standardLubinTatePrimitivePointInteger hπ n)
          (standardLubinTatePrimitivePolynomial F π n).derivative) =
      ((n * ((Nat.card F.residueField - 1) *
              Nat.card F.residueField ^ n) +
          (Nat.card F.residueField - 2) *
              Nat.card F.residueField ^ n : ℕ) : ℕ∞)

theorem

standardLubinTatePrimitivePolynomial_map_levelCoefficientHom_derivative_addVal

L383 ↗

LubinTate.standardLubinTatePrimitivePolynomial_map_levelCoefficientHom_derivative_addVal

Documentation

Every integral root of the primitive polynomial in its standard level has the same derivative valuation as the distinguished primitive point.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTatePrimitivePolynomial_map_levelCoefficientHom_derivative_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ)
    {y : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring}
    (hy :
      y ∈
        ((standardLubinTatePrimitivePolynomial F π n).map
          (standardLubinTateLevelCoefficientHom hπ n)).roots) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (((standardLubinTatePrimitivePolynomial F π n).map
          (standardLubinTateLevelCoefficientHom hπ n)).derivative.eval y) =
      ((n * ((Nat.card F.residueField - 1) *
              Nat.card F.residueField ^ n) +
          (Nat.card F.residueField - 2) *
              Nat.card F.residueField ^ n : ℕ) : ℕ∞)

theorem

standardLubinTatePrimitivePolynomial_derivativeExponent_eq

L494 ↗

LubinTate.standardLubinTatePrimitivePolynomial_derivativeExponent_eq

Documentation

Arithmetic form of the derivative exponent used by the root-product comparison.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTatePrimitivePolynomial_derivativeExponent_eq
    (F : LocalField.{u, v} K) (n : ℕ) :
    n * ((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n) +
        (Nat.card F.residueField - 2) *
          Nat.card F.residueField ^ n =
      (n + 1) * ((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n) -
        Nat.card F.residueField ^ n

def

standardLubinTateChangedPrimitivePolynomialInCompositum

L521 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomialInCompositum

Documentation

The changed primitive polynomial after passing through the changed level and then into the common compositum valuation ring.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

def
    standardLubinTateChangedPrimitivePolynomialInCompositum
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateChangedLevelCompositumCompleteDVF
      hπ u n).valuationSubring[X]

def

standardLubinTateOriginalPrimitivePointInChangedLevelCompositum

L537 ↗

LubinTate.standardLubinTateOriginalPrimitivePointInChangedLevelCompositum

Documentation

The original distinguished primitive point in the common compositum valuation ring.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

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

def

standardLubinTateChangedPrimitivePointInCompositum

L549 ↗

LubinTate.standardLubinTateChangedPrimitivePointInCompositum

Documentation

The distinguished changed primitive point in the common compositum valuation ring.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

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

theorem

standardLubinTateChangedLevelCompositum_coefficientHom_eq

L563 ↗

LubinTate.standardLubinTateChangedLevelCompositum_coefficientHom_eq

Documentation

The two routes from base coefficients into the common compositum valuation ring agree.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateChangedLevelCompositum_coefficientHom_eq
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateChangedLevelToCompositumIntegerMap hπ u n).comp
        (standardLubinTateLevelCoefficientHom
          (standardLubinTateChangedUniformizer_isUniformizer hπ u) n) =
    (standardLubinTateLevelToChangedLevelCompositumIntegerMap
        hπ u n).comp
        (standardLubinTateLevelCoefficientHom hπ n)

theorem

standardLubinTateChangedPrimitivePolynomialInCompositum_monic

L606 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomialInCompositum_monic

Documentation

The changed primitive polynomial is monic in the common valuation ring.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTateChangedPrimitivePolynomialInCompositum_monic
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateChangedPrimitivePolynomialInCompositum
      hπ u n).Monic

theorem

standardLubinTateChangedPrimitivePolynomialInCompositum_splits

L621 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomialInCompositum_splits

Documentation

The changed primitive polynomial splits in the common valuation ring.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTateChangedPrimitivePolynomialInCompositum_splits
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateChangedPrimitivePolynomialInCompositum
      hπ u n).Splits

theorem

standardLubinTateChangedPrimitivePolynomialInCompositum_natDegree_ne_zero

L634 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomialInCompositum_natDegree_ne_zero

Documentation

The changed primitive polynomial remains nonconstant in the common valuation ring.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateChangedPrimitivePolynomialInCompositum_natDegree_ne_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateChangedPrimitivePolynomialInCompositum
      hπ u n).natDegree ≠ 0

theorem

standardLubinTateChangedPrimitivePolynomialInCompositum_eval_original

L667 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomialInCompositum_eval_original

Documentation

Evaluation in the common compositum agrees with first evaluating at the original primitive point and then applying the original-level valuation-ring inclusion.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateChangedPrimitivePolynomialInCompositum_eval_original
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateChangedPrimitivePolynomialInCompositum
        hπ u n).eval
        (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
          hπ u n) =
      standardLubinTateLevelToChangedLevelCompositumIntegerMap hπ u n
        (Polynomial.eval₂
          (standardLubinTateLevelCoefficientHom hπ n)
          (standardLubinTatePrimitivePointInteger hπ n)
          (standardLubinTatePrimitivePolynomial F
            (standardLubinTateChangedUniformizer F π u) n))

theorem

standardLubinTateChangedPrimitivePolynomialInCompositum_eval_addVal_ge

L690 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomialInCompositum_eval_addVal_ge

Documentation

The changed-polynomial evaluation lower bound after transport to the common compositum.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateChangedPrimitivePolynomialInCompositum_eval_addVal_ge
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    ((standardLubinTateLevelToChangedLevelCompositumRamificationIndex
          hπ u n *
        (((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n) * (n + 2)) : ℕ) : ℕ∞) ≤
      IsDiscreteValuationRing.addVal
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring
        ((standardLubinTateChangedPrimitivePolynomialInCompositum
          hπ u n).eval
          (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
            hπ u n))

theorem

standardLubinTateChangedPrimitivePolynomialInCompositum_derivative_addVal

L731 ↗

LubinTate.standardLubinTateChangedPrimitivePolynomialInCompositum_derivative_addVal

Documentation

Every changed root in the compositum has the transported exact derivative valuation.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateChangedPrimitivePolynomialInCompositum_derivative_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    {beta :
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuationSubring}
    (hbeta :
      beta ∈
        (standardLubinTateChangedPrimitivePolynomialInCompositum
          hπ u n).roots) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring
        ((standardLubinTateChangedPrimitivePolynomialInCompositum
          hπ u n).derivative.eval beta) =
      standardLubinTateChangedLevelToCompositumRamificationIndex hπ u n •
        ((n * ((Nat.card F.residueField - 1) *
                Nat.card F.residueField ^ n) +
            (Nat.card F.residueField - 2) *
                Nat.card F.residueField ^ n : ℕ) : ℕ∞)

theorem

standardLubinTateLevelToChangedLevelCompositumRamificationIndex_pos

L805 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositumRamificationIndex_pos

Documentation

The relative ramification index of the original level in the common compositum is positive.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateLevelToChangedLevelCompositumRamificationIndex_pos
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    0 <
      standardLubinTateLevelToChangedLevelCompositumRamificationIndex
        hπ u n

theorem

exists_standardLubinTateChangedPrimitiveRootInCompositum_close

L845 ↗

LubinTate.exists_standardLubinTateChangedPrimitiveRootInCompositum_close

Documentation

At principal-unit depth n + 1, the changed primitive polynomial has a root in the common compositum which is closer to the old primitive point than the transported level-n Galois displacement bound.

The root-product estimate first gives the stronger lower bound e * q^(n+1) for the distance. Here e is the relative ramification index of the original level in the compositum.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    exists_standardLubinTateChangedPrimitiveRootInCompositum_close
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    ∃ beta :
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring,
      beta ∈
          (standardLubinTateChangedPrimitivePolynomialInCompositum
            hπ u n).roots ∧
        ((standardLubinTateLevelToChangedLevelCompositumRamificationIndex
              hπ u n *
            Nat.card F.residueField ^ n : ℕ) : ℕ∞) <
          IsDiscreteValuationRing.addVal
            (standardLubinTateChangedLevelCompositumCompleteDVF
              hπ u n).valuationSubring
            (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
                hπ u n -
              beta)

theorem

standardLubinTateOriginalPrimitivePointInChangedLevelCompositum_displacement_addVal_le

L996 ↗

LubinTate.standardLubinTateOriginalPrimitivePointInChangedLevelCompositum_displacement_addVal_le

Documentation

A nontrivial displacement of the old primitive point by a Galois automorphism of the common compositum is bounded by the old level-n bound, scaled by the relative ramification index.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateOriginalPrimitivePointInChangedLevelCompositum_displacement_addVal_le
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (σ :
      Gal(standardLubinTateChangedLevelCompositumField hπ u n/K))
    (hne :
      valuationSubringAutOfUniqueExtension
          (standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueDVFValuationExtension
            hπ u n)
          σ
          (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
            hπ u n) ≠
        standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
          hπ u n) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring
        (valuationSubringAutOfUniqueExtension
            (standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueDVFValuationExtension
              hπ u n)
            σ
            (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
              hπ u n) -
          standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
            hπ u n) ≤
      ((standardLubinTateLevelToChangedLevelCompositumRamificationIndex
            hπ u n *
          Nat.card F.residueField ^ n : ℕ) : ℕ∞)

theorem

standardLubinTateChangedPrimitiveRootInCompositum_mem_changedRestrict

L1112 ↗

LubinTate.standardLubinTateChangedPrimitiveRootInCompositum_mem_changedRestrict

Documentation

A changed primitive root in the compositum lies in the restricted copy of the changed standard level.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateChangedPrimitiveRootInCompositum_mem_changedRestrict
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    {beta :
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuationSubring}
    (hbeta :
      beta ∈
        (standardLubinTateChangedPrimitivePolynomialInCompositum
          hπ u n).roots) :
    (beta : standardLubinTateChangedLevelCompositumField hπ u n) ∈
      IntermediateField.restrict
        (le_sup_right :
          standardLubinTateChangedLevelField hπ u n ≤
            standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateOriginalPrimitivePointInChangedLevelCompositum_fixed_of_fixed_close

L1177 ↗

LubinTate.standardLubinTateOriginalPrimitivePointInChangedLevelCompositum_fixed_of_fixed_close

Documentation

A compositum automorphism fixing a sufficiently close changed root also fixes the old primitive point.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateOriginalPrimitivePointInChangedLevelCompositum_fixed_of_fixed_close
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    {beta :
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuationSubring}
    (hclose :
      ((standardLubinTateLevelToChangedLevelCompositumRamificationIndex
              hπ u n *
            Nat.card F.residueField ^ n : ℕ) : ℕ∞) <
        IsDiscreteValuationRing.addVal
          (standardLubinTateChangedLevelCompositumCompleteDVF
            hπ u n).valuationSubring
          (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
              hπ u n -
            beta))
    (σ :
      Gal(standardLubinTateChangedLevelCompositumField hπ u n/K))
    (hfix :
      σ (beta :
        standardLubinTateChangedLevelCompositumField hπ u n) =
        (beta :
          standardLubinTateChangedLevelCompositumField hπ u n)) :
    σ
        (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
          hπ u n :
          standardLubinTateChangedLevelCompositumField hπ u n) =
      (standardLubinTateOriginalPrimitivePointInChangedLevelCompositum
        hπ u n :
        standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateHigherUnit_restrict_changedLevel_eq_originalLevel

L1239 ↗

LubinTate.standardLubinTateHigherUnit_restrict_changedLevel_eq_originalLevel

Documentation

Inside the common compositum, the restricted copies of the original and changed standard levels coincide at principal-unit depth n + 1.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateHigherUnit_restrict_changedLevel_eq_originalLevel
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    IntermediateField.restrict
        (le_sup_right :
          standardLubinTateChangedLevelField hπ u n ≤
            standardLubinTateChangedLevelCompositumField hπ u n) =
      IntermediateField.restrict
        (le_sup_left :
          standardLubinTateLevelField hπ n ≤
            standardLubinTateChangedLevelCompositumField hπ u n)

def

standardLubinTateHigherUnitChangedLevelAlgEquiv

L1375 ↗

LubinTate.standardLubinTateHigherUnitChangedLevelAlgEquiv

Documentation

The changed standard level is K-isomorphic to the original standard level when the unit factor is congruent to one at depth n + 1.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

def standardLubinTateHigherUnitChangedLevelAlgEquiv
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    standardLubinTateChangedLevelField hπ u n ≃ₐ[K]
      standardLubinTateLevelField hπ n

theorem

standardLubinTateUnitFactorFieldUnit_mem_standardNormSubgroup_of_mem_higher

L1404 ↗

LubinTate.standardLubinTateUnitFactorFieldUnit_mem_standardNormSubgroup_of_mem_higher

Documentation

A unit factor congruent to one at depth n + 1 is a norm from the original standard level.

Source context 10 commands

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

noncomputable section
open scoped Polynomial IntermediateField
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]

Lean source · statement

theorem
    standardLubinTateUnitFactorFieldUnit_mem_standardNormSubgroup_of_mem_higher
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (hu : u ∈
      CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)) :
    standardLubinTateUnitFactorFieldUnit F u ∈
      standardLubinTateNormSubgroup hπ n

Module documentation

Stability of a standard Lubin--Tate level under a deep unit change

Declarations