Module

DirectThetaAtCompletedLevel.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.DirectThetaAtCompletedLevel

46 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: direct theta at the standard completed level

The standard completed primitive point lambda is a division-level n + 1 point for the source parameter T. This file genuinely evaluates the direct theta series at lambda, iterates

theta^φ ∘ e_T = e_(uT) ∘ theta,

and proves that theta(lambda) is primitive target uT-torsion at the same division level.

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.DirectThetaIteration
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ThetaLocalInverse

Imported by5

instance

equalCharacteristicDirectThetaCompletedBaseCharP

L42 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCompletedBaseCharP

Source context 8 commands

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

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

Lean source · statement

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

instance

equalCharacteristicDirectThetaCompletedLevelCharP

L52 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCompletedLevelCharP

Source context 8 commands

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

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

Lean source · statement

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

instance

equalCharacteristicDirectThetaBaseValuationIsNontrivial

L62 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaBaseValuationIsNontrivial

Source context 8 commands

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

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

Lean source · statement

instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial

instance

equalCharacteristicDirectThetaBaseValuationRankOne

L69 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaBaseValuationRankOne

Source context 9 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField

Lean source · statement

instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne

instance

equalCharacteristicDirectThetaBaseNormedField

L75 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaBaseNormedField

Source context 10 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField

Lean source · statement

instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField)

instance

equalCharacteristicDirectThetaLevelNormedField

L81 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaLevelNormedField

Source context 11 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField

Lean source · statement

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

instance

equalCharacteristicDirectThetaLevelIsUltrametric

L86 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaLevelIsUltrametric

Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n

Lean source · statement

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

instance

equalCharacteristicDirectThetaLevelCompleteSpace

L91 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaLevelCompleteSpace

Source context 13 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n

Lean source · statement

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

instance

equalCharacteristicDirectThetaLevelValued

L96 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaLevelValued

Source context 14 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n

Lean source · statement

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

instance

equalCharacteristicDirectThetaIntegerLinearTopology

L101 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaIntegerLinearTopology

Source context 15 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n

Lean source · statement

instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n))

instance

equalCharacteristicDirectThetaIntegerCompleteSpace

L108 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaIntegerCompleteSpace

Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology

Lean source · statement

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

instance

equalCharacteristicDirectThetaIntegerUniformAddGroup

L114 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaIntegerUniformAddGroup

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace

Lean source · statement

instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n))

instance

equalCharacteristicDirectThetaCoefficientUniformSpace

L120 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCoefficientUniformSpace

Source context 18 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup

Lean source · statement

instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧)

theorem

equalCharacteristicDirectThetaCoefficientHom_continuous

L125 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCoefficientHom_continuous

Source context 19 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥

Lean source · statement

theorem equalCharacteristicDirectThetaCoefficientHom_continuous
    (F : LocalField.{u, v} K) (n : ℕ) :
    Continuous (equalCharacteristicCompletedLevelCoefficientHom F n)

instance

equalCharacteristicDirectThetaCoefficientAlgebra

L130 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCoefficientAlgebra

Source context 19 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥

Lean source · statement

instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n))

theorem

equalCharacteristicDirectThetaSourceUniformizerInteger_coe

L139 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceUniformizerInteger_coe

Documentation

The formal source T maps to the actual standard completed-level uniformizer.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaSourceUniformizerInteger_coe
    (F : LocalField.{u, v} K) (n : ℕ) :
    ((equalCharacteristicCompletedLevelUniformizerInteger F n :
      Valued.integer (equalCharacteristicCompletedLevelField F n)) :
        equalCharacteristicCompletedLevelField F n) =
      equalCharacteristicCompletedLevelUniformizer F n

def

equalCharacteristicDirectThetaTargetUniformizerInteger

L158 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaTargetUniformizerInteger

Documentation

The direct target parameter uT in the standard completed-level valuation ring.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

def

equalCharacteristicDirectThetaTargetUniformizer

L165 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaTargetUniformizer

Documentation

The same genuine target parameter in the ambient completed level field.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectThetaTargetUniformizerInteger_coe

