NYLL
Module

CompletedLevel.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedLevel
47 declarations indexed from sourceView source ↗

Module documentation

Completed p-adic Lubin--Tate levels

For the completed maximal-unramified coefficient field

E = Frac(W(AlgebraicClosure (ZMod p))),

this file base-changes the standard primitive Lubin--Tate polynomial from ℚ_[p] to E and takes its actual splitting field. The complete discrete valuation on that finite separable extension is selected from the integral closure of the canonical Witt valuation ring. This is the mixed- characteristic evaluation field needed by the changed-uniformizer descent.

The integral polynomial, splitting field, and valuations below are the existing mathlib/LCFT objects. No parallel p-adic field, integer ring, or completion is introduced.

Imports7
Imported by3

Declarations

def

padicCompletedPrimitivePolynomialInteger

L51 ↗
LubinTate.padicCompletedPrimitivePolynomialInteger
Documentation

The primitive standard Lubin--Tate polynomial over the canonical valuation ring of the completed-unramified field.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
def padicCompletedPrimitivePolynomialInteger
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial
      (padicCompletedUnramifiedCompleteDVF p).valuationSubring
def

padicCompletedPrimitivePolynomial

L62 ↗
LubinTate.padicCompletedPrimitivePolynomial
Documentation

The primitive standard Lubin--Tate polynomial after base change from ℚ_[p] to the completed-unramified fraction field.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
def padicCompletedPrimitivePolynomial
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial (padicCompletedUnramifiedField p)
theorem

padicCompletedPrimitivePolynomialInteger_map

L72 ↗
LubinTate.padicCompletedPrimitivePolynomialInteger_map
Documentation

Mapping the integral completed primitive polynomial to the fraction field gives the field-valued base change.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomialInteger_map
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomialInteger p n).map
        (algebraMap
          (padicCompletedUnramifiedCompleteDVF p).valuationSubring
          (padicCompletedUnramifiedField p)) =
      padicCompletedPrimitivePolynomial p n
theorem

padicCompletedPrimitivePolynomialInteger_monic

L100 ↗
LubinTate.padicCompletedPrimitivePolynomialInteger_monic
Documentation

The integral completed primitive polynomial is monic.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomialInteger_monic
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomialInteger p n).Monic
theorem

padicCompletedPrimitivePolynomial_monic

L108 ↗
LubinTate.padicCompletedPrimitivePolynomial_monic
Documentation

The field-valued completed primitive polynomial is monic.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomial_monic
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomial p n).Monic
theorem

padicCompletedPrimitivePolynomial_natDegree

L116 ↗
LubinTate.padicCompletedPrimitivePolynomial_natDegree
Documentation

The completed primitive polynomial has degree (p - 1) * p ^ n.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomial_natDegree
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomial p n).natDegree =
      (p - 1) * p ^ n
theorem

padicCompletedPrimitivePolynomial_separable

L140 ↗
LubinTate.padicCompletedPrimitivePolynomial_separable
Documentation

The completed primitive polynomial remains separable after base change.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomial_separable
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomial p n).Separable
def

padicCompletedLevelField

L148 ↗
LubinTate.padicCompletedLevelField
Documentation

The actual finite splitting field over the completed-unramified coefficient field.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
def padicCompletedLevelField
    (p : ℕ) [Fact p.Prime] (n : ℕ)
instance

padicCompletedLevelField_field

L153 ↗
LubinTate.padicCompletedLevelField_field
Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
instance padicCompletedLevelField_field
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Field (padicCompletedLevelField p n)
instance

padicCompletedLevelField_algebra

L160 ↗
LubinTate.padicCompletedLevelField_algebra
Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
instance padicCompletedLevelField_algebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
instance

padicCompletedLevelField_module

L170 ↗
LubinTate.padicCompletedLevelField_module
Source context 11 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
section
Lean source · statement
instance padicCompletedLevelField_module
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    @Module (padicCompletedUnramifiedField p) (padicCompletedLevelField p n)
      (inferInstance : DivisionRing (padicCompletedUnramifiedField p)).toRing.toSemiring
      (inferInstance : AddCommGroup (padicCompletedLevelField p n)).toAddCommMonoid
