Module

ChangedCompletedLevel.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ChangedCompletedLevel

53 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: the completed changed-uniformizer level

For u ∈ κ⟦T⟧ˣ, the theta construction used in the completed theta-intertwining theorem intertwines the target parameter T with the source parameter u⁻¹T. This file therefore base-changes the primitive polynomial for u⁻¹T to the completed maximal- unramified field, forms its genuine splitting field, and constructs the primitive analytic evaluation point there.

The repository's primitive polynomial indexed by n cuts out division level n + 1; this shift is kept explicit throughout.

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedLevel
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ChangedUniformizer

Imported by4

instance

equalCharacteristicChangedCompletedBaseAlgebra

L42 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseAlgebra

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 equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)

instance

equalCharacteristicChangedCompletedBaseCharP

L48 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseCharP

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

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

instance

equalCharacteristicChangedCompletedBaseValuationIsNontrivial

L58 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseValuationIsNontrivial

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

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

instance

equalCharacteristicChangedCompletedBaseValuationRankOne

L64 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseValuationRankOne

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k

Lean source · statement

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

instance

equalCharacteristicChangedCompletedBaseNormedField

L70 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseNormedField

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k

Lean source · statement

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

def

equalCharacteristicThetaSourceUnit

L78 ↗

LubinTate.EqualCharacteristic.equalCharacteristicThetaSourceUnit

Documentation

The source unit is u⁻¹; hence its parameter is u⁻¹T, in the orientation of the theta intertwining relation.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

def equalCharacteristicThetaSourceUnit
    {k : Type*} [Field k] (u : k⟦X⟧ˣ) : k⟦X⟧ˣ

def

equalCharacteristicChangedCompletedPrimitivePolynomial

L84 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial

Documentation

The primitive polynomial for source parameter u⁻¹T, after base change to (AlgebraicClosure κ)((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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

def equalCharacteristicChangedCompletedPrimitivePolynomial
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Polynomial (equalCharacteristicCompletedUnramifiedField F.residueField)

theorem

equalCharacteristicChangedCompletedPrimitivePolynomial_monic

L93 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial_monic

Documentation

The changed primitive polynomial remains monic after completion.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedPrimitivePolynomial F u n).Monic

theorem

equalCharacteristicChangedCompletedPrimitivePolynomial_natDegree

L100 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial_natDegree

Documentation

The completed changed 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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedPrimitivePolynomial F u n).natDegree =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

def

equalCharacteristicChangedCompletedLevelField

L110 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField

Documentation

The genuine splitting field of the source primitive polynomial.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

def equalCharacteristicChangedCompletedLevelField
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ)

instance

equalCharacteristicChangedCompletedLevelField_field

L115 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField_field

Documentation

The splitting field of the completed changed 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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

instance equalCharacteristicChangedCompletedLevelField_field
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Field (equalCharacteristicChangedCompletedLevelField F u n)

instance

equalCharacteristicChangedCompletedLevelField_algebra

L123 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField_algebra

Documentation

The changed 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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k

Lean source · statement

instance equalCharacteristicChangedCompletedLevelField_algebra
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)

instance

equalCharacteristicChangedCompletedLevelField_module

L133 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField_module

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section

Lean source · statement

instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid

instance

equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance

L147 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance

Documentation

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

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)

Lean source · statement

instance equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    FiniteDimensional
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)

instance

equalCharacteristicChangedCompletedLevelField_isAlgebraic

L157 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField_isAlgebraic

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)

Lean source · statement

instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)

instance

equalCharacteristicChangedCompletedLevelField_charP

L169 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField_charP

Documentation

The changed completed level field has the residue characteristic.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

instance equalCharacteristicChangedCompletedLevelField_charP
    (F : LocalField.{u, v} K) [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CharP (equalCharacteristicChangedCompletedLevelField F u n)
      F.residueCharacteristic

def

equalCharacteristicChangedCompletedLevelFieldEquivSplittingField

L181 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelFieldEquivSplittingField

Documentation

Comparison with the library splitting-field model.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

def
    equalCharacteristicChangedCompletedLevelFieldEquivSplittingField
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedLevelField F u n ≃ₐ[
      equalCharacteristicCompletedUnramifiedField F.residueField]
      (equalCharacteristicChangedCompletedPrimitivePolynomial F u n).SplittingField

def

equalCharacteristicChangedCompletedLevelFieldOfSplittingField

L191 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelFieldOfSplittingField

Documentation

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

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

def
    equalCharacteristicChangedCompletedLevelFieldOfSplittingField
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedPrimitivePolynomial F u n).SplittingField
      →ₐ[equalCharacteristicCompletedUnramifiedField F.residueField]
        equalCharacteristicChangedCompletedLevelField F u n

