NYLL
Module

PrimitivePoint.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.PrimitivePoint
42 declarations indexed from sourceView source ↗

Module documentation

The chosen complete valuation and primitive Lubin--Tate point

This module constructs the actual complete discrete valuation on an explicit finite equal-characteristic Lubin--Tate level. It proves that the chosen primitive point generates the integral closure and is a uniformizer.

Imports12
Imported by3

Declarations

theorem

isEisensteinAt_map_ringEquiv

L47 ↗
LubinTate.isEisensteinAt_map_ringEquiv
Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
Lean source · statement
theorem isEisensteinAt_map_ringEquiv
    {R S : Type*} [CommRing R] [CommRing S]
    (e : R ≃+* S) {f : Polynomial R} {I : Ideal R}
    (hf : f.IsEisensteinAt I) :
    (f.map e).IsEisensteinAt (I.map e)
theorem

isIntegral_mem_adjoin_of_powerBasis_minpoly_isEisensteinAt

L77 ↗
LubinTate.isIntegral_mem_adjoin_of_powerBasis_minpoly_isEisensteinAt
Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
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

L122 ↗
LubinTate.integralClosure_adjoin_eq_top_of_powerBasis_minpoly_isEisensteinAt
Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
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

equalCharacteristicLubinTateBaseCompleteDVF

L163 ↗
LubinTate.equalCharacteristicLubinTateBaseCompleteDVF
Documentation

The canonical complete discrete valuation on the equal-characteristic Laurent-series base used by the explicit Lubin--Tate level construction.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
def equalCharacteristicLubinTateBaseCompleteDVF
    (F : LocalField.{0, v} K₀) :
    ValuationTheory.DiscreteValuationField.CompleteDVF.{0, 0}
      F.residueField⸨X⸩
theorem

equalCharacteristicLubinTateBaseCompleteDVF_valuation_eq

L175 ↗
LubinTate.equalCharacteristicLubinTateBaseCompleteDVF_valuation_eq
Documentation

The valuation packaged by the chosen Laurent-series base is the canonical valuation induced by the equal-characteristic valuative relation.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · full declaration
theorem equalCharacteristicLubinTateBaseCompleteDVF_valuation_eq
    (F : LocalField.{0, v} K₀) :
    (equalCharacteristicLubinTateBaseCompleteDVF F).valuation =
      letI : ValuativeRel F.residueField⸨X⸩ :=
        equalCharacteristicLaurentValuativeRel F
      ValuativeRel.valuation F.residueField⸨X⸩ := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  let : IsNonarchimedeanLocalField F.residueField⸨X⸩ :=
    equalCharacteristicLaurentIsNonarchimedeanLocalField F
  change
    (LocalFieldTheory.localCompleteDVF F.residueField⸨X⸩).valuation =
      ValuativeRel.valuation F.residueField⸨X⸩
  unfold LocalFieldTheory.localCompleteDVF
  unfold ValuationTheory.Valuations.completeDVFOfCompleteValuedField
  rfl
def

equalCharacteristicLaurentValuativeIntegerEquivLubinTateBaseValuationSubring

L194 ↗
LubinTate.equalCharacteristicLaurentValuativeIntegerEquivLubinTateBaseValuationSubring
Documentation

