Module

ThetaEvaluation.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Theta.ThetaEvaluation

7 declarations indexed from sourceView source ↗

Module documentation

Analytic evaluation for theta

The theta series of the completed theta-intertwining theorem has coefficients in (AlgebraicClosure k)[[T]]. This file evaluates it at a topologically nilpotent element of the valued integer ring of the completed unramified Laurent field. The value is accompanied by its convergent coefficient sum, and the formal intertwining identity is transported through this genuine analytic evaluation map.

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.CompletedUnramifiedField
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Theta.ThetaSeries

Imported by4

instance

equalCharacteristicThetaEvaluationCoefficientUniformSpace

L37 ↗

LubinTate.EqualCharacteristic.equalCharacteristicThetaEvaluationCoefficientUniformSpace

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries PowerSeries.WithPiTopology Topology Valued WithZero
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
omit [Finite k] in

Lean source · statement

instance equalCharacteristicThetaEvaluationCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k)

instance

equalCharacteristicThetaEvaluationLinearTopology

L40 ↗

LubinTate.EqualCharacteristic.equalCharacteristicThetaEvaluationLinearTopology

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries PowerSeries.WithPiTopology Topology Valued WithZero
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance equalCharacteristicThetaEvaluationCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicThetaEvaluationLinearTopology :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))

instance

equalCharacteristicThetaEvaluationCompleteSpace

L46 ↗

LubinTate.EqualCharacteristic.equalCharacteristicThetaEvaluationCompleteSpace

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries PowerSeries.WithPiTopology Topology Valued WithZero
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance equalCharacteristicThetaEvaluationCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
noncomputable local instance equalCharacteristicThetaEvaluationLinearTopology :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerLinearTopology

Lean source · statement

instance equalCharacteristicThetaEvaluationCompleteSpace :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))

instance

equalCharacteristicThetaEvaluationUniformAddGroup

L51 ↗

LubinTate.EqualCharacteristic.equalCharacteristicThetaEvaluationUniformAddGroup

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries PowerSeries.WithPiTopology Topology Valued WithZero
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance equalCharacteristicThetaEvaluationCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
noncomputable local instance equalCharacteristicThetaEvaluationLinearTopology :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaEvaluationCompleteSpace :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerCompleteSpace

Lean source · statement

instance equalCharacteristicThetaEvaluationUniformAddGroup :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))

def

equalCharacteristicCompletedThetaValue

L58 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedThetaValue

Documentation

The analytic value of the theta series at a topologically nilpotent element of the completed-unramified integer ring.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries PowerSeries.WithPiTopology Topology Valued WithZero
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance equalCharacteristicThetaEvaluationCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
noncomputable local instance equalCharacteristicThetaEvaluationLinearTopology :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaEvaluationCompleteSpace :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaEvaluationUniformAddGroup :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerIsUniformAddGroup

Lean source · statement

def equalCharacteristicCompletedThetaValue
    (u : k⟦X⟧ˣ)
    (a : Valued.integer (equalCharacteristicCompletedUnramifiedField k))
    (ha : PowerSeries.HasEval a) :
    Valued.integer (equalCharacteristicCompletedUnramifiedField k)

theorem

equalCharacteristicCompletedThetaValue_hasSum

L69 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedThetaValue_hasSum

Documentation

The defining coefficient series for the analytic theta value converges. This records every natural degree, including the zero coefficients away from the additive exponents q^j.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries PowerSeries.WithPiTopology Topology Valued WithZero
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance equalCharacteristicThetaEvaluationCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
noncomputable local instance equalCharacteristicThetaEvaluationLinearTopology :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaEvaluationCompleteSpace :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaEvaluationUniformAddGroup :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerIsUniformAddGroup

Lean source · full declaration

theorem equalCharacteristicCompletedThetaValue_hasSum
    (u : k⟦X⟧ˣ)
    (a : Valued.integer (equalCharacteristicCompletedUnramifiedField k))
    (ha : PowerSeries.HasEval a) :
    HasSum
      (fun n : ℕ ↦
        equalCharacteristicPowerSeriesToCompletedInteger k
            (PowerSeries.coeff n (equalCharacteristicThetaSeries u)) *
          a ^ n)
      (equalCharacteristicCompletedThetaValue k u a ha) := by
  rw [equalCharacteristicCompletedThetaValue,
    equalCharacteristicCompletedIntegerEvaluation,
    PowerSeries.coe_eval₂Hom]
  exact PowerSeries.hasSum_eval₂
    (equalCharacteristicPowerSeriesToCompletedInteger_continuous k)
    ha (equalCharacteristicThetaSeries u)

theorem

equalCharacteristicThetaSeries_intertwines_evaluated

L89 ↗

LubinTate.EqualCharacteristic.equalCharacteristicThetaSeries_intertwines_evaluated

Documentation

Analytic evaluation of the theta intertwining identity. The right-hand formal composition is evaluated explicitly as theta(a)^q + T * theta(a) in the completed-unramified integer ring.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries PowerSeries.WithPiTopology Topology Valued WithZero
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance equalCharacteristicThetaEvaluationCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
noncomputable local instance equalCharacteristicThetaEvaluationLinearTopology :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k))
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaEvaluationCompleteSpace :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaEvaluationUniformAddGroup :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedUnramifiedField k)) :=
  valuedIntegerIsUniformAddGroup

Lean source · statement

theorem equalCharacteristicThetaSeries_intertwines_evaluated
    (u : k⟦X⟧ˣ)
    (a : Valued.integer (equalCharacteristicCompletedUnramifiedField k))
    (ha : PowerSeries.HasEval a) :
    equalCharacteristicCompletedIntegerEvaluation k a ha
        (PowerSeries.subst
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (equalCharacteristicCompletedSourceUniformizer u))
          (equalCharacteristicThetaSeriesFrobenius u)) =
      equalCharacteristicCompletedThetaValue k u a ha ^ Nat.card k +
        equalCharacteristicCompletedIntegerUniformizer k *
          equalCharacteristicCompletedThetaValue k u a ha

Module documentation

Analytic evaluation for theta

Declarations

equalCharacteristicThetaEvaluationCoefficientUniformSpace

equalCharacteristicThetaEvaluationLinearTopology

equalCharacteristicThetaEvaluationCompleteSpace

equalCharacteristicThetaEvaluationUniformAddGroup

equalCharacteristicCompletedThetaValue

equalCharacteristicCompletedThetaValue_hasSum

equalCharacteristicThetaSeries_intertwines_evaluated