L173 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaTargetUniformizerInteger_coe

Documentation

Coercing the integral theta target uniformizer returns its field value.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaTargetUniformizerInteger_coe
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ((equalCharacteristicDirectThetaTargetUniformizerInteger F u n :
      Valued.integer (equalCharacteristicCompletedLevelField F n)) :
        equalCharacteristicCompletedLevelField F n) =
      equalCharacteristicDirectThetaTargetUniformizer F u n

def

equalCharacteristicDirectThetaSourceIterate

L182 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceIterate

Documentation

The standard source orbit of the chosen primitive point.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectTheta_sourceIterate_norm_lt_one_aux

L190 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectTheta_sourceIterate_norm_lt_one_aux

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectTheta_sourceIterate_norm_lt_one_aux
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] (n i : ℕ)
    (x : equalCharacteristicCompletedLevelField F n) (hx : ‖x‖ < 1) :
    ‖equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicCompletedLevelUniformizer F n) i x‖ < 1

theorem

equalCharacteristicDirectThetaSourceIterate_norm_lt_one

L213 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceIterate_norm_lt_one

Documentation

Every direct theta source iterate has norm strictly below one.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

def

equalCharacteristicDirectThetaSourceIterateInteger

L222 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceIterateInteger

Documentation

Each source iterate as a point of the spectral valuation ring.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectThetaSourceIterateInteger_coe

L233 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceIterateInteger_coe

Documentation

Coercing an integral source iterate returns the underlying field element.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaSourceIterateInteger_coe
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] (n i : ℕ) :
    ((equalCharacteristicDirectThetaSourceIterateInteger F n i :
      Valued.integer (equalCharacteristicCompletedLevelField F n)) :
        equalCharacteristicCompletedLevelField F n) =
      equalCharacteristicDirectThetaSourceIterate F n i

theorem

equalCharacteristicDirectThetaSourceIterateInteger_norm_lt_one

L243 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceIterateInteger_norm_lt_one

Documentation

Each integral source iterate has norm strictly below one.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectThetaSourceIterateInteger_hasEval

L251 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceIterateInteger_hasEval

Documentation

Power series can be evaluated at every integral direct source iterate.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectTheta_sourceLubinTate_evaluation

L263 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectTheta_sourceLubinTate_evaluation

Documentation

Evaluating e_T moves one step along the actual source orbit.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectTheta_sourceLubinTate_evaluation
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] (n i : ℕ) :
    equalCharacteristicCompletedLevelEvaluation F n
        (equalCharacteristicDirectThetaSourceIterateInteger F n i)
        (equalCharacteristicDirectThetaSourceIterateInteger_hasEval F n i)
        (equalCharacteristicCompletedLubinTateSeries
          (PowerSeries.X : (AlgebraicClosure F.residueField)⟦X⟧)) =
      equalCharacteristicDirectThetaSourceIterateInteger F n (i + 1)

theorem

equalCharacteristicDirectThetaEvaluation_hasEval_of_hasSubst

L300 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaEvaluation_hasEval_of_hasSubst

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaEvaluation_hasEval_of_hasSubst
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : Valued.integer (equalCharacteristicCompletedLevelField F n))
    (hx : PowerSeries.HasEval x)
    (a : ((AlgebraicClosure F.residueField)⟦X⟧)⟦X⟧)
    (ha : PowerSeries.HasSubst a) :
    PowerSeries.HasEval
      (equalCharacteristicCompletedLevelEvaluation F n x hx a)

theorem

equalCharacteristicDirectThetaEvaluation_subst

L316 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaEvaluation_subst

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaEvaluation_subst
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : Valued.integer (equalCharacteristicCompletedLevelField F n))
    (hx : PowerSeries.HasEval x)
    (a f : ((AlgebraicClosure F.residueField)⟦X⟧)⟦X⟧)
    (ha : PowerSeries.HasSubst a)
    (haEval : PowerSeries.HasEval
      (equalCharacteristicCompletedLevelEvaluation F n x hx a)) :
    equalCharacteristicCompletedLevelEvaluation F n x hx
        (PowerSeries.subst a f) =
      equalCharacteristicCompletedLevelEvaluation F n
        (equalCharacteristicCompletedLevelEvaluation F n x hx a) haEval f

