Module

CompletedLevel.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedLevel

52 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: a completed Lubin--Tate level field

Let k be the residue field and put K∞ = (AlgebraicClosure k)((T)). This file base-changes the primitive Lubin--Tate polynomial to K∞, takes its genuine splitting field, and equips that finite extension with the spectral norm. A chosen primitive root is proved to lie in the maximal ideal of the resulting complete valued field, hence is an actual analytic evaluation point for the theta series of the completed theta-intertwining theorem.

Imports7

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.CompletedUnramifiedField
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.PrimitiveIrreducible
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.PrimitiveTorsion
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.LevelField
Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Mathlib.FieldTheory.SplittingField.Construction

Imported by6

instance

equalCharacteristicCompletedLevelBaseAlgebra

L45 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelBaseAlgebra

Documentation

The coefficientwise algebra structure k((T)) → (AlgebraicClosure k)((T)).

Source context 8 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)

instance

equalCharacteristicCompletedLevelBaseCharP

L51 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelBaseCharP

Source context 9 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

instance equalCharacteristicCompletedLevelBaseCharP
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] :
    CharP (equalCharacteristicCompletedUnramifiedField F.residueField)
      F.residueCharacteristic

theorem

equalCharacteristicCompletedBaseValuationIsNontrivial

L63 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseValuationIsNontrivial

Documentation

The Laurent valuation on the completed maximal-unramified base is nontrivial, witnessed by T.

Source context 9 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial

instance

equalCharacteristicCompletedBaseValuationIsNontrivialInstance

L85 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseValuationIsNontrivialInstance

Source context 9 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial

def

equalCharacteristicCompletedBaseValuationRankOne

L93 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseValuationRankOne

Documentation

The rank-one structure on the discrete Laurent valuation.

Source context 10 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k

Lean source · statement

def equalCharacteristicCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne

instance

equalCharacteristicCompletedBaseValuationRankOneInstance

L101 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseValuationRankOneInstance

Source context 10 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k

Lean source · statement

instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne

def

equalCharacteristicCompletedBaseNormedField

L109 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseNormedField

Documentation

The norm on the completed-unramified Laurent field induced by its rank-one valuation.

Source context 11 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k

Lean source · statement

def equalCharacteristicCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k)

instance

equalCharacteristicCompletedBaseNormedFieldInstance

L116 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseNormedFieldInstance

Source context 11 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k

Lean source · statement

instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k)

def

equalCharacteristicCompletedPrimitivePolynomial

L124 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial

Documentation

The primitive level-n+1 polynomial after coefficientwise base change to (AlgebraicClosure k)((T)).

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

def equalCharacteristicCompletedPrimitivePolynomial
    (F : LocalField.{u, v} K) (n : ℕ) :
    Polynomial (equalCharacteristicCompletedUnramifiedField F.residueField)

theorem

equalCharacteristicCompletedPrimitivePolynomial_monic

L132 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_monic

Documentation

The completed primitive polynomial is monic.

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

theorem equalCharacteristicCompletedPrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedPrimitivePolynomial F n).Monic

theorem

equalCharacteristicCompletedPrimitivePolynomial_natDegree

L138 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_natDegree

Documentation

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

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

theorem equalCharacteristicCompletedPrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedPrimitivePolynomial F n).natDegree =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

def

equalCharacteristicCompletedLevelField

L147 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelField

Documentation

The actual finite completed level field used to evaluate theta.

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

def equalCharacteristicCompletedLevelField
    (F : LocalField.{u, v} K) (n : ℕ)

instance

equalCharacteristicCompletedLevelField_field

L152 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelField_field

Documentation

The splitting field of the completed primitive polynomial is a field.

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