instance

padicCompletedLevelField_finiteDimensional

L178 ↗
LubinTate.padicCompletedLevelField_finiteDimensional
Source context 12 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
section
local instance padicCompletedLevelField_module
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    @Module (padicCompletedUnramifiedField p) (padicCompletedLevelField p n)
      (inferInstance : DivisionRing (padicCompletedUnramifiedField p)).toRing.toSemiring
      (inferInstance : AddCommGroup (padicCompletedLevelField p n)).toAddCommMonoid :=
  @Algebra.toModule (padicCompletedUnramifiedField p) (padicCompletedLevelField p n)
    _ _ (padicCompletedLevelField_algebra p n)
Lean source · statement
instance padicCompletedLevelField_finiteDimensional
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    FiniteDimensional (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
instance

padicCompletedLevelField_isGalois

L190 ↗
LubinTate.padicCompletedLevelField_isGalois
Documentation

The completed level is the splitting field of a separable polynomial, hence is Galois over its completed-unramified base.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
instance padicCompletedLevelField_isGalois
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsGalois (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
theorem

padicCompletedPrimitivePolynomial_splits

L201 ↗
LubinTate.padicCompletedPrimitivePolynomial_splits
Documentation

The completed primitive polynomial splits over the completed level.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomial_splits
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    ((padicCompletedPrimitivePolynomial p n).map
      (algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n))).Splits
theorem

padicCompletedPrimitivePolynomial_adjoin_rootSet

L211 ↗
LubinTate.padicCompletedPrimitivePolynomial_adjoin_rootSet
Documentation

The roots of the completed primitive polynomial generate its splitting field.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomial_adjoin_rootSet
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra.adjoin (padicCompletedUnramifiedField p)
        ((padicCompletedPrimitivePolynomial p n).rootSet
          (padicCompletedLevelField p n) :
          Set (padicCompletedLevelField p n)) =
      ⊤
theorem

padicCompletedPrimitivePolynomial_map_degree_ne_zero

L221 ↗
LubinTate.padicCompletedPrimitivePolynomial_map_degree_ne_zero
Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomial_map_degree_ne_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    ((padicCompletedPrimitivePolynomial p n).map
      (algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n))).degree ≠ 0
def

padicCompletedPrimitiveRoot

L239 ↗
LubinTate.padicCompletedPrimitiveRoot
Documentation

A chosen primitive standard division point in the completed level.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
def padicCompletedPrimitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedLevelField p n
theorem

padicCompletedPrimitiveRoot_isRoot

L249 ↗
LubinTate.padicCompletedPrimitiveRoot_isRoot
Documentation

The chosen completed primitive point is a root of the genuine base-changed primitive polynomial.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitiveRoot_isRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    ((padicCompletedPrimitivePolynomial p n).map
      (algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n))).IsRoot
      (padicCompletedPrimitiveRoot p n)
theorem

padicCompletedPrimitiveRoot_aeval_integerPolynomial

L262 ↗
LubinTate.padicCompletedPrimitiveRoot_aeval_integerPolynomial
Documentation

The integral completed primitive polynomial annihilates the chosen root in the actual splitting field.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitiveRoot_aeval_integerPolynomial
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.aeval (padicCompletedPrimitiveRoot p n)
        (padicCompletedPrimitivePolynomialInteger p n) = 0
theorem

padicCompletedPrimitiveRoot_isIntegral

L290 ↗
LubinTate.padicCompletedPrimitiveRoot_isIntegral
Documentation

The chosen primitive point is integral over the canonical Witt valuation ring.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitiveRoot_isIntegral
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsIntegral
      (padicCompletedUnramifiedCompleteDVF p).valuationSubring
      (padicCompletedPrimitiveRoot p n)
theorem