theorem

equalCharacteristicChangedCompletedPrimitivePolynomial_splits

L202 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial_splits

Documentation

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

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitivePolynomial_splits
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicChangedCompletedLevelField F u n))).Splits

theorem

equalCharacteristicChangedCompletedPrimitivePolynomial_adjoin_rootSet

L212 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial_adjoin_rootSet

Documentation

The roots of the changed primitive polynomial generate the named completed level field.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

theorem
    equalCharacteristicChangedCompletedPrimitivePolynomial_adjoin_rootSet
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).rootSet
          (equalCharacteristicChangedCompletedLevelField F u n) :
          Set (equalCharacteristicChangedCompletedLevelField F u n)) = ⊤

theorem

equalCharacteristicChangedCompletedLevelField_finiteDimensional

L224 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelField_finiteDimensional

Documentation

Supplies finite-dimensionality of the changed completed level field explicitly.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

theorem equalCharacteristicChangedCompletedLevelField_finiteDimensional
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    FiniteDimensional
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)

theorem

equalCharacteristicChangedCompletedPrimitivePolynomial_map_degree_ne_zero

L231 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial_map_degree_ne_zero

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitivePolynomial_map_degree_ne_zero
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicChangedCompletedLevelField F u n))).degree ≠ 0

def

equalCharacteristicChangedCompletedPrimitiveRoot

L250 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot

Documentation

A chosen primitive division-level n + 1 point for source parameter u⁻¹T.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

def equalCharacteristicChangedCompletedPrimitiveRoot
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedLevelField F u n

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_isRoot

L260 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_isRoot

Documentation

The distinguished completed primitive element is a root of the changed polynomial.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_isRoot
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicChangedCompletedLevelField F u n))).IsRoot
          (equalCharacteristicChangedCompletedPrimitiveRoot F u n)

def

equalCharacteristicChangedCompletedLevelNormedField

L273 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelNormedField

Documentation

The spectral norm on the changed completed level field.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

def equalCharacteristicChangedCompletedLevelNormedField
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n)

instance

equalCharacteristicChangedCompletedLevelNormedFieldInstance

L281 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelNormedFieldInstance

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)

Lean source · statement

instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n)

theorem

equalCharacteristicChangedCompletedLevelIsUltrametric

L288 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelIsUltrametric

Documentation

The spectral norm on the changed completed level field is ultrametric.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedLevelIsUltrametric
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n)

instance

equalCharacteristicChangedCompletedLevelIsUltrametricInstance

L299 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelIsUltrametricInstance

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n

Lean source · statement

instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n)

theorem

equalCharacteristicChangedCompletedLevelCompleteSpace

L305 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelCompleteSpace

Documentation

The changed completed level field is complete for its spectral norm.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedLevelCompleteSpace
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n)

instance

equalCharacteristicChangedCompletedLevelCompleteSpaceInstance

L312 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelCompleteSpaceInstance

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n

Lean source · statement

instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n)

def

equalCharacteristicChangedCompletedLevelValued

L319 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelValued

Documentation

Defines equalCharacteristicChangedCompletedLevelValued.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n

Lean source · statement

def equalCharacteristicChangedCompletedLevelValued
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0

instance

equalCharacteristicChangedCompletedLevelValuedInstance

L324 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelValuedInstance

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n

Lean source · statement

instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0

def

equalCharacteristicChangedCompletedBaseUniformizer

L330 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseUniformizer

Documentation

The source parameter u⁻¹T in the completed maximal-unramified base.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

def equalCharacteristicChangedCompletedBaseUniformizer
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) :
    equalCharacteristicCompletedUnramifiedField F.residueField

theorem

equalCharacteristicChangedCompletedBaseUniformizer_ne_zero

L339 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseUniformizer_ne_zero

Documentation

The changed base uniformizer remains nonzero after completion.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedBaseUniformizer_ne_zero
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedCompletedBaseUniformizer F u ≠ 0

theorem

equalCharacteristicChangedLaurentUniformizer_valuation_le_exp_neg_one