instance equalCharacteristicCompletedLevelField_field
    (F : LocalField.{u, v} K) (n : ℕ) :
    Field (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelField_algebra

L159 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelField_algebra

Documentation

The completed level field is an algebra over the completed unramified field.

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

instance equalCharacteristicCompletedLevelField_algebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelLaurentAlgebra

L167 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelLaurentAlgebra

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelScalarTower

L176 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelScalarTower

Source context 13 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra

Lean source · statement

instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelCharP

L183 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelCharP

Source context 14 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

instance equalCharacteristicCompletedLevelCharP
    (F : LocalField.{u, v} K) [CharP K F.residueCharacteristic]
    (n : ℕ) :
    CharP (equalCharacteristicCompletedLevelField F n)
      F.residueCharacteristic

instance

equalCharacteristicCompletedLevelField_module

L195 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelField_module

Source context 15 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section

Lean source · statement

instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid

instance

equalCharacteristicCompletedLevelField_finiteDimensionalInstance

L209 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelField_finiteDimensionalInstance

Documentation

The completed level field is finite-dimensional over its completed base.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

instance equalCharacteristicCompletedLevelField_finiteDimensionalInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    FiniteDimensional
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelField_isAlgebraic

L220 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelField_isAlgebraic

Documentation

The completed level field is algebraic over its completed base.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

instance equalCharacteristicCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

def

equalCharacteristicCompletedLevelFieldEquivSplittingField

L232 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelFieldEquivSplittingField

Documentation

Comparison with the library splitting-field model.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

def equalCharacteristicCompletedLevelFieldEquivSplittingField
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicCompletedLevelField F n ≃ₐ[
      equalCharacteristicCompletedUnramifiedField F.residueField]
      (equalCharacteristicCompletedPrimitivePolynomial F n).SplittingField

def

equalCharacteristicCompletedLevelFieldOfSplittingField

L241 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelFieldOfSplittingField

Documentation

Construct a named completed-level element from the splitting-field model.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

def equalCharacteristicCompletedLevelFieldOfSplittingField
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedPrimitivePolynomial F n).SplittingField →ₐ[
      equalCharacteristicCompletedUnramifiedField F.residueField]
      equalCharacteristicCompletedLevelField F n

theorem

equalCharacteristicCompletedPrimitivePolynomial_splits

L250 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_splits

Documentation

The defining primitive polynomial splits over the named completed level field.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

theorem equalCharacteristicCompletedPrimitivePolynomial_splits
    (F : LocalField.{u, v} K) (n : ℕ) :
    ((equalCharacteristicCompletedPrimitivePolynomial F n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n))).Splits

theorem

equalCharacteristicCompletedPrimitivePolynomial_adjoin_rootSet

L260 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_adjoin_rootSet

Documentation

The roots of the defining polynomial generate the named completed level field.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

theorem equalCharacteristicCompletedPrimitivePolynomial_adjoin_rootSet
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ((equalCharacteristicCompletedPrimitivePolynomial F n).rootSet
          (equalCharacteristicCompletedLevelField F n) :
          Set (equalCharacteristicCompletedLevelField F n)) = ⊤

theorem

equalCharacteristicCompletedLevelField_finiteDimensional

L272 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelField_finiteDimensional

Documentation

The completed level field is finite-dimensional over the completed maximal-unramified Laurent field.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

theorem equalCharacteristicCompletedLevelField_finiteDimensional
    (F : LocalField.{u, v} K) (n : ℕ) :
    FiniteDimensional
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicCompletedPrimitivePolynomial_map_degree_ne_zero

L279 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_map_degree_ne_zero

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

theorem equalCharacteristicCompletedPrimitivePolynomial_map_degree_ne_zero
    (F : LocalField.{u, v} K) (n : ℕ) :
    ((equalCharacteristicCompletedPrimitivePolynomial F n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n))).degree ≠ 0

def

equalCharacteristicCompletedPrimitiveRoot

L296 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot

Documentation

A chosen primitive root in the completed level field.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

def equalCharacteristicCompletedPrimitiveRoot
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicCompletedLevelField F n

theorem

equalCharacteristicCompletedPrimitiveRoot_isRoot

L307 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_isRoot

Documentation

The chosen element is a root of the base-changed primitive polynomial.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

theorem equalCharacteristicCompletedPrimitiveRoot_isRoot
    (F : LocalField.{u, v} K) (n : ℕ) :
    ((equalCharacteristicCompletedPrimitivePolynomial F n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n))).IsRoot
          (equalCharacteristicCompletedPrimitiveRoot F n)

def

equalCharacteristicCompletedLevelNormedField

L319 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelNormedField

Documentation

The spectral norm on the finite completed level field.

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

def equalCharacteristicCompletedLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelNormedFieldInstance

