Module

ChangedLevelCompositum.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.ChangedLevelCompositum

38 declarations indexed from sourceView source ↗

Module documentation

A common valued field for original and changed Lubin--Tate levels

The standard level for a uniformizer π and the standard level for a unit change uπ both live in the fixed separable closure of the base field. Their compositum therefore gives a literal common overfield. This file chooses the complete discrete valuation supplied by the integral closure of the base valuation ring in that compositum.

Uniqueness of valuation extension from the complete base shows that the chosen compositum valuation extends the already chosen valuation on each level. The two inclusions consequently preserve valuation-ring and maximal-ideal membership. Their normalized additive valuations scale by the corresponding ramification index; no equality between the two levels and no higher-unit hypothesis is used.

Imports3

Imported by2

abbrev

standardLubinTateChangedLevelCompositumField

L45 ↗

LubinTate.standardLubinTateChangedLevelCompositumField

Documentation

The compositum of the standard π-level and the standard uπ-level inside the fixed separable closure.

Source context 8 commands

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

noncomputable section
universe u v
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

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

theorem

standardLubinTateChangedLevelCompositumField_finiteDimensional

L55 ↗

LubinTate.standardLubinTateChangedLevelCompositumField_finiteDimensional

Documentation

The original and changed finite levels have a finite-dimensional compositum over the base field.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelCompositumField_finiteDimensional
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    FiniteDimensional K
      (standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateChangedLevelCompositumField_isSeparable

L72 ↗

LubinTate.standardLubinTateChangedLevelCompositumField_isSeparable

Documentation

The compositum is separable over the base field.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelCompositumField_isSeparable
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    Algebra.IsSeparable K
      (standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateChangedLevelCompositumField_isGalois

L93 ↗

LubinTate.standardLubinTateChangedLevelCompositumField_isGalois

Documentation

The compositum is Galois over the base field.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelCompositumField_isGalois
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    IsGalois K
      (standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateChangedLevelCompositumCompleteDVFData_exists

L114 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVFData_exists

Source context 8 commands

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

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

Lean source · full declaration

theorem
    standardLubinTateChangedLevelCompositumCompleteDVFData_exists
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    ∃ target : CompleteDVF.{u, 0}
        (standardLubinTateChangedLevelCompositumField hπ u n),
      ∃ hExt :
          F.toCompleteDVF.valuation.HasExtension target.valuation,
        letI :
            F.toCompleteDVF.valuation.HasExtension target.valuation :=
          hExt
        IsIntegralClosure target.valuationSubring F.valuationSubring
            (standardLubinTateChangedLevelCompositumField hπ u n) ∧
          degree F.toCompleteDVF.toDVF target.toDVF =
            ramificationIndex F.toCompleteDVF.toDVF target.toDVF *
              residueDegree F.toCompleteDVF.toDVF target.toDVF := by
  let M := standardLubinTateChangedLevelCompositumField hπ u n
  let : FiniteDimensional K M :=
    standardLubinTateChangedLevelCompositumField_finiteDimensional
      hπ u n
  let : Algebra.IsSeparable K M :=
    standardLubinTateChangedLevelCompositumField_isSeparable hπ u n
  exact
    exists_integralClosure_standard_fundamental_identity
      (K := K) (L := M) F.toCompleteDVF

def

standardLubinTateChangedLevelCompositumCompleteDVF

L143 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVF

Documentation

The complete discrete valuation on the common compositum selected from the integral closure of the base valuation ring.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelCompositumCompleteDVF
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    CompleteDVF.{u, 0}
      (standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateChangedLevelCompositumCompleteDVF_hasExtension

L154 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVF_hasExtension

Documentation

The compositum valuation extends the base valuation.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelCompositumCompleteDVF_hasExtension
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    F.toCompleteDVF.valuation.HasExtension
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation

instance

standardLubinTateChangedLevelCompositumCompleteDVF_hasExtensionInstance

L167 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVF_hasExtensionInstance

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelCompositumCompleteDVF_hasExtensionInstance
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    F.toCompleteDVF.valuation.HasExtension
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation

theorem

standardLubinTateChangedLevelCompositumCompleteDVF_isIntegralClosure

L180 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVF_isIntegralClosure

Documentation

The chosen compositum valuation ring is the integral closure of the base valuation ring.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelCompositumCompleteDVF_isIntegralClosure
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    IsIntegralClosure
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuationSubring
      F.valuationSubring
      (standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateChangedLevelCompositumCompleteDVF_fundamentalIdentity

L197 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVF_fundamentalIdentity

Documentation

The chosen compositum valuation satisfies the finite-extension fundamental identity.

Source context 8 commands

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

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

Lean source · full declaration

theorem
    standardLubinTateChangedLevelCompositumCompleteDVF_fundamentalIdentity
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    let target :=
      standardLubinTateChangedLevelCompositumCompleteDVF hπ u n
    degree F.toCompleteDVF.toDVF target.toDVF =
      ramificationIndex F.toCompleteDVF.toDVF target.toDVF *
        residueDegree F.toCompleteDVF.toDVF target.toDVF :=
  (Classical.choose_spec
    (Classical.choose_spec
      (standardLubinTateChangedLevelCompositumCompleteDVFData_exists
        hπ u n))).2

theorem

standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueValuationExtension

L214 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueValuationExtension

Documentation

Completeness of the base makes the chosen compositum valuation the unique extension of the base valuation.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueValuationExtension
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    ValuationTheory.DiscreteValuationField.ValuedExtension.HasUniqueValuationExtension.{u, v, u,
      0, 0}
      (base := F.toCompleteDVF)
      (target :=
        standardLubinTateChangedLevelCompositumCompleteDVF hπ u n)

theorem

standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueDVFValuationExtension

L237 ↗

LubinTate.standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueDVFValuationExtension

Documentation

The same uniqueness statement after forgetting completeness.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelCompositumCompleteDVF_hasUniqueDVFValuationExtension
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, u, 0, 0}
      F.toCompleteDVF.toDVF
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).toDVF

def

standardLubinTateLevelToChangedLevelCompositum

L251 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositum

Documentation

The literal inclusion of the original level into the common compositum.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateLevelToChangedLevelCompositum
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    standardLubinTateLevelField hπ n →ₐ[K]
      standardLubinTateChangedLevelCompositumField hπ u n

def

standardLubinTateChangedLevelToCompositum

L261 ↗

LubinTate.standardLubinTateChangedLevelToCompositum

Documentation

The literal inclusion of the changed level into the common compositum.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelToCompositum
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    standardLubinTateChangedLevelField hπ u n →ₐ[K]
      standardLubinTateChangedLevelCompositumField hπ u n

theorem

standardLubinTateLevelToChangedLevelCompositum_coe

L272 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositum_coe

Documentation

The original-level inclusion is the ambient identity on separable-closure elements.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateLevelToChangedLevelCompositum_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (x : standardLubinTateLevelField hπ n) :
    ((standardLubinTateLevelToChangedLevelCompositum hπ u n x :
        standardLubinTateChangedLevelCompositumField hπ u n) :
      SeparableClosure K) =
        (x : SeparableClosure K)

theorem

standardLubinTateChangedLevelToCompositum_coe

L286 ↗

LubinTate.standardLubinTateChangedLevelToCompositum_coe

Documentation

The changed-level inclusion is the ambient identity on separable-closure elements.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelToCompositum_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (x : standardLubinTateChangedLevelField hπ u n) :
    ((standardLubinTateChangedLevelToCompositum hπ u n x :
        standardLubinTateChangedLevelCompositumField hπ u n) :
      SeparableClosure K) =
        (x : SeparableClosure K)

theorem

standardLubinTateLevelToChangedLevelCompositum_levelGenerator_coe

L300 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositum_levelGenerator_coe

Documentation

The original primitive generator has the same ambient value after inclusion in the compositum.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositum_levelGenerator_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    ((standardLubinTateLevelToChangedLevelCompositum hπ u n
          (standardLubinTateLevelGenerator hπ n) :
        standardLubinTateChangedLevelCompositumField hπ u n) :
      SeparableClosure K) =
        chosenStandardLubinTatePrimitiveRoot hπ n

theorem

standardLubinTateChangedLevelToCompositum_levelGenerator_coe

L315 ↗

LubinTate.standardLubinTateChangedLevelToCompositum_levelGenerator_coe

Documentation

The changed primitive generator has the same ambient value after inclusion in the compositum.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelToCompositum_levelGenerator_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    ((standardLubinTateChangedLevelToCompositum hπ u n
          (standardLubinTateChangedLevelGenerator hπ u n) :
        standardLubinTateChangedLevelCompositumField hπ u n) :
      SeparableClosure K) =
        chosenStandardLubinTatePrimitiveRoot
          (standardLubinTateChangedUniformizer_isUniformizer hπ u) n

def

standardLubinTateLevelToChangedLevelCompositumAlgebra

L330 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositumAlgebra

Documentation

The algebra structure corresponding to the original-level inclusion.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateLevelToChangedLevelCompositumAlgebra
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    Algebra (standardLubinTateLevelField hπ n)
      (standardLubinTateChangedLevelCompositumField hπ u n)

def

standardLubinTateChangedLevelToCompositumAlgebra

L342 ↗

LubinTate.standardLubinTateChangedLevelToCompositumAlgebra

Documentation

The algebra structure corresponding to the changed-level inclusion.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelToCompositumAlgebra
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    Algebra (standardLubinTateChangedLevelField hπ u n)
      (standardLubinTateChangedLevelCompositumField hπ u n)

theorem

standardLubinTateLevelToChangedLevelCompositum_hasExtension

L354 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositum_hasExtension

Documentation

The compositum valuation extends the chosen valuation on the original level.

Source context 8 commands

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

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

Lean source · full declaration

theorem standardLubinTateLevelToChangedLevelCompositum_hasExtension
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    letI : Algebra (standardLubinTateLevelField hπ n)
        (standardLubinTateChangedLevelCompositumField hπ u n) :=
      standardLubinTateLevelToChangedLevelCompositumAlgebra hπ u n
    (standardLubinTateLevelCompleteDVF hπ n).valuation.HasExtension
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation := by
  let L := standardLubinTateLevelField hπ n
  let M := standardLubinTateChangedLevelCompositumField hπ u n
  let level := standardLubinTateLevelCompleteDVF hπ n
  let target :=
    standardLubinTateChangedLevelCompositumCompleteDVF hπ u n
  let : Algebra L M :=
    standardLubinTateLevelToChangedLevelCompositumAlgebra hπ u n
  let : IsScalarTower K L M :=
    IsScalarTower.of_algebraMap_eq' rfl
  let vcomap := target.valuation.comap (algebraMap L M)
  let : F.toCompleteDVF.valuation.HasExtension vcomap :=
    { val_isEquiv_comap := by
        rw [_root_.Valuation.isEquiv_iff_val_le_one]
        intro a
        change
          F.toCompleteDVF.valuation a ≤ 1 ↔
            target.valuation
              (algebraMap L M (algebraMap K L a)) ≤ 1
        rw [← IsScalarTower.algebraMap_apply K L M]
        exact
          (_root_.Valuation.HasExtension.val_map_le_one_iff
            (vR := F.toCompleteDVF.valuation)
            (vA := target.valuation) a).symm }
  exact
    { val_isEquiv_comap := by
        simpa only [vcomap] using
          standardLubinTateLevelCompleteDVF_hasUniqueValuationExtension
            hπ n vcomap }

theorem

standardLubinTateChangedLevelToCompositum_hasExtension

L395 ↗

LubinTate.standardLubinTateChangedLevelToCompositum_hasExtension

Documentation

The compositum valuation extends the chosen valuation on the changed level.

Source context 8 commands

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

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

Lean source · full declaration

theorem standardLubinTateChangedLevelToCompositum_hasExtension
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    letI : Algebra (standardLubinTateChangedLevelField hπ u n)
        (standardLubinTateChangedLevelCompositumField hπ u n) :=
      standardLubinTateChangedLevelToCompositumAlgebra hπ u n
    (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).valuation.HasExtension
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation := by
  let hπ' :=
    standardLubinTateChangedUniformizer_isUniformizer hπ u
  let L' := standardLubinTateChangedLevelField hπ u n
  let M := standardLubinTateChangedLevelCompositumField hπ u n
  let level := standardLubinTateLevelCompleteDVF hπ' n
  let target :=
    standardLubinTateChangedLevelCompositumCompleteDVF hπ u n
  let : Algebra L' M :=
    standardLubinTateChangedLevelToCompositumAlgebra hπ u n
  let : IsScalarTower K L' M :=
    IsScalarTower.of_algebraMap_eq' rfl
  let vcomap := target.valuation.comap (algebraMap L' M)
  let : F.toCompleteDVF.valuation.HasExtension vcomap :=
    { val_isEquiv_comap := by
        rw [_root_.Valuation.isEquiv_iff_val_le_one]
        intro a
        change
          F.toCompleteDVF.valuation a ≤ 1 ↔
            target.valuation
              (algebraMap L' M (algebraMap K L' a)) ≤ 1
        rw [← IsScalarTower.algebraMap_apply K L' M]
        exact
          (_root_.Valuation.HasExtension.val_map_le_one_iff
            (vR := F.toCompleteDVF.valuation)
            (vA := target.valuation) a).symm }
  exact
    { val_isEquiv_comap := by
        simpa only [vcomap] using
          standardLubinTateLevelCompleteDVF_hasUniqueValuationExtension
            hπ' n vcomap }

theorem

standardLubinTateLevelToChangedLevelCompositum_val_le_one_iff

L440 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositum_val_le_one_iff

Documentation

The common valuation detects integrality of an original-level element exactly as the chosen original-level valuation does.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositum_val_le_one_iff
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (x : standardLubinTateLevelField hπ n) :
    (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation
        (standardLubinTateLevelToChangedLevelCompositum
          hπ u n x) ≤ 1 ↔
      (standardLubinTateLevelCompleteDVF hπ n).valuation x ≤ 1

theorem

standardLubinTateLevelToChangedLevelCompositum_val_lt_one_iff

L470 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositum_val_lt_one_iff

Documentation

The common valuation detects maximal-ideal membership of an original-level element.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositum_val_lt_one_iff
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (x : standardLubinTateLevelField hπ n) :
    (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation
        (standardLubinTateLevelToChangedLevelCompositum
          hπ u n x) < 1 ↔
      (standardLubinTateLevelCompleteDVF hπ n).valuation x < 1

theorem

standardLubinTateChangedLevelToCompositum_val_le_one_iff

L500 ↗

LubinTate.standardLubinTateChangedLevelToCompositum_val_le_one_iff

Documentation

The common valuation detects integrality of a changed-level element exactly as the chosen changed-level valuation does.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelToCompositum_val_le_one_iff
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (x : standardLubinTateChangedLevelField hπ u n) :
    (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation
        (standardLubinTateChangedLevelToCompositum hπ u n x) ≤ 1 ↔
      (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).valuation x ≤ 1

theorem

standardLubinTateChangedLevelToCompositum_val_lt_one_iff

L532 ↗

LubinTate.standardLubinTateChangedLevelToCompositum_val_lt_one_iff

Documentation

The common valuation detects maximal-ideal membership of a changed-level element.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelToCompositum_val_lt_one_iff
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (x : standardLubinTateChangedLevelField hπ u n) :
    (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuation
        (standardLubinTateChangedLevelToCompositum hπ u n x) < 1 ↔
      (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).valuation x < 1

def

standardLubinTateLevelToChangedLevelCompositumRamificationIndex

L564 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositumRamificationIndex

Documentation

The ramification index of the original level inside the common compositum.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositumRamificationIndex
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) : ℕ

def

standardLubinTateChangedLevelToCompositumRamificationIndex

L583 ↗

LubinTate.standardLubinTateChangedLevelToCompositumRamificationIndex

Documentation

The ramification index of the changed level inside the common compositum.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelToCompositumRamificationIndex
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) : ℕ

def

standardLubinTateLevelToChangedLevelCompositumIntegerMap

L602 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositumIntegerMap

Documentation

The valuation-ring map induced by the original-level inclusion.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositumIntegerMap
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring →+*
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuationSubring

def

standardLubinTateChangedLevelToCompositumIntegerMap

L623 ↗

LubinTate.standardLubinTateChangedLevelToCompositumIntegerMap

Documentation

The valuation-ring map induced by the changed-level inclusion.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelToCompositumIntegerMap
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).valuationSubring →+*
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).valuationSubring

theorem

standardLubinTateLevelToChangedLevelCompositumIntegerMap_apply_coe

L648 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositumIntegerMap_apply_coe

Documentation

Coercion of the original-level integer map is the field inclusion.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositumIntegerMap_apply_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (a :
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring) :
    (((standardLubinTateLevelToChangedLevelCompositumIntegerMap
          hπ u n a :
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring)) :
      standardLubinTateChangedLevelCompositumField hπ u n) =
        standardLubinTateLevelToChangedLevelCompositum
          hπ u n (a.val :
            standardLubinTateLevelField hπ n)

theorem

standardLubinTateChangedLevelToCompositumIntegerMap_apply_coe

L682 ↗

LubinTate.standardLubinTateChangedLevelToCompositumIntegerMap_apply_coe

Documentation

Coercion of the changed-level integer map is the field inclusion.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelToCompositumIntegerMap_apply_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (a :
      (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).valuationSubring) :
    (((standardLubinTateChangedLevelToCompositumIntegerMap
          hπ u n a :
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring)) :
      standardLubinTateChangedLevelCompositumField hπ u n) =
        standardLubinTateChangedLevelToCompositum
          hπ u n (a.val :
            standardLubinTateChangedLevelField hπ u n)

theorem

standardLubinTateLevelToChangedLevelCompositum_addVal

L719 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositum_addVal

Documentation

Normalized additive valuation along the original-level inclusion scales by its ramification index in the compositum.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateLevelToChangedLevelCompositum_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (a :
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring
        (standardLubinTateLevelToChangedLevelCompositumIntegerMap
          hπ u n a) =
      standardLubinTateLevelToChangedLevelCompositumRamificationIndex
          hπ u n •
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF
            hπ n).valuationSubring a

theorem

standardLubinTateChangedLevelToCompositum_addVal

L755 ↗

LubinTate.standardLubinTateChangedLevelToCompositum_addVal

Documentation

Normalized additive valuation along the changed-level inclusion scales by its ramification index in the compositum.

Source context 8 commands

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

noncomputable section
universe u v
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 standardLubinTateChangedLevelToCompositum_addVal
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ)
    (a :
      (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).valuationSubring) :
    IsDiscreteValuationRing.addVal
        (standardLubinTateChangedLevelCompositumCompleteDVF
          hπ u n).valuationSubring
        (standardLubinTateChangedLevelToCompositumIntegerMap
          hπ u n a) =
      standardLubinTateChangedLevelToCompositumRamificationIndex
          hπ u n •
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF
            (standardLubinTateChangedUniformizer_isUniformizer
              hπ u) n).valuationSubring a

theorem

nat_eq_of_nsmul_enat_eq

L793 ↗

LubinTate.nat_eq_of_nsmul_enat_eq

Source context 8 commands

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

noncomputable section
universe u v
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 nat_eq_of_nsmul_enat_eq
    {a b d : ℕ} (hd : 0 < d)
    (h : a • (d : ℕ∞) = b • (d : ℕ∞)) :
    a = b

theorem

standardLubinTateLevelToChangedLevelCompositumRamificationIndex_eq

L813 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositumRamificationIndex_eq

Documentation

The original and changed levels have the same ramification index inside their common compositum.

Both relative indices scale the valuation of the same base uniformizer. That uniformizer has the common finite-level valuation (q - 1) * q ^ n on either side, and its two images in the literal compositum agree. Positivity of the finite-level degree then permits cancellation.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositumRamificationIndex_eq
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n : ℕ) :
    standardLubinTateLevelToChangedLevelCompositumRamificationIndex
        hπ u n =
      standardLubinTateChangedLevelToCompositumRamificationIndex
        hπ u n

theorem

standardLubinTateLevelToChangedLevelCompositumIntegerMap_mem_maximalIdeal_pow

L915 ↗

LubinTate.standardLubinTateLevelToChangedLevelCompositumIntegerMap_mem_maximalIdeal_pow

Documentation

Original-level maximal-ideal depth scales by the ramification index in the compositum.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateLevelToChangedLevelCompositumIntegerMap_mem_maximalIdeal_pow
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n r : ℕ)
    {a :
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring}
    (ha :
      a ∈ (standardLubinTateLevelCompleteDVF
        hπ n).maximalIdeal ^ r) :
    standardLubinTateLevelToChangedLevelCompositumIntegerMap hπ u n a ∈
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).maximalIdeal ^
          (standardLubinTateLevelToChangedLevelCompositumRamificationIndex
            hπ u n * r)

theorem

standardLubinTateChangedLevelToCompositumIntegerMap_mem_maximalIdeal_pow

L950 ↗

LubinTate.standardLubinTateChangedLevelToCompositumIntegerMap_mem_maximalIdeal_pow

Documentation

Changed-level maximal-ideal depth scales by the ramification index in the compositum.

Source context 8 commands

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

noncomputable section
universe u v
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
    standardLubinTateChangedLevelToCompositumIntegerMap_mem_maximalIdeal_pow
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (u : F.valuationSubringˣ) (n r : ℕ)
    {a :
      (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).valuationSubring}
    (ha :
      a ∈ (standardLubinTateLevelCompleteDVF
        (standardLubinTateChangedUniformizer_isUniformizer
          hπ u) n).maximalIdeal ^ r) :
    standardLubinTateChangedLevelToCompositumIntegerMap hπ u n a ∈
      (standardLubinTateChangedLevelCompositumCompleteDVF
        hπ u n).maximalIdeal ^
          (standardLubinTateChangedLevelToCompositumRamificationIndex
            hπ u n * r)

Module documentation

A common valued field for original and changed Lubin--Tate levels

Declarations