L348 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizer_valuation_le_exp_neg_one

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedLaurentUniformizer_valuation_le_exp_neg_one
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) :
    (Valued.v : Valuation F.residueField⸨X⸩ ℤᵐ⁰)
        (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u)) ≤
      WithZero.exp (-1 : ℤ)

theorem

equalCharacteristicChangedCompletedBaseUniformizer_norm_lt_one

L366 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedBaseUniformizer_norm_lt_one

Documentation

The completed source parameter u⁻¹T is topologically nilpotent.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedBaseUniformizer_norm_lt_one
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) :
    ‖equalCharacteristicChangedCompletedBaseUniformizer F u‖ < 1

def

equalCharacteristicChangedCompletedLevelUniformizer

L394 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelUniformizer

Documentation

The image of the source parameter in its completed splitting field.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

def equalCharacteristicChangedCompletedLevelUniformizer
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedLevelField F u n

theorem

equalCharacteristicChangedCompletedLevelUniformizer_ne_zero

L402 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelUniformizer_ne_zero

Documentation

The image of the changed uniformizer in the level field is nonzero.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedLevelUniformizer_ne_zero
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedLevelUniformizer F u n ≠ 0

theorem

equalCharacteristicChangedCompletedLevelUniformizer_norm

L411 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelUniformizer_norm

Documentation

The changed spectral norm extends the completed-base 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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedLevelUniformizer_norm
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ‖equalCharacteristicChangedCompletedLevelUniformizer F u n‖ =
      ‖equalCharacteristicChangedCompletedBaseUniformizer F u‖

theorem

equalCharacteristicChangedCompletedLevelUniformizer_norm_lt_one

L424 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelUniformizer_norm_lt_one

Documentation

The changed level uniformizer has norm strictly below one.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedLevelUniformizer_norm_lt_one
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ‖equalCharacteristicChangedCompletedLevelUniformizer F u n‖ < 1

theorem

equalCharacteristicChangedPiPolynomial_eval₂

L430 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomial_eval₂

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedPiPolynomial_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (x : A) :
    Polynomial.eval₂ φ x
        (equalCharacteristicChangedPiPolynomial F
          (equalCharacteristicThetaSourceUnit u)) =
      equalCharacteristicLubinTateAmbientPiEnd F
        (φ (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u))) x

theorem

equalCharacteristicChangedPiPolynomialIterate_eval₂

L445 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPiPolynomialIterate_eval₂

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedPiPolynomialIterate_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (equalCharacteristicChangedPiPolynomialIterate F
          (equalCharacteristicThetaSourceUnit u) n) =
      equalCharacteristicLubinTateAmbientPiIterate F
        (φ (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u))) n x

theorem

equalCharacteristicChangedPrimitivePolynomial_eval₂

L486 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedPrimitivePolynomial_eval₂

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedPrimitivePolynomial_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (equalCharacteristicChangedPrimitivePolynomial F
          (equalCharacteristicThetaSourceUnit u) n) =
      equalCharacteristicLubinTateAmbientPiIterate F
          (φ (equalCharacteristicChangedLaurentUniformizer F
            (equalCharacteristicThetaSourceUnit u))) n x ^
          (Nat.card F.residueField - 1) +
        φ (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u))

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_equation

L507 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_equation

Documentation

The chosen source point satisfies the primitive u⁻¹T equation.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_equation
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicChangedCompletedLevelUniformizer F u n) n
        (equalCharacteristicChangedCompletedPrimitiveRoot F u n) ^
          (Nat.card F.residueField - 1) +
      equalCharacteristicChangedCompletedLevelUniformizer F u n = 0

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_torsion

L539 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_torsion

Documentation

The root is killed at division level n + 1.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicChangedCompletedLevelUniformizer F u n) (n + 1)
      (equalCharacteristicChangedCompletedPrimitiveRoot F u n)

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_not_torsion_pred

L563 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_not_torsion_pred

Documentation

The chosen root is not already a division-level n point.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_not_torsion_pred
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ¬ IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicChangedCompletedLevelUniformizer F u n) n
      (equalCharacteristicChangedCompletedPrimitiveRoot F u n)

theorem

equalCharacteristicChangedCompletedAmbientPiEnd_norm_of_one_le

L579 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedAmbientPiEnd_norm_of_one_le

Documentation