padicCompletedLevelCompleteDVFData_exists

L299 ↗
LubinTate.padicCompletedLevelCompleteDVFData_exists
Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · full declaration
theorem padicCompletedLevelCompleteDVFData_exists
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    ∃ target : CompleteDVF.{0, 0} (padicCompletedLevelField p n),
      ∃ hExt :
          (padicCompletedUnramifiedCompleteDVF p).valuation.HasExtension
            target.valuation,
        letI :
            (padicCompletedUnramifiedCompleteDVF p).valuation.HasExtension
              target.valuation := hExt
        IsIntegralClosure target.valuationSubring
            (padicCompletedUnramifiedCompleteDVF p).valuationSubring
            (padicCompletedLevelField p n) ∧
          degree (padicCompletedUnramifiedCompleteDVF p).toDVF target.toDVF =
            ramificationIndex
                (padicCompletedUnramifiedCompleteDVF p).toDVF target.toDVF *
              residueDegree
                (padicCompletedUnramifiedCompleteDVF p).toDVF target.toDVF := by
  exact
    exists_integralClosure_standard_fundamental_identity
      (K := padicCompletedUnramifiedField p)
      (L := padicCompletedLevelField p n)
      (padicCompletedUnramifiedCompleteDVF p)
def

padicCompletedLevelCompleteDVF

L324 ↗
LubinTate.padicCompletedLevelCompleteDVF
Documentation

The complete discrete valuation on the completed level selected from its actual integral closure over the Witt valuation ring.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
def padicCompletedLevelCompleteDVF
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteDVF.{0, 0} (padicCompletedLevelField p n)
theorem

padicCompletedLevelCompleteDVF_hasExtension

L331 ↗
LubinTate.padicCompletedLevelCompleteDVF_hasExtension
Documentation

The selected completed-level valuation extends the completed-unramified base valuation.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedLevelCompleteDVF_hasExtension
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedUnramifiedCompleteDVF p).valuation.HasExtension
      (padicCompletedLevelCompleteDVF p n).valuation
instance

padicCompletedLevelCompleteDVF_hasExtensionInstance

L339 ↗
LubinTate.padicCompletedLevelCompleteDVF_hasExtensionInstance
Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
instance padicCompletedLevelCompleteDVF_hasExtensionInstance
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedUnramifiedCompleteDVF p).valuation.HasExtension
      (padicCompletedLevelCompleteDVF p n).valuation
theorem

padicCompletedLevelCompleteDVF_isIntegralClosure

L347 ↗
LubinTate.padicCompletedLevelCompleteDVF_isIntegralClosure
Documentation

The completed-level valuation ring is the actual integral closure of the completed-unramified valuation ring.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedLevelCompleteDVF_isIntegralClosure
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsIntegralClosure
      (padicCompletedLevelCompleteDVF p n).valuationSubring
      (padicCompletedUnramifiedCompleteDVF p).valuationSubring
      (padicCompletedLevelField p n)
theorem

padicCompletedPrimitiveRoot_mem_valuationSubring

L359 ↗
LubinTate.padicCompletedPrimitiveRoot_mem_valuationSubring
Documentation

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

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitiveRoot_mem_valuationSubring
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedPrimitiveRoot p n ∈
      (padicCompletedLevelCompleteDVF p n).valuation.valuationSubring
def

padicCompletedPrimitiveRootInteger

L383 ↗
LubinTate.padicCompletedPrimitiveRootInteger
Documentation

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

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
def padicCompletedPrimitiveRootInteger
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedPrimitiveRootInteger_coe

L392 ↗
LubinTate.padicCompletedPrimitiveRootInteger_coe
Documentation

Coercing the integral primitive point returns the chosen splitting-field root.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitiveRootInteger p n :
      padicCompletedLevelField p n) =
        padicCompletedPrimitiveRoot p n
theorem

padicCompletedPrimitiveRootInteger_aeval

L401 ↗
LubinTate.padicCompletedPrimitiveRootInteger_aeval
Documentation