L326 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelNormedFieldInstance

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)

Lean source · statement

instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicCompletedLevelIsUltrametric

L332 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelIsUltrametric

Documentation

The spectral norm is nonarchimedean.

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n

Lean source · statement

theorem equalCharacteristicCompletedLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelIsUltrametricInstance

L343 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelIsUltrametricInstance

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n

Lean source · statement

instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicCompletedLevelCompleteSpace

L349 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelCompleteSpace

Documentation

Finite dimensionality makes the spectral level field complete.

Source context 18 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n

Lean source · statement

theorem equalCharacteristicCompletedLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedLevelCompleteSpaceInstance

L356 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelCompleteSpaceInstance

Source context 18 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n

Lean source · statement

instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n)

def

equalCharacteristicCompletedLevelValued

L362 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelValued

Documentation

The valuation attached to the spectral norm.

Source context 19 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n

Lean source · statement

def equalCharacteristicCompletedLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0

instance

equalCharacteristicCompletedLevelValuedInstance

L367 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelValuedInstance

Source context 19 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n

Lean source · statement

instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0

def

equalCharacteristicCompletedBaseUniformizer

L373 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseUniformizer

Documentation

The Laurent parameter in the completed maximal-unramified base.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

def equalCharacteristicCompletedBaseUniformizer
    (F : LocalField.{u, v} K) :
    equalCharacteristicCompletedUnramifiedField F.residueField

theorem

equalCharacteristicCompletedBase_algebraMap_uniformizer

L379 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBase_algebraMap_uniformizer

Documentation

Coefficientwise base change fixes the Laurent parameter.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedBase_algebraMap_uniformizer
    (F : LocalField.{u, v} K) :
    algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicLaurentUniformizer F) =
      equalCharacteristicCompletedBaseUniformizer F

theorem

equalCharacteristicCompletedBaseUniformizer_norm_lt_one

L408 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedBaseUniformizer_norm_lt_one

Documentation

The completed-base Laurent parameter has norm strictly less than one.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedBaseUniformizer_norm_lt_one
    (F : LocalField.{u, v} K) :
    ‖equalCharacteristicCompletedBaseUniformizer F‖ < 1

def

equalCharacteristicCompletedLevelUniformizer

L427 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelUniformizer

Documentation

The image of T in the completed level field.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

def equalCharacteristicCompletedLevelUniformizer
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicCompletedLevelField F n

theorem

equalCharacteristicCompletedLevelUniformizer_norm

L435 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelUniformizer_norm

Documentation

The spectral norm extends the norm of the completed-unramified base.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedLevelUniformizer_norm
    (F : LocalField.{u, v} K) (n : ℕ) :
    ‖equalCharacteristicCompletedLevelUniformizer F n‖ =
      ‖equalCharacteristicCompletedBaseUniformizer F‖

theorem

equalCharacteristicCompletedLevelUniformizer_norm_lt_one

L448 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelUniformizer_norm_lt_one

Documentation

The completed level uniformizer has norm strictly below one.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedLevelUniformizer_norm_lt_one
    (F : LocalField.{u, v} K) (n : ℕ) :
    ‖equalCharacteristicCompletedLevelUniformizer F n‖ < 1

theorem

equalCharacteristicCompletedPrimitiveRoot_equation

L456 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_equation

Documentation

The chosen root satisfies the genuine primitive Lubin--Tate equation over the completed-unramified base.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedPrimitiveRoot_equation
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicCompletedLevelUniformizer F n) n
        (equalCharacteristicCompletedPrimitiveRoot F n) ^
          (Nat.card F.residueField - 1) +
      equalCharacteristicCompletedLevelUniformizer F n = 0

def

equalCharacteristicLubinTateLevelFieldToCompleted

L490 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToCompleted

Documentation

The original separable-closure level field embeds into the completed level field, sending its primitive generator to the chosen completed root.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

def equalCharacteristicLubinTateLevelFieldToCompleted
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateLevelField F n →ₐ[F.residueField⸨X⸩]
      equalCharacteristicCompletedLevelField F n

theorem

equalCharacteristicLubinTateLevelFieldToCompleted_generator

L538 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToCompleted_generator

Documentation