If x is on or outside the unit sphere, the changed Lubin--Tate endomorphism has the norm of its leading term.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedAmbientPiEnd_norm_of_one_le
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x : equalCharacteristicChangedCompletedLevelField F u n)
    (hx : 1 ≤ ‖x‖) :
    ‖equalCharacteristicLubinTateAmbientPiEnd F
        (equalCharacteristicChangedCompletedLevelUniformizer F u n) x‖ =
      ‖x‖ ^ Nat.card F.residueField

theorem

equalCharacteristicChangedCompletedAmbientPiIterate_norm_of_one_le

L616 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedAmbientPiIterate_norm_of_one_le

Documentation

On or outside the unit sphere, every iterate has the norm of its leading q-power term.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedAmbientPiIterate_norm_of_one_le
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (level i : ℕ)
    (x : equalCharacteristicChangedCompletedLevelField F u level)
    (hx : 1 ≤ ‖x‖) :
    ‖equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicChangedCompletedLevelUniformizer F u level) i x‖ =
      ‖x‖ ^ (Nat.card F.residueField ^ i)

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_norm_lt_one

L643 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_norm_lt_one

Documentation

The primitive u⁻¹T-point lies strictly inside the spectral unit ball.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_norm_lt_one
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ‖equalCharacteristicChangedCompletedPrimitiveRoot F u n‖ < 1

def

equalCharacteristicChangedCompletedPrimitiveRootInteger

L679 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRootInteger

Documentation

The changed primitive root as an element of the spectral valuation ring.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

def equalCharacteristicChangedCompletedPrimitiveRootInteger
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued.integer (equalCharacteristicChangedCompletedLevelField F u n)

theorem

equalCharacteristicChangedCompletedPrimitiveRootInteger_coe

L691 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRootInteger_coe

Documentation

Coercing the integral primitive root returns the underlying completed root.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRootInteger_coe
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ((equalCharacteristicChangedCompletedPrimitiveRootInteger F u n :
      Valued.integer
        (equalCharacteristicChangedCompletedLevelField F u n)) :
          equalCharacteristicChangedCompletedLevelField F u n) =
      equalCharacteristicChangedCompletedPrimitiveRoot F u n

theorem

equalCharacteristicChangedCompletedPrimitiveRootInteger_mem_maximalIdeal

L703 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRootInteger_mem_maximalIdeal

Documentation

The integral primitive point lies in the maximal ideal.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRootInteger_mem_maximalIdeal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedPrimitiveRootInteger F u n ∈
      Valued.maximalIdeal
        (equalCharacteristicChangedCompletedLevelField F u n)

theorem

equalCharacteristicChangedCompletedPrimitiveRootInteger_hasEval

L724 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRootInteger_hasEval

Documentation

The maximal-ideal primitive point supports convergent power-series evaluation.

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]
noncomputable local instance equalCharacteristicChangedCompletedBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance equalCharacteristicChangedCompletedBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
noncomputable local instance equalCharacteristicChangedCompletedBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
section
local instance equalCharacteristicChangedCompletedLevelField_module
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    @Module (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)
      (inferInstance : DivisionRing
        (equalCharacteristicCompletedUnramifiedField F.residueField)).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicChangedCompletedLevelField F u n)).toAddCommMonoid :=
  @Algebra.toModule
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
local instance equalCharacteristicChangedCompletedLevelField_isAlgebraic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.IsAlgebraic
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  @Algebra.IsAlgebraic.of_finite
    (equalCharacteristicCompletedUnramifiedField F.residueField)
    (equalCharacteristicChangedCompletedLevelField F u n) _ _ _
    (equalCharacteristicChangedCompletedLevelField_algebra F u n)
    (equalCharacteristicChangedCompletedLevelField_finiteDimensionalInstance F u n)
noncomputable local instance equalCharacteristicChangedCompletedLevelNormedFieldInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    NontriviallyNormedField
      (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelNormedField F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelIsUltrametricInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelIsUltrametric F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelCompleteSpaceInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    CompleteSpace (equalCharacteristicChangedCompletedLevelField F u n) :=
  equalCharacteristicChangedCompletedLevelCompleteSpace F u n
noncomputable local instance equalCharacteristicChangedCompletedLevelValuedInstance
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Valued (equalCharacteristicChangedCompletedLevelField F u n) ℝ≥0 :=
  equalCharacteristicChangedCompletedLevelValued F u n

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRootInteger_hasEval
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    PowerSeries.HasEval
      (equalCharacteristicChangedCompletedPrimitiveRootInteger F u n)

Module documentation

The completed theta-intertwining theorem: the completed changed-uniformizer level

Declarations