The integral primitive polynomial annihilates the primitive point in the completed-level valuation ring.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_aeval
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.aeval (padicCompletedPrimitiveRootInteger p n)
        (padicCompletedPrimitivePolynomialInteger p n) = 0
theorem

padicCompletedPrimitivePolynomialInteger_isWeaklyEisensteinAt

L421 ↗
LubinTate.padicCompletedPrimitivePolynomialInteger_isWeaklyEisensteinAt
Documentation

Base change preserves the weak Eisenstein condition for the completed primitive polynomial.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitivePolynomialInteger_isWeaklyEisensteinAt
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePolynomialInteger p n).IsWeaklyEisensteinAt
      (padicCompletedUnramifiedCompleteDVF p).maximalIdeal
theorem

padicCompletedPrimitiveRootInteger_mem_maximalIdeal

L434 ↗
LubinTate.padicCompletedPrimitiveRootInteger_mem_maximalIdeal
Documentation

The completed primitive point lies in the maximal ideal of the selected level valuation ring.

Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_mem_maximalIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedPrimitiveRootInteger p n ∈
      (padicCompletedLevelCompleteDVF p n).maximalIdeal
instance

padicCompletedLevelWittUniformSpace

L469 ↗
LubinTate.padicCompletedLevelWittUniformSpace
Source context 10 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p)
instance

padicCompletedLevelTargetWithIdeal

L475 ↗
LubinTate.padicCompletedLevelTargetWithIdeal
Source context 11 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
Lean source · full declaration
instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
instance

padicCompletedLevelTargetCompleteSpace

L482 ↗
LubinTate.padicCompletedLevelTargetCompleteSpace
Source context 12 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
Lean source · statement
instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring
instance

padicCompletedLevelTargetT2Space

L491 ↗
LubinTate.padicCompletedLevelTargetT2Space
Source context 13 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
Lean source · statement
instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedPrimitiveRootInteger_hasEval

L502 ↗
LubinTate.padicCompletedPrimitiveRootInteger_hasEval
Documentation

The chosen completed primitive point is a genuine convergent evaluation point for Witt-coefficient power series.

Source context 14 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRootInteger_hasEval
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    PowerSeries.HasEval (padicCompletedPrimitiveRootInteger p n)
def

padicCompletedLevelWittCoefficientHom

L510 ↗
LubinTate.padicCompletedLevelWittCoefficientHom
Documentation

The canonical Witt-coefficient map into the valuation ring of the actual completed level.

