NYLL
Module

PrimitiveUniformizer.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveUniformizer
39 declarations indexed from sourceView source ↗

Module documentation

Uniformizers in standard Lubin--Tate level fields

Let F be a local field, let π be a chosen uniformizer, and let Lₙ = K(λₙ) be the simple extension generated by a chosen root of the standard primitive division polynomial. This file puts the integral-closure complete discrete valuation on Lₙ and proves that λₙ is a uniformizer.

The valuation calculation uses the actual Eisenstein polynomial. Its constant coefficient has target additive valuation equal to the ramification index, while every nonconstant lower term lies one step deeper in the target maximal-ideal filtration. Comparing with the leading term and the fundamental identity forces the normalized additive valuation of λₙ to be one.

Imports7
Imported by4

Declarations

theorem

isIntegral_mem_adjoin_of_powerBasis_minpoly_isEisensteinAt

L48 ↗
LubinTate.isIntegral_mem_adjoin_of_powerBasis_minpoly_isEisensteinAt
Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem
    isIntegral_mem_adjoin_of_powerBasis_minpoly_isEisensteinAt
    {R K' L : Type*} [CommRing R] [IsDomain R]
    [IsDiscreteValuationRing R] [Field K'] [Field L]
    [Algebra R K'] [Algebra K' L] [Algebra R L]
    [IsScalarTower R K' L] [IsFractionRing R K']
    [FiniteDimensional K' L] [Algebra.IsSeparable K' L]
    (B : PowerBasis K' L) (pi : R) (hpi : Irreducible pi)
    (hBint : IsIntegral R B.gen)
    (hei : (minpoly R B.gen).IsEisensteinAt
      (Ideal.span ({pi} : Set R)))
    {z : L} (hzint : IsIntegral R z) :
    z ∈ Algebra.adjoin R ({B.gen} : Set L)
theorem

integralClosure_adjoin_eq_top_of_powerBasis_minpoly_isEisensteinAt

L93 ↗
LubinTate.integralClosure_adjoin_eq_top_of_powerBasis_minpoly_isEisensteinAt
Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem
    integralClosure_adjoin_eq_top_of_powerBasis_minpoly_isEisensteinAt
    {R K' L A : Type*} [CommRing R] [IsDomain R]
    [IsDiscreteValuationRing R] [Field K'] [Field L] [CommRing A]
    [Algebra R K'] [Algebra K' L] [Algebra R L]
    [Algebra R A] [Algebra A L]
    [IsScalarTower R K' L] [IsScalarTower R A L]
    [IsFractionRing R K'] [FiniteDimensional K' L]
    [Algebra.IsSeparable K' L] [IsIntegralClosure A R L]
    (B : PowerBasis K' L) (pi : R) (hpi : Irreducible pi)
    (a : A) (ha : algebraMap A L a = B.gen)
    (hmap_injective : Function.Injective (algebraMap A L))
    (hBint : IsIntegral R B.gen)
    (hei : (minpoly R B.gen).IsEisensteinAt
      (Ideal.span ({pi} : Set R))) :
    Algebra.adjoin R ({a} : Set A) = ⊤
def

standardLubinTateLevelPowerBasis

L130 ↗
LubinTate.standardLubinTateLevelPowerBasis
Documentation

The canonical power basis of the simple standard Lubin--Tate level extension.

Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateLevelPowerBasis
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    PowerBasis K (standardLubinTateLevelField hπ n)
def

standardLubinTateLevelGenerator

L139 ↗
LubinTate.standardLubinTateLevelGenerator
Documentation

The chosen primitive root, regarded as an element of its standard level field.

Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateLevelGenerator
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTateLevelField hπ n
theorem

standardLubinTateLevelGenerator_coe

L148 ↗
LubinTate.standardLubinTateLevelGenerator_coe
Documentation

The level-field generator is the chosen primitive root after inclusion into the separable closure.

Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateLevelGenerator_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    ((standardLubinTateLevelGenerator hπ n :
        standardLubinTateLevelField hπ n) : SeparableClosure K) =
      chosenStandardLubinTatePrimitiveRoot hπ n
theorem

standardLubinTateLevelPowerBasis_minpoly

L160 ↗
LubinTate.standardLubinTateLevelPowerBasis_minpoly
Documentation

The minimal polynomial of the level-field generator is the standard primitive division polynomial over the base field.

Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateLevelPowerBasis_minpoly
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    minpoly K (standardLubinTateLevelPowerBasis hπ n).gen =
      standardLubinTatePrimitivePolynomialOverField F π n
theorem

standardLubinTateLevelGenerator_aeval_primitivePolynomial

L176 ↗
LubinTate.standardLubinTateLevelGenerator_aeval_primitivePolynomial
Documentation

The integral primitive polynomial annihilates the level-field generator.

Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateLevelGenerator_aeval_primitivePolynomial
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Polynomial.aeval (standardLubinTateLevelGenerator hπ n)
        (standardLubinTatePrimitivePolynomial F π n) = 0
instance

standardLubinTateLevelField_finiteDimensionalInstance

L196 ↗
LubinTate.standardLubinTateLevelField_finiteDimensionalInstance
Source context 9 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
Lean source · statement
instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n)
instance

standardLubinTateLevelField_isSeparableInstance

L203 ↗
LubinTate.standardLubinTateLevelField_isSeparableInstance
Source context 10 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
Lean source · statement
instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n)
theorem

standardLubinTateLevelCompleteDVFData_exists

L212 ↗
LubinTate.standardLubinTateLevelCompleteDVFData_exists
Source context 11 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
Lean source · full declaration
theorem standardLubinTateLevelCompleteDVFData_exists
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    ∃ target : CompleteDVF.{u, 0} (standardLubinTateLevelField hπ n),
      ∃ hExt : F.toCompleteDVF.valuation.HasExtension target.valuation,
        letI : F.toCompleteDVF.valuation.HasExtension target.valuation := hExt
        IsIntegralClosure target.valuationSubring F.valuationSubring
            (standardLubinTateLevelField hπ n) ∧
          degree F.toCompleteDVF.toDVF target.toDVF =
            ramificationIndex F.toCompleteDVF.toDVF target.toDVF *
              residueDegree F.toCompleteDVF.toDVF target.toDVF := by
  exact
    exists_integralClosure_standard_fundamental_identity
      (K := K) (L := standardLubinTateLevelField hπ n)
      F.toCompleteDVF
def

standardLubinTateLevelCompleteDVF

L230 ↗
LubinTate.standardLubinTateLevelCompleteDVF
Documentation

The complete discrete valuation on a standard Lubin--Tate level field selected from its actual integral closure over the base valuation ring.

Source context 11 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
Lean source · statement
def standardLubinTateLevelCompleteDVF
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteDVF.{u, 0} (standardLubinTateLevelField hπ n)
theorem

standardLubinTateLevelCompleteDVF_hasExtension

L237 ↗
LubinTate.standardLubinTateLevelCompleteDVF_hasExtension
Documentation

The chosen level valuation extends the given base valuation.

Source context 11 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
Lean source · statement
theorem standardLubinTateLevelCompleteDVF_hasExtension
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    F.toCompleteDVF.valuation.HasExtension
      (standardLubinTateLevelCompleteDVF hπ n).valuation
instance

standardLubinTateLevelCompleteDVF_hasExtensionInstance

L246 ↗
LubinTate.standardLubinTateLevelCompleteDVF_hasExtensionInstance
Source context 11 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
Lean source · statement
instance
    standardLubinTateLevelCompleteDVF_hasExtensionInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    F.toCompleteDVF.valuation.HasExtension
      (standardLubinTateLevelCompleteDVF hπ n).valuation
instance

standardLubinTateLevelValuationSubring_isScalarTower

L254 ↗
LubinTate.standardLubinTateLevelValuationSubring_isScalarTower
Source context 11 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
Lean source · statement
instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n)
theorem

standardLubinTateLevelCompleteDVF_isIntegralClosure

L264 ↗
LubinTate.standardLubinTateLevelCompleteDVF_isIntegralClosure
Documentation

The target valuation ring is the actual integral closure of the base valuation ring in the standard level field.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTateLevelCompleteDVF_isIntegralClosure
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsIntegralClosure
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      F.valuationSubring (standardLubinTateLevelField hπ n)
theorem

standardLubinTateLevelCompleteDVF_fundamentalIdentity

L276 ↗
LubinTate.standardLubinTateLevelCompleteDVF_fundamentalIdentity
Documentation

The chosen integral-closure valuation satisfies the fundamental identity at the standard Lubin--Tate level.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTateLevelCompleteDVF_fundamentalIdentity
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    degree F.toCompleteDVF.toDVF
        (standardLubinTateLevelCompleteDVF hπ n).toDVF =
      ramificationIndex F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF *
        residueDegree F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF
instance

standardLubinTateLevelValuationSubring_moduleFinite

L289 ↗
LubinTate.standardLubinTateLevelValuationSubring_moduleFinite
Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance
    standardLubinTateLevelValuationSubring_moduleFinite
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Module.Finite F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
def

standardLubinTateLevelLocalField

L311 ↗
LubinTate.standardLubinTateLevelLocalField
Documentation

The chosen complete-DVF structure is a local-field structure: its residue field is finite over the finite residue field of F.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
def standardLubinTateLevelLocalField
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    LocalField.{u, 0} (standardLubinTateLevelField hπ n)
theorem

standardLubinTateLevelGenerator_isIntegral_over_valuationSubring

L324 ↗
LubinTate.standardLubinTateLevelGenerator_isIntegral_over_valuationSubring
Documentation

The level generator is integral over the base valuation ring, witnessed by the genuine integral primitive division polynomial.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTateLevelGenerator_isIntegral_over_valuationSubring
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsIntegral F.valuationSubring
      (standardLubinTateLevelGenerator hπ n)
theorem

standardLubinTatePrimitivePoint_minpoly

L335 ↗
LubinTate.standardLubinTatePrimitivePoint_minpoly
Documentation

The integral minimal polynomial of the primitive level generator is the standard primitive division polynomial.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePoint_minpoly
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    minpoly F.valuationSubring
        (standardLubinTateLevelPowerBasis hπ n).gen =
      standardLubinTatePrimitivePolynomial F π n
theorem

standardLubinTateLevelGenerator_mem_valuationSubring

L357 ↗
LubinTate.standardLubinTateLevelGenerator_mem_valuationSubring
Documentation

The chosen primitive root belongs to the selected integral-closure valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTateLevelGenerator_mem_valuationSubring
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTateLevelGenerator hπ n ∈
      (standardLubinTateLevelCompleteDVF hπ n).valuation.valuationSubring
def

standardLubinTatePrimitivePointInteger

L382 ↗
LubinTate.standardLubinTatePrimitivePointInteger
Documentation

The primitive division point as an element of the chosen level valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
def standardLubinTatePrimitivePointInteger
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

standardLubinTatePrimitivePointInteger_coe

L392 ↗
LubinTate.standardLubinTatePrimitivePointInteger_coe
Documentation

The valuation-ring primitive point has the chosen level generator as its underlying field element.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePrimitivePointInteger hπ n).val =
        standardLubinTateLevelGenerator hπ n
theorem

standardLubinTatePrimitivePointInteger_adjoin_eq_top

L401 ↗
LubinTate.standardLubinTatePrimitivePointInteger_adjoin_eq_top
Documentation

The primitive Lubin--Tate point generates the entire integral-closure valuation ring over the base valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_adjoin_eq_top
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.adjoin F.valuationSubring
        ({standardLubinTatePrimitivePointInteger hπ n} :
          Set
            (standardLubinTateLevelCompleteDVF hπ n).valuationSubring) =
      ⊤
def

standardLubinTatePrimitivePointIntegerToSeparableClosure

L435 ↗
LubinTate.standardLubinTatePrimitivePointIntegerToSeparableClosure
Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
def
    standardLubinTatePrimitivePointIntegerToSeparableClosure
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring →+*
      SeparableClosure K
theorem

standardLubinTatePrimitivePointIntegerToSeparableClosure_injective

L444 ↗
LubinTate.standardLubinTatePrimitivePointIntegerToSeparableClosure_injective
Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerToSeparableClosure_injective
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Function.Injective
      (standardLubinTatePrimitivePointIntegerToSeparableClosure hπ n)
theorem

standardLubinTatePrimitivePointIntegerToSeparableClosure_comp_integerMap

L459 ↗
LubinTate.standardLubinTatePrimitivePointIntegerToSeparableClosure_comp_integerMap
Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerToSeparableClosure_comp_integerMap
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePrimitivePointIntegerToSeparableClosure hπ n).comp
        (integerMap F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF) =
      (algebraMap K (SeparableClosure K)).comp
        (algebraMap F.valuationSubring K)
theorem

standardLubinTatePrimitivePointIntegerToSeparableClosure_apply

L481 ↗
LubinTate.standardLubinTatePrimitivePointIntegerToSeparableClosure_apply
Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerToSeparableClosure_apply
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTatePrimitivePointIntegerToSeparableClosure hπ n
        (standardLubinTatePrimitivePointInteger hπ n) =
      chosenStandardLubinTatePrimitiveRoot hπ n
theorem

polynomial_eval₂_mem_ideal_of_coeff_mem

L494 ↗
LubinTate.polynomial_eval₂_mem_ideal_of_coeff_mem
Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem polynomial_eval₂_mem_ideal_of_coeff_mem
    {R S : Type*} [CommSemiring R] [CommSemiring S]
    (f : R →+* S) (I : Ideal S) (P : Polynomial R) (z : S)
    (hcoeff : ∀ i, f (P.coeff i) ∈ I) :
    P.eval₂ f z ∈ I
theorem

standardLubinTatePrimitivePointInteger_aeval

L505 ↗
LubinTate.standardLubinTatePrimitivePointInteger_aeval
Documentation

The integral primitive polynomial annihilates the primitive point in the valuation ring of the standard finite level.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_aeval
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Polynomial.aeval (standardLubinTatePrimitivePointInteger hπ n)
        (standardLubinTatePrimitivePolynomial F π n) = 0
theorem

standardLubinTatePrimitivePointInteger_addVal_and_ramificationIndex

L523 ↗
LubinTate.standardLubinTatePrimitivePointInteger_addVal_and_ramificationIndex
Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem
    standardLubinTatePrimitivePointInteger_addVal_and_ramificationIndex
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTatePrimitivePointInteger hπ n) = 1 ∧
      ramificationIndex F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF =
        degree F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF
theorem

standardLubinTatePrimitivePointInteger_addVal

L755 ↗
LubinTate.standardLubinTatePrimitivePointInteger_addVal
Documentation

The chosen primitive division point has normalized additive valuation one in the integral-closure valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (standardLubinTatePrimitivePointInteger hπ n) = 1
theorem

standardLubinTateLevel_ramificationIndex_eq_degree

L766 ↗
LubinTate.standardLubinTateLevel_ramificationIndex_eq_degree
Documentation

The standard finite Lubin--Tate level is totally ramified: its ramification index equals its field degree.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTateLevel_ramificationIndex_eq_degree
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    ramificationIndex F.toCompleteDVF.toDVF
        (standardLubinTateLevelCompleteDVF hπ n).toDVF =
      degree F.toCompleteDVF.toDVF
        (standardLubinTateLevelCompleteDVF hπ n).toDVF
theorem

standardLubinTateUniformizerInteger_map_addVal

L779 ↗
LubinTate.standardLubinTateUniformizerInteger_map_addVal
Documentation

The image of any base-field uniformizer in a standard finite level has additive valuation equal to the degree of that level. The uniformizer used here need not be the parameter defining the Lubin--Tate level.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTateUniformizerInteger_map_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    {ϖ : F.valuationSubring}
    (hϖ : F.toCompleteDVF.valuation.IsUniformizer (ϖ : K))
    (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (integerMap F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF ϖ) =
      (((Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n : ℕ) : ℕ∞)
theorem

standardLubinTateBaseUniformizerInteger_map_addVal

L817 ↗
LubinTate.standardLubinTateBaseUniformizerInteger_map_addVal
Documentation

The image of the parameter uniformizer has additive valuation equal to the standard finite-level degree.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTateBaseUniformizerInteger_map_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
        (integerMap F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF π) =
      (((Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n : ℕ) : ℕ∞)
theorem

standardLubinTatePrimitivePointInteger_irreducible

L830 ↗
LubinTate.standardLubinTatePrimitivePointInteger_irreducible
Documentation

The primitive point is irreducible in the integral-closure valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_irreducible
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Irreducible (standardLubinTatePrimitivePointInteger hπ n)
theorem

standardLubinTatePrimitivePoint_isUniformizer

L849 ↗
LubinTate.standardLubinTatePrimitivePoint_isUniformizer
Documentation

The chosen primitive division point is a uniformizer of the standard Lubin--Tate level field with its integral-closure valuation.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePoint_isUniformizer
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTateLevelCompleteDVF hπ n).valuation.IsUniformizer
      (standardLubinTatePrimitivePointInteger hπ n).val
theorem

standardLubinTatePrimitivePointInteger_iterate_succ_eq_zero

L860 ↗
LubinTate.standardLubinTatePrimitivePointInteger_iterate_succ_eq_zero
Documentation

Evaluation in the chosen target valuation ring records that the primitive level-n + 1 point is killed by the level-n + 1 standard iterate.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_iterate_succ_eq_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Polynomial.eval₂
        (integerMap F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF)
        (standardLubinTatePrimitivePointInteger hπ n)
        (standardLubinTatePolynomialIterate F π (n + 1)) = 0
theorem

standardLubinTatePrimitivePointInteger_iterate_ne_zero_of_le

L881 ↗
LubinTate.standardLubinTatePrimitivePointInteger_iterate_ne_zero_of_le
Documentation

No iterate of index at most n already kills the primitive level-n + 1 point, now expressed inside the chosen target valuation ring.

Source context 12 commands

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

noncomputable section
open scoped Polynomial
universe u v w x
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensionalInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
local instance standardLubinTateLevelField_isSeparableInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra.IsSeparable K (standardLubinTateLevelField hπ n) :=
  (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable
      (F := K) (E := SeparableClosure K)).2
    (Algebra.IsSeparable.isSeparable K
      (chosenStandardLubinTatePrimitiveRoot hπ n))
local instance standardLubinTateLevelValuationSubring_isScalarTower
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsScalarTower F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
      (standardLubinTateLevelField hπ n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem standardLubinTatePrimitivePointInteger_iterate_ne_zero_of_le
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    {r : ℕ} (hr : r ≤ n) :
    Polynomial.eval₂
        (integerMap F.toCompleteDVF.toDVF
          (standardLubinTateLevelCompleteDVF hπ n).toDVF)
        (standardLubinTatePrimitivePointInteger hπ n)
        (standardLubinTatePolynomialIterate F π r) ≠ 0

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