Identity on Laurent-series elements identifies the canonical valuative integer ring with the valuation ring packaged by the chosen complete DVF.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · full declaration
def
    equalCharacteristicLaurentValuativeIntegerEquivLubinTateBaseValuationSubring
    (F : LocalField.{0, v} K₀) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    (ValuativeRel.valuation F.residueField⸨X⸩).integer ≃+*
      (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring := by
  letI : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  let hval :=
    equalCharacteristicLubinTateBaseCompleteDVF_valuation_eq F
  exact
    { toFun := fun x => ⟨x, by
        change
          (equalCharacteristicLubinTateBaseCompleteDVF F).valuation
              (x : F.residueField⸨X⸩) ≤ 1
        rw [hval]
        exact x.property⟩
      invFun := fun x => ⟨x, by
        change
          ValuativeRel.valuation F.residueField⸨X⸩
              (x : F.residueField⸨X⸩) ≤ 1
        rw [← hval]
        exact x.property⟩
      left_inv := fun _ => rfl
      right_inv := fun _ => rfl
      map_mul' := fun _ _ => rfl
      map_add' := fun _ _ => rfl }
def

equalCharacteristicPowerSeriesEquivLubinTateBaseValuationSubring

L225 ↗
LubinTate.equalCharacteristicPowerSeriesEquivLubinTateBaseValuationSubring
Documentation

Power series are exactly the valuation ring of the chosen equal-characteristic Laurent-series base.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
def
    equalCharacteristicPowerSeriesEquivLubinTateBaseValuationSubring
    (F : LocalField.{0, v} K₀) :
    F.residueField⟦X⟧ ≃+*
      (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
theorem

equalCharacteristicPowerSeriesEquivLubinTateBaseValuationSubring_coe

L240 ↗
LubinTate.equalCharacteristicPowerSeriesEquivLubinTateBaseValuationSubring_coe
Documentation

The power-series/valuation-ring equivalence is the usual inclusion after coercion to the Laurent-series field.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicPowerSeriesEquivLubinTateBaseValuationSubring_coe
    (F : LocalField.{0, v} K₀) (f : F.residueField⟦X⟧) :
    ((equalCharacteristicPowerSeriesEquivLubinTateBaseValuationSubring F f :
        (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring) :
      F.residueField⸨X⸩) =
        (f : F.residueField⸨X⸩)
def

equalCharacteristicLubinTateBaseUniformizerInteger

L251 ↗
LubinTate.equalCharacteristicLubinTateBaseUniformizerInteger
Documentation

The Laurent parameter T, now regarded as an element of the valuation ring packaged by the chosen base complete DVF.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
def equalCharacteristicLubinTateBaseUniformizerInteger
    (F : LocalField.{0, v} K₀) :
    (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
theorem

equalCharacteristicLubinTateBaseUniformizerInteger_coe

L259 ↗
LubinTate.equalCharacteristicLubinTateBaseUniformizerInteger_coe
Documentation

The chosen base valuation-ring parameter has Laurent-series value T.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTateBaseUniformizerInteger_coe
    (F : LocalField.{0, v} K₀) :
    (equalCharacteristicLubinTateBaseUniformizerInteger F :
      F.residueField⸨X⸩) =
        equalCharacteristicLaurentUniformizer F
theorem

equalCharacteristicLubinTateBaseUniformizerInteger_irreducible

L270 ↗
LubinTate.equalCharacteristicLubinTateBaseUniformizerInteger_irreducible
Documentation

The Laurent parameter is irreducible in the valuation ring packaged by the chosen base complete DVF.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTateBaseUniformizerInteger_irreducible
    (F : LocalField.{0, v} K₀) :
    Irreducible (equalCharacteristicLubinTateBaseUniformizerInteger F)
def

equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring

L279 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring
Documentation

The integral primitive division polynomial, with its coefficients transported from κ[[T]] to the chosen base valuation ring.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
def
    equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring
    (F : LocalField.{0, v} K₀) (n : ℕ) :
    Polynomial
      (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
theorem

equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_monic

L289 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_monic
Documentation

The primitive division polynomial remains monic after transport to the chosen base valuation ring.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_monic
    (F : LocalField.{0, v} K₀) (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring
      F n).Monic
theorem

equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_map

L298 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_map
Documentation

Mapping the valuation-ring primitive polynomial into the Laurent-series field recovers the original primitive division polynomial.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_map
    (F : LocalField.{0, v} K₀) (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring
        F n).map
          (algebraMap
            (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
            F.residueField⸨X⸩) =
      equalCharacteristicLubinTatePrimitivePolynomial F n
theorem

equalCharacteristicLubinTateLevelCompleteDVFData_exists

L314 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVFData_exists
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension
  (exists_integralClosure_standard_fundamental_identity) in
Lean source · full declaration
theorem equalCharacteristicLubinTateLevelCompleteDVFData_exists
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    ∃ target :
        ValuationTheory.DiscreteValuationField.CompleteDVF.{0, 0}
          (equalCharacteristicLubinTateLevelField F n),
      ∃ hExt :
          (equalCharacteristicLubinTateBaseCompleteDVF F).valuation.HasExtension
            target.valuation,
        letI :
            (equalCharacteristicLubinTateBaseCompleteDVF F).valuation.HasExtension
              target.valuation := hExt
        IsIntegralClosure target.valuationSubring
            (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
            (equalCharacteristicLubinTateLevelField F n) ∧
          ValuationTheory.DiscreteValuationField.ValuedExtension.degree
              (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
              target.toDVF =
            ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
                (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
                target.toDVF *
              ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
                (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
                target.toDVF := by
  let : FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
    equalCharacteristicLubinTateLevelField_finiteDimensional F n
  let : IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
    equalCharacteristicLubinTateLevelField_isGalois F n
  exact
    exists_integralClosure_standard_fundamental_identity
      (K := F.residueField⸨X⸩)
      (L := equalCharacteristicLubinTateLevelField F n)
      (equalCharacteristicLubinTateBaseCompleteDVF F)
def

equalCharacteristicLubinTateLevelCompleteDVF

L354 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF
Documentation

A complete-DVF structure on the explicit equal-characteristic Lubin--Tate level field, chosen from its actual integral closure over κ((T)).

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
def equalCharacteristicLubinTateLevelCompleteDVF
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    ValuationTheory.DiscreteValuationField.CompleteDVF.{0, 0}
      (equalCharacteristicLubinTateLevelField F n)
theorem

equalCharacteristicLubinTateLevelCompleteDVF_hasExtension

L365 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF_hasExtension
Documentation

The chosen level valuation extends the canonical Laurent-series base valuation.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTateLevelCompleteDVF_hasExtension
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTateBaseCompleteDVF F).valuation.HasExtension
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuation
instance

equalCharacteristicLubinTateLevelCompleteDVF_hasExtensionInstance

L377 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF_hasExtensionInstance
Documentation

Provides the canonical extension instance for the chosen equal-characteristic Lubin--Tate level valuation.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
instance
    equalCharacteristicLubinTateLevelCompleteDVF_hasExtensionInstance
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTateBaseCompleteDVF F).valuation.HasExtension
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuation
theorem

equalCharacteristicLubinTateLevelCompleteDVF_isIntegralClosure

L388 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF_isIntegralClosure
Documentation

The valuation ring of the chosen level target is the actual integral closure of the Laurent-series base valuation ring.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTateLevelCompleteDVF_isIntegralClosure
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsIntegralClosure
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
      (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
      (equalCharacteristicLubinTateLevelField F n)
theorem

equalCharacteristicLubinTateLevelCompleteDVF_fundamentalIdentity

L402 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF_fundamentalIdentity
Documentation

The chosen integral-closure valuation realizes the fundamental identity for the explicit finite Lubin--Tate level.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTateLevelCompleteDVF_fundamentalIdentity
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    ValuationTheory.DiscreteValuationField.ValuedExtension.degree
        (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
        (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF =
      ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
          (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
          (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF *
        ValuationTheory.DiscreteValuationField.ValuedExtension.residueDegree
          (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
          (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF
theorem

equalCharacteristicLubinTateLevelPowerBasis_gen_isIntegral_over_baseValuationSubring

L422 ↗
LubinTate.equalCharacteristicLubinTateLevelPowerBasis_gen_isIntegral_over_baseValuationSubring
Documentation

The power-basis generator is integral over the chosen base valuation ring. Its witness is the transported integral primitive polynomial, not a field-level integrality surrogate.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicLubinTateLevelPowerBasis_gen_isIntegral_over_baseValuationSubring
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsIntegral
      (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
      (equalCharacteristicLubinTateLevelPowerBasis F n).gen
theorem

equalCharacteristicLubinTateLevelPowerBasis_gen_mem_valuationSubring

L465 ↗
LubinTate.equalCharacteristicLubinTateLevelPowerBasis_gen_mem_valuationSubring
Documentation

The chosen primitive Lubin--Tate division point belongs to the actual integral-closure valuation ring selected on the level field.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicLubinTateLevelPowerBasis_gen_mem_valuationSubring
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTateLevelPowerBasis F n).gen ∈
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuation.valuationSubring
def

equalCharacteristicLubinTatePrimitivePointInteger

L497 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger
Documentation

The primitive level-n+1 division point as an element of the chosen target valuation ring. Its norm computation below proves that this element is a uniformizer.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
def equalCharacteristicLubinTatePrimitivePointInteger
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
theorem

equalCharacteristicLubinTatePrimitivePointInteger_coe

L508 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_coe
Documentation

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

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePointInteger_coe
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePointInteger F n).val =
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen
theorem

equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_isEisensteinAt

L518 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_isEisensteinAt
Documentation

The transported integral primitive polynomial is Eisenstein at the chosen Laurent uniformizer.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring_isEisensteinAt
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring
      F n).IsEisensteinAt
        (Ideal.span
          ({equalCharacteristicLubinTateBaseUniformizerInteger F} :
            Set
              (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring))
theorem

equalCharacteristicLubinTatePrimitivePoint_minpoly

L546 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePoint_minpoly
Documentation

The integral minimal polynomial of the primitive point is the transported Lubin--Tate primitive polynomial.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePoint_minpoly
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    minpoly
        (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTatePrimitivePolynomialInBaseValuationSubring
        F n
theorem

equalCharacteristicLubinTatePrimitivePointInteger_adjoin_eq_top

L569 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_adjoin_eq_top
Documentation

The primitive Lubin--Tate point generates the entire chosen integral closure over the Laurent-series valuation ring.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePointInteger_adjoin_eq_top
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    Algebra.adjoin
        (equalCharacteristicLubinTateBaseCompleteDVF F).valuationSubring
        ({equalCharacteristicLubinTatePrimitivePointInteger F n} :
          Set
            (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring) =
      ⊤
theorem

equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueValuationExtension

L619 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueValuationExtension
Documentation

Finite separability gives uniqueness of the chosen complete valuation extension on the explicit level field.

Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension (
  HasUniqueValuationExtension
  hasUniqueValuationExtension_of_finite_separable
) in
Lean source · statement
theorem
    equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueValuationExtension
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    HasUniqueValuationExtension.{0, 0, 0, 0, y}
      (base := equalCharacteristicLubinTateBaseCompleteDVF F)
      (target := equalCharacteristicLubinTateLevelCompleteDVF F n)
theorem

equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension

L643 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
Documentation

Uniqueness after forgetting completeness, in the form required by the real lower ramification groups.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{0, 0, 0, 0, y}
      (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
      (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF
theorem

addVal_prod_valuationSubringAut

L653 ↗
LubinTate.addVal_prod_valuationSubringAut
Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem addVal_prod_valuationSubringAut
    {K₁ L₁ : Type} [Field K₁] [Field L₁] [Algebra K₁ L₁]
    [FiniteDimensional K₁ L₁] [IsGalois K₁ L₁]
    (base : DVF.{0, 0} K₁) (target : DVF.{0, 0} L₁)
    [base.valuation.HasExtension target.valuation]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{0, 0, 0, 0, 0}
        base target)
    (a : target.valuationSubring) :
    IsDiscreteValuationRing.addVal target.valuationSubring
        (∏ sigma : Gal(L₁/K₁),
          valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq sigma a) =
      Nat.card Gal(L₁/K₁) •
        IsDiscreteValuationRing.addVal target.valuationSubring a
instance

equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer

L690 ↗
LubinTate.equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
Lean source · statement
instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
instance

equalCharacteristicLubinTateLevelField_isGalois_forUniformizer

L699 ↗
LubinTate.equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
Source context 15 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
Lean source · statement
instance
    equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
theorem

equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension_zero

L708 ↗
LubinTate.equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension_zero
Source context 16 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem
    equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension_zero
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{0, 0, 0, 0, 0}
      (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
      (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF
theorem

equalCharacteristicLubinTateBaseUniformizerInteger_map_addVal

L720 ↗
LubinTate.equalCharacteristicLubinTateBaseUniformizerInteger_map_addVal
Documentation

The image of the Laurent parameter in a Lubin--Tate level has additive valuation equal to the ramification index.

Source context 16 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem equalCharacteristicLubinTateBaseUniformizerInteger_map_addVal
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (integerMap
          (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
          (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF
          (equalCharacteristicLubinTateBaseUniformizerInteger F)) =
      (ramificationIndex
        (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
        (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF : ℕ∞)
theorem

equalCharacteristicLubinTateBaseUniformizer_orbitProduct

L741 ↗
LubinTate.equalCharacteristicLubinTateBaseUniformizer_orbitProduct
Documentation

The norm identity for the negative primitive point, lifted to the chosen valuation rings as the product of its full Galois orbit.

Source context 16 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · full declaration
theorem equalCharacteristicLubinTateBaseUniformizer_orbitProduct
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    let base := equalCharacteristicLubinTateBaseCompleteDVF F
    let target := equalCharacteristicLubinTateLevelCompleteDVF F n
    integerMap base.toDVF target.toDVF
        (equalCharacteristicLubinTateBaseUniformizerInteger F) =
      ∏ sigma : Gal((equalCharacteristicLubinTateLevelField F n) /
          F.residueField⸨X⸩),
        valuationSubringAutOfUniqueExtension
          (base := base.toDVF) (target := target.toDVF)
          (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension_zero
            F n)
          sigma (-equalCharacteristicLubinTatePrimitivePointInteger F n) := by
  classical
  dsimp only
  apply Subtype.ext
  simp only [integerMap_apply,
    equalCharacteristicLubinTateBaseUniformizerInteger_coe]
  change
    algebraMap F.residueField⸨X⸩
        (equalCharacteristicLubinTateLevelField F n)
        (equalCharacteristicLaurentUniformizer F) =
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuation.valuationSubring.subtype
          (∏ sigma : Gal((equalCharacteristicLubinTateLevelField F n) /
              F.residueField⸨X⸩),
            valuationSubringAutOfUniqueExtension
              (base :=
                (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF)
              (target :=
                (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF)
              (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension_zero
                F n)
              sigma (-equalCharacteristicLubinTatePrimitivePointInteger F n))
  rw [map_prod]
  calc
    algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)
          (equalCharacteristicLaurentUniformizer F) =
        algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n)
          (Algebra.norm F.residueField⸨X⸩
            (-equalCharacteristicLubinTateLevelGenerator F n)) := by
              rw [equalCharacteristicLubinTate_norm_neg_levelGenerator]
    _ = ∏ sigma : Gal((equalCharacteristicLubinTateLevelField F n) /
          F.residueField⸨X⸩),
        sigma (-equalCharacteristicLubinTateLevelGenerator F n) :=
      Algebra.norm_eq_prod_automorphisms
        F.residueField⸨X⸩
        (-equalCharacteristicLubinTateLevelGenerator F n)
    _ = ∏ sigma : Gal((equalCharacteristicLubinTateLevelField F n) /
          F.residueField⸨X⸩),
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuation.valuationSubring.subtype
            (valuationSubringAutOfUniqueExtension
              (base :=
                (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF)
              (target :=
                (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF)
              (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension_zero
                F n)
              sigma (-equalCharacteristicLubinTatePrimitivePointInteger F n)) := by
      apply Finset.prod_congr rfl
      intro sigma _hsigma
      change
        sigma (-equalCharacteristicLubinTateLevelGenerator F n) =
          sigma (-(equalCharacteristicLubinTateLevelPowerBasis F n).gen)
      rfl
theorem

equalCharacteristicLubinTatePrimitivePointInteger_addVal

L812 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_addVal
Documentation

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

Source context 16 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePointInteger_addVal
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (equalCharacteristicLubinTatePrimitivePointInteger F n) = 1
theorem

equalCharacteristicLubinTatePrimitivePointInteger_irreducible

L903 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_irreducible
Documentation

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

Source context 16 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePointInteger_irreducible
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    Irreducible (equalCharacteristicLubinTatePrimitivePointInteger F n)
theorem

equalCharacteristicLubinTatePrimitivePoint_isUniformizer

L923 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePoint_isUniformizer
Documentation

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

Source context 16 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointUniformizer
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePoint_isUniformizer
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTateLevelCompleteDVF F n).valuation.IsUniformizer
      (equalCharacteristicLubinTatePrimitivePointInteger F n).val
theorem

equalCharacteristicLubinTatePrimitivePointInteger_displacement_coe_eq_aeval

L939 ↗
LubinTate.equalCharacteristicLubinTatePrimitivePointInteger_displacement_coe_eq_aeval
Documentation

After passing the primitive point to the chosen valuation ring, its Galois displacement is still the evaluation of the genuine Lubin--Tate bracket polynomial for a - 1. The normalized valuation is computed below from the first nonzero visible coefficient.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
Lean source · statement
theorem
    equalCharacteristicLubinTatePrimitivePointInteger_displacement_coe_eq_aeval
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (σ : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩))
    (a : equalCharacteristicLubinTateUnitParameter F n)
    (ha :
      σ (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
        equalCharacteristicLubinTateLevelBracket F n (n + 1)
          (equalCharacteristicLubinTateUnitParameterSeries F n a)
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen) :
    (RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension
            (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
              F n)
            σ (equalCharacteristicLubinTatePrimitivePointInteger F n) -
        equalCharacteristicLubinTatePrimitivePointInteger F n :
      (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring).val =
        Polynomial.aeval
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen
          (equalCharacteristicLubinTateBracketPolynomial F (n + 1)
            (equalCharacteristicLubinTateUnitParameterSeries F n a - 1))
instance

equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation

L1023 ↗
LubinTate.equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
Lean source · statement
instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
instance

equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation

L1032 ↗
LubinTate.equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
Source context 15 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
Lean source · statement
instance
    equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
theorem

equalCharacteristicLubinTateBaseUniformizerInteger_map_addVal_eq_degree

L1043 ↗
LubinTate.equalCharacteristicLubinTateBaseUniformizerInteger_map_addVal_eq_degree
Documentation

In the chosen level valuation, the Laurent parameter has additive valuation equal to the explicit Lubin--Tate degree (q - 1)q^n.

Source context 16 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.ValuedExtension
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
section PrimitivePointDisplacementValuation
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forDisplacementValuation
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forDisplacementValuation
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem equalCharacteristicLubinTateBaseUniformizerInteger_map_addVal_eq_degree
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsDiscreteValuationRing.addVal
        (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
        (integerMap
          (equalCharacteristicLubinTateBaseCompleteDVF F).toDVF
          (equalCharacteristicLubinTateLevelCompleteDVF F n).toDVF
          (equalCharacteristicLubinTateBaseUniformizerInteger F)) =
      ((Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n : ℕ)

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