Source context 14 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedLevelWittCoefficientHom
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedUnramifiedWittRing p →+*
      (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedLevelWittCoefficientHom_apply

L522 ↗
LubinTate.padicCompletedLevelWittCoefficientHom_apply
Documentation

The Witt-coefficient map is the ambient fraction-field algebra map after coercion.

Source context 14 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedLevelWittCoefficientHom_apply
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : padicCompletedUnramifiedWittRing p) :
    ((padicCompletedLevelWittCoefficientHom p n a :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
      padicCompletedLevelField p n) =
        algebraMap (padicCompletedUnramifiedField p)
          (padicCompletedLevelField p n)
          (algebraMap (padicCompletedUnramifiedWittRing p)
            (padicCompletedUnramifiedField p) a)
theorem

padicCompletedLevelWittCoefficientHom_continuous

L536 ↗
LubinTate.padicCompletedLevelWittCoefficientHom_continuous
Documentation

With the discrete coefficient topology, the canonical Witt map into the completed level is continuous.

Source context 14 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedLevelWittCoefficientHom_continuous
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Continuous (padicCompletedLevelWittCoefficientHom p n)
instance

padicCompletedLevelWittAlgebra

L541 ↗
LubinTate.padicCompletedLevelWittAlgebra
Source context 14 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring
def

padicCompletedLevelPowerSeriesEval

L550 ↗
LubinTate.padicCompletedLevelPowerSeriesEval
Documentation

Analytic evaluation of Witt-coefficient power series in the actual completed level.

Source context 15 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring :=
  (padicCompletedLevelWittCoefficientHom p n).toAlgebra
Lean source · statement
def padicCompletedLevelPowerSeriesEval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    (padicCompletedUnramifiedWittRing p)⟦X⟧ →+*
      (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedLevelPowerSeriesEval_X

L562 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_X
Documentation

Completed-level evaluation sends the power-series variable to the chosen evaluation point.

Source context 15 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring :=
  (padicCompletedLevelWittCoefficientHom p n).toAlgebra
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_X
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    padicCompletedLevelPowerSeriesEval p n x hx PowerSeries.X = x
theorem

padicCompletedLevelPowerSeriesEval_C

L573 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_C
Documentation

Completed-level evaluation sends constants through the canonical Witt coefficient map.

Source context 15 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring :=
  (padicCompletedLevelWittCoefficientHom p n).toAlgebra
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_C
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a : padicCompletedUnramifiedWittRing p) :
    padicCompletedLevelPowerSeriesEval p n x hx (PowerSeries.C a) =
      padicCompletedLevelWittCoefficientHom p n a
theorem

padicCompletedLevelPowerSeriesEval_coe

L586 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_coe
Documentation

On polynomial power series, completed-level analytic evaluation agrees with ordinary polynomial evaluation.

Source context 15 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring :=
  (padicCompletedLevelWittCoefficientHom p n).toAlgebra
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (P : Polynomial (padicCompletedUnramifiedWittRing p)) :
    padicCompletedLevelPowerSeriesEval p n x hx
        (P : PowerSeries (padicCompletedUnramifiedWittRing p)) =
      Polynomial.eval₂
        (padicCompletedLevelWittCoefficientHom p n) x P
theorem

padicCompletedLevelPowerSeriesEval_continuous

L600 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_continuous
Documentation

Evaluation at a topologically nilpotent completed-level integer is continuous.

Source context 15 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring :=
  (padicCompletedLevelWittCoefficientHom p n).toAlgebra
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_continuous
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    Continuous (padicCompletedLevelPowerSeriesEval p n x hx)
theorem

padicCompletedLevelPowerSeriesEval_hasEval

L612 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_hasEval
Documentation

Evaluating a Witt-coefficient series with zero constant coefficient produces another topologically nilpotent completed-level integer.

Source context 15 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring :=
  (padicCompletedLevelWittCoefficientHom p n).toAlgebra
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_hasEval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (f : PowerSeries (padicCompletedUnramifiedWittRing p))
    (hf : PowerSeries.HasSubst f) :
    PowerSeries.HasEval
      (padicCompletedLevelPowerSeriesEval p n x hx f)
theorem

padicCompletedLevelPowerSeriesEval_subst

L625 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_subst
Documentation

Completed-level analytic evaluation commutes with one-variable formal substitution.

Source context 15 commands

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

noncomputable section
open Filter
open scoped Polynomial
open scoped PowerSeries
open scoped PowerSeries.WithPiTopology
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
private noncomputable local instance (priority := 50)
    padicCompletedLevelWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedLevelTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedLevelTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedLevelTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    padicCompletedLevelWittAlgebra
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra (padicCompletedUnramifiedWittRing p)
      (padicCompletedLevelCompleteDVF p n).valuationSubring :=
  (padicCompletedLevelWittCoefficientHom p n).toAlgebra
Lean source · statement
theorem padicCompletedLevelPowerSeriesEval_subst
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (a f : PowerSeries (padicCompletedUnramifiedWittRing p))
    (ha : PowerSeries.HasSubst a)
    (haEval : PowerSeries.HasEval
      (padicCompletedLevelPowerSeriesEval p n x hx a)) :
    padicCompletedLevelPowerSeriesEval p n x hx
        (PowerSeries.subst a f) =
      padicCompletedLevelPowerSeriesEval p n
        (padicCompletedLevelPowerSeriesEval p n x hx a)
        haEval f

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