The canonical finite-level embedding sends its simple-extension generator to the chosen primitive root in the completed level field.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicLubinTateLevelFieldToCompleted_generator
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateLevelFieldToCompleted F n
        (IntermediateField.AdjoinSimple.gen F.residueField⸨X⸩
          (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)) =
      equalCharacteristicCompletedPrimitiveRoot F n

theorem

equalCharacteristicCompletedAmbientPiEnd_norm_of_one_le

L562 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedAmbientPiEnd_norm_of_one_le

Documentation

If x has norm at least one, then e(x) = x^q + Tx has the same norm as its leading term.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedAmbientPiEnd_norm_of_one_le
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (x : equalCharacteristicCompletedLevelField F n)
    (hx : 1 ≤ ‖x‖) :
    ‖equalCharacteristicLubinTateAmbientPiEnd F
        (equalCharacteristicCompletedLevelUniformizer F n) x‖ =
      ‖x‖ ^ Nat.card F.residueField

theorem

equalCharacteristicCompletedAmbientPiIterate_norm_of_one_le

L601 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedAmbientPiIterate_norm_of_one_le

Documentation

Above the unit sphere, every Lubin--Tate iterate has the norm of its leading q-power term.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedAmbientPiIterate_norm_of_one_le
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (level i : ℕ) (x : equalCharacteristicCompletedLevelField F level)
    (hx : 1 ≤ ‖x‖) :
    ‖equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicCompletedLevelUniformizer F level) i x‖ =
      ‖x‖ ^ (Nat.card F.residueField ^ i)

theorem

equalCharacteristicCompletedPrimitiveRoot_norm_lt_one

L631 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_norm_lt_one

Documentation

The primitive root lies strictly inside the unit ball. This follows directly from its Lubin--Tate equation and the spectral norm.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedPrimitiveRoot_norm_lt_one
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ‖equalCharacteristicCompletedPrimitiveRoot F n‖ < 1

def

equalCharacteristicCompletedPrimitiveRootInteger

L665 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRootInteger

Documentation

The primitive root lifted to the spectral valuation ring.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

def equalCharacteristicCompletedPrimitiveRootInteger
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Valued.integer (equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicCompletedPrimitiveRootInteger_coe

L677 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRootInteger_coe

Documentation

Coercing the integral primitive root returns the underlying completed root.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedPrimitiveRootInteger_coe
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ((equalCharacteristicCompletedPrimitiveRootInteger F n :
      Valued.integer (equalCharacteristicCompletedLevelField F n)) :
        equalCharacteristicCompletedLevelField F n) =
      equalCharacteristicCompletedPrimitiveRoot F n

theorem

equalCharacteristicCompletedPrimitiveRootInteger_mem_maximalIdeal

L688 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRootInteger_mem_maximalIdeal

Documentation

The integral primitive root belongs to the maximal ideal.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedPrimitiveRootInteger_mem_maximalIdeal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicCompletedPrimitiveRootInteger F n ∈
      Valued.maximalIdeal (equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicCompletedPrimitiveRootInteger_hasEval

L705 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRootInteger_hasEval

Documentation

The primitive root is a genuine analytic evaluation point for outer power series over the completed level integer ring.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The coefficientwise algebra structure
`k((T)) → (AlgebraicClosure k)((T))`. -/
noncomputable local instance equalCharacteristicCompletedLevelBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicCompletedBaseValuationIsNontrivialInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicCompletedBaseValuationRankOneInstance
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicCompletedBaseNormedFieldInstance
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
noncomputable local instance equalCharacteristicCompletedLevelLaurentAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)).comp
    (algebraMap F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField))).toAlgebra
noncomputable local instance equalCharacteristicCompletedLevelScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
section
local instance equalCharacteristicCompletedLevelField_module
    (F : LocalField.{u, v} K) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicCompletedLevelField F n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicCompletedLevelField F n) _ _
    (equalCharacteristicCompletedLevelField_algebra F n)
noncomputable local instance equalCharacteristicCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

theorem equalCharacteristicCompletedPrimitiveRootInteger_hasEval
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    PowerSeries.HasEval
      (equalCharacteristicCompletedPrimitiveRootInteger F n)

Module documentation

The completed theta-intertwining theorem: a completed Lubin--Tate level field

Declarations