def

equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate

L344 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate

Documentation

The analytic value of the i-th direct Frobenius twist at the i-th standard source iterate.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_hasSum

L356 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_hasSum

Documentation

The evaluated Frobenius theta iterate is summable at the matching source iterate.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · full declaration

theorem
    equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_hasSum
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n i : ℕ) :
    HasSum
      (fun m : ℕ ↦
        equalCharacteristicCompletedLevelCoefficientHom F n
            (PowerSeries.coeff m
              (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)) *
          equalCharacteristicDirectThetaSourceIterateInteger F n i ^ m)
      (equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate
        F u n i) := by
  rw [equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate,
    equalCharacteristicCompletedLevelEvaluation, PowerSeries.coe_eval₂Hom]
  exact PowerSeries.hasSum_eval₂
    (equalCharacteristicDirectThetaCoefficientHom_continuous F n)
    (equalCharacteristicDirectThetaSourceIterateInteger_hasEval F n i)
    (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)

theorem

equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_hasEval

L377 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_hasEval

Documentation

The Frobenius theta iterate admits evaluation at the matching source iterate.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectThetaSeriesFrobeniusIterate_coeff_one_isUnit

L392 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobeniusIterate_coeff_one_isUnit

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem
    equalCharacteristicDirectThetaSeriesFrobeniusIterate_coeff_one_isUnit
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) (i : ℕ) :
    IsUnit (PowerSeries.coeff 1
      (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i))

theorem

equalCharacteristicDirectThetaFrobeniusIterateCoefficientOne_isUnit

L417 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateCoefficientOne_isUnit

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem
    equalCharacteristicDirectThetaFrobeniusIterateCoefficientOne_isUnit
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ)
    (n i : ℕ) :
    IsUnit
      (equalCharacteristicCompletedLevelCoefficientHom F n
        (PowerSeries.coeff 1
          (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)))

theorem

equalCharacteristicDirectThetaFrobeniusIterateAtZero_hasSum

L428 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateAtZero_hasSum

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · full declaration

theorem
    equalCharacteristicDirectThetaFrobeniusIterateAtZero_hasSum
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ)
    (n i : ℕ) :
    HasSum
      (fun m : ℕ ↦
        equalCharacteristicCompletedLevelCoefficientHom F n
            (PowerSeries.coeff m
              (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)) *
          (0 : Valued.integer
            (equalCharacteristicCompletedLevelField F n)) ^ m)
      0 := by
  have hterms :
      (fun m : ℕ ↦
        equalCharacteristicCompletedLevelCoefficientHom F n
            (PowerSeries.coeff m
              (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)) *
          (0 : Valued.integer
            (equalCharacteristicCompletedLevelField F n)) ^ m) =
        fun _ ↦ 0 := by
    funext m
    cases m with
    | zero =>
        simp [PowerSeries.coeff_zero_eq_constantCoeff_apply,
          equalCharacteristicDirectThetaSeriesFrobeniusIterate_constantCoeff]
    | succ m => simp
  rw [hterms]
  exact hasSum_zero

theorem

equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_norm

L457 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_norm

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem
    equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_norm
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n i : ℕ) :
    ‖equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate F u n i‖ =
      ‖equalCharacteristicDirectThetaSourceIterateInteger F n i‖

theorem

equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_succ

L481 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_succ

Documentation

Analytic form of the i-th direct second identity.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_succ
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n i : ℕ) :
    equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate
        F u n (i + 1) =
      equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate F u n i ^
          Nat.card F.residueField +
        equalCharacteristicDirectThetaTargetUniformizerInteger F u n *
          equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate
            F u n i

def

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot

L549 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot

Documentation

Genuine analytic evaluation of the direct theta series at the standard completed primitive root lambda.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

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

theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_hasSum

L560 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_hasSum

Documentation

The coefficient expansion defining the direct theta value converges.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · full declaration

theorem equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_hasSum
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    HasSum
      (fun m : ℕ ↦
        equalCharacteristicCompletedLevelCoefficientHom F n
            (PowerSeries.coeff m (equalCharacteristicDirectThetaSeries u)) *
          equalCharacteristicCompletedPrimitiveRootInteger F n ^ m)
      (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F u n) := by
  rw [equalCharacteristicDirectThetaAtCompletedPrimitiveRoot,
    equalCharacteristicCompletedLevelEvaluation, PowerSeries.coe_eval₂Hom]
  exact PowerSeries.hasSum_eval₂
    (equalCharacteristicDirectThetaCoefficientHom_continuous F n)
    (equalCharacteristicCompletedPrimitiveRootInteger_hasEval F n)
    (equalCharacteristicDirectThetaSeries u)

theorem

equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_zero

L577 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_zero

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem
    equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate F u n 0 =
      equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F u n

theorem

equalCharacteristicDirectThetaSourceRoot_torsion

L603 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceRoot_torsion

Documentation

The standard primitive root is killed by the source parameter T at division level n + 1.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaSourceRoot_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicCompletedLevelUniformizer F n) (n + 1)
      (equalCharacteristicCompletedPrimitiveRoot F n)

theorem

equalCharacteristicDirectThetaSourceRoot_not_torsion_pred

L626 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSourceRoot_not_torsion_pred

Documentation

The standard primitive root is not killed at source division level n.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaSourceRoot_not_torsion_pred
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    ¬ IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicCompletedLevelUniformizer F n) n
      (equalCharacteristicCompletedPrimitiveRoot F n)

theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_targetIterate

L650 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_targetIterate

Documentation

Iterating the evaluated second identity identifies the target uT orbit of theta(lambda) with the successive twisted source evaluations.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_targetIterate
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n i : ℕ) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicDirectThetaTargetUniformizer F u n) i
        (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F u n :
          equalCharacteristicCompletedLevelField F n) =
      (equalCharacteristicDirectThetaFrobeniusIterateAtSourceIterate
        F u n i : equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_torsion

L694 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_torsion

Documentation

The direct theta value is killed by target uT at division level n + 1.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicDirectThetaTargetUniformizer F u n) (n + 1)
      (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F u n :
        equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_not_torsion_pred

L718 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_not_torsion_pred

Documentation

The target value is not killed at division level n.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_not_torsion_pred
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ¬ IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicDirectThetaTargetUniformizer F u n) n
      (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F u n :
        equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isPrimitive

L749 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isPrimitive

Documentation

Hence theta(lambda) is a primitive target uT-division point at division level n + 1.

Source context 20 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance
    equalCharacteristicDirectThetaBaseValuationIsNontrivial
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseValuationRankOne
    (F : LocalField.{u, v} K) :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField F.residueField) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne F.residueField
noncomputable local instance equalCharacteristicDirectThetaBaseNormedField
    (F : LocalField.{u, v} K) :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedBaseNormedField F.residueField
noncomputable local instance equalCharacteristicDirectThetaLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicDirectThetaLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicDirectThetaLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicDirectThetaLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicDirectThetaIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicDirectThetaIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicDirectThetaIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance
    equalCharacteristicDirectThetaCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
private noncomputable local instance equalCharacteristicDirectThetaCoefficientAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra ((AlgebraicClosure F.residueField)⟦X⟧)
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  (equalCharacteristicCompletedLevelCoefficientHom F n).toAlgebra

Lean source · statement

theorem equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isPrimitive
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsEqualCharacteristicLubinTateAmbientTorsion F
        (equalCharacteristicDirectThetaTargetUniformizer F u n) (n + 1)
        (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F u n :
          equalCharacteristicCompletedLevelField F n) ∧
      ¬ IsEqualCharacteristicLubinTateAmbientTorsion F
        (equalCharacteristicDirectThetaTargetUniformizer F u n) n
        (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F u n :
          equalCharacteristicCompletedLevelField F n)

Module documentation

The completed theta-intertwining theorem: direct theta at the standard completed level

Declarations