NYLL
Module

DirectThetaSeries.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.DirectThetaSeries
18 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: the direct-orientation theta series

This file constructs the theta series in the orientation used directly in the completed theta-intertwining theorem: the source prime is pi = T and the target prime is bar_pi = uT. Thus the second identity is

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

This coefficient recursion is mathematically distinct from the constructed specialization u⁻¹T → T. The first theta identity and analytic evaluation at division points are developed in the corresponding companion modules.

Imports2
Imported by5

Declarations

def

equalCharacteristicDirectCompletedTargetUniformizer

L41 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectCompletedTargetUniformizer
Documentation

The target prime bar_pi = uT in the completed maximal-unramified coefficient ring.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
def equalCharacteristicDirectCompletedTargetUniformizer
    (u : k⟦X⟧ˣ) : (AlgebraicClosure k)⟦X⟧
def

equalCharacteristicDirectThetaGamma

L48 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaGamma
Documentation

The direct-orientation contracting coefficient gamma_j = u⁻¹ T^(q^j-1).

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
def equalCharacteristicDirectThetaGamma
    (u : k⟦X⟧ˣ) (j : ℕ) : (AlgebraicClosure k)⟦X⟧
theorem

equalCharacteristicDirectThetaGamma_constantCoeff

L55 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaGamma_constantCoeff
Documentation

Positive-index direct theta gamma terms have zero constant coefficient.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectThetaGamma_constantCoeff
    (u : k⟦X⟧ˣ) (j : ℕ) (hj : 0 < j) :
    PowerSeries.coeff 0 (equalCharacteristicDirectThetaGamma u j) = 0
theorem

equalCharacteristicDirectTargetUniformizer_mul_gamma

L65 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectTargetUniformizer_mul_gamma
Documentation

Clearing the direct gamma by the target prime uT gives T^(q^j).

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectTargetUniformizer_mul_gamma
    (u : k⟦X⟧ˣ) (j : ℕ) (hj : 0 < j) :
    equalCharacteristicDirectCompletedTargetUniformizer u *
        equalCharacteristicDirectThetaGamma u j =
      PowerSeries.X ^ (Nat.card k ^ j)
def

equalCharacteristicDirectThetaBeta

L97 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaBeta
Documentation

The direct right-hand side beta(b) = u⁻¹ (phi(b)-b^q)/T of the contracting recursion.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
def equalCharacteristicDirectThetaBeta
    (u : k⟦X⟧ˣ) (b : (AlgebraicClosure k)⟦X⟧) :
    (AlgebraicClosure k)⟦X⟧
theorem

equalCharacteristicDirectTargetUniformizer_mul_beta

L107 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectTargetUniformizer_mul_beta
Documentation

Clearing the direct beta by uT recovers its numerator phi(b)-b^q.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectTargetUniformizer_mul_beta
    (u : k⟦X⟧ˣ) (b : (AlgebraicClosure k)⟦X⟧) :
    equalCharacteristicDirectCompletedTargetUniformizer u *
        equalCharacteristicDirectThetaBeta u b =
      equalCharacteristicPowerSeriesFrobenius k b - b ^ Nat.card k
def

equalCharacteristicDirectThetaCoefficient

L142 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCoefficient
Documentation

Coefficients of the direct-orientation additive theta series. Its linear coefficient solves phi(b₀)=u b₀; the later coefficients are the actual recursively constructed solutions of the contracting equations.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · full declaration
def equalCharacteristicDirectThetaCoefficient
    (u : k⟦X⟧ˣ) : ℕ → (AlgebraicClosure k)⟦X⟧
  | 0 => equalCharacteristicSemilinearUnit (u : k⟦X⟧)
      (by
        intro hzero
        have hunit := PowerSeries.isUnit_constantCoeff (u : k⟦X⟧) u.isUnit
        apply hunit.ne_zero
        simpa [PowerSeries.coeff_zero_eq_constantCoeff_apply] using hzero)
  | j + 1 =>
      contractingFrobeniusEquationSolution
        (equalCharacteristicCoefficientFrobenius k).toRingHom
        (equalCharacteristicDirectThetaGamma u (j + 1))
        (equalCharacteristicDirectThetaBeta u
          (equalCharacteristicDirectThetaCoefficient u j))
theorem

equalCharacteristicDirectThetaCoefficient_zero

L159 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCoefficient_zero
Documentation

The zeroth direct theta coefficient is the semilinear source unit.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · full declaration
theorem equalCharacteristicDirectThetaCoefficient_zero
    (u : k⟦X⟧ˣ) :
    equalCharacteristicDirectThetaCoefficient u 0 =
      equalCharacteristicSemilinearUnit (u : k⟦X⟧)
        (by
          intro hzero
          have hunit := PowerSeries.isUnit_constantCoeff (u : k⟦X⟧) u.isUnit
          apply hunit.ne_zero
          simpa [PowerSeries.coeff_zero_eq_constantCoeff_apply] using hzero) :=
  rfl
theorem

equalCharacteristicDirectThetaCoefficient_succ_equation

L172 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCoefficient_succ_equation
Documentation

The direct contracting recursion b_(j+1) - gamma_(j+1) phi(b_(j+1)) = beta(b_j).

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectThetaCoefficient_succ_equation
    (u : k⟦X⟧ˣ) (j : ℕ) :
    equalCharacteristicDirectThetaCoefficient u (j + 1) -
        equalCharacteristicDirectThetaGamma u (j + 1) *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicDirectThetaCoefficient u (j + 1)) =
      equalCharacteristicDirectThetaBeta u
        (equalCharacteristicDirectThetaCoefficient u j)
theorem

equalCharacteristicDirectThetaCoefficient_succ_comparison

L192 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaCoefficient_succ_comparison
Documentation

The coefficient comparison obtained after clearing uT.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectThetaCoefficient_succ_comparison
    (u : k⟦X⟧ˣ) (j : ℕ) :
    equalCharacteristicDirectCompletedTargetUniformizer u *
          equalCharacteristicDirectThetaCoefficient u (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicDirectThetaCoefficient u (j + 1)) =
      equalCharacteristicPowerSeriesFrobenius k
          (equalCharacteristicDirectThetaCoefficient u j) -
        equalCharacteristicDirectThetaCoefficient u j ^ Nat.card k
def

equalCharacteristicDirectThetaSeries

L221 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries
Documentation

The genuine sparse outer theta series for the direct orientation T → uT.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
def equalCharacteristicDirectThetaSeries
    (u : k⟦X⟧ˣ) : ((AlgebraicClosure k)⟦X⟧)⟦X⟧
theorem

equalCharacteristicDirectThetaSeries_coeff_pow

L228 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries_coeff_pow
Documentation

The direct theta coefficient at q ^ j is its jth recursive coefficient.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectThetaSeries_coeff_pow
    (u : k⟦X⟧ˣ) (j : ℕ) :
    PowerSeries.coeff (Nat.card k ^ j)
        (equalCharacteristicDirectThetaSeries u) =
      equalCharacteristicDirectThetaCoefficient u j
theorem

equalCharacteristicDirectThetaSeries_constantCoeff

L238 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries_constantCoeff
Documentation

The direct theta series has zero constant coefficient.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectThetaSeries_constantCoeff
    (u : k⟦X⟧ˣ) :
    PowerSeries.constantCoeff (equalCharacteristicDirectThetaSeries u) = 0
theorem

equalCharacteristicDirectThetaSeries_hasSubst

L244 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries_hasSubst
Documentation

The direct theta series is valid as a substitution series.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectThetaSeries_hasSubst
    (u : k⟦X⟧ˣ) :
    PowerSeries.HasSubst (equalCharacteristicDirectThetaSeries u)
def

equalCharacteristicDirectThetaSeriesFrobenius

L251 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobenius
Documentation

Arithmetic Frobenius on every coefficient of the direct theta series.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
def equalCharacteristicDirectThetaSeriesFrobenius
    (u : k⟦X⟧ˣ) : ((AlgebraicClosure k)⟦X⟧)⟦X⟧
theorem

equalCharacteristicDirectThetaSeriesFrobenius_eq_qAdditiveSeries

L257 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobenius_eq_qAdditiveSeries
Documentation

Frobenius of direct theta is the q-additive series of Frobenius coefficients.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · full declaration
theorem equalCharacteristicDirectThetaSeriesFrobenius_eq_qAdditiveSeries
    (u : k⟦X⟧ˣ) :
    equalCharacteristicDirectThetaSeriesFrobenius u =
      equalCharacteristicQAdditiveSeries k
        (fun j ↦ equalCharacteristicPowerSeriesFrobenius k
          (equalCharacteristicDirectThetaCoefficient u j)) := by
  exact equalCharacteristicQAdditiveSeries_map k
    (equalCharacteristicPowerSeriesFrobenius k)
    (equalCharacteristicDirectThetaCoefficient u)
theorem

equalCharacteristicDirectThetaSeries_intertwines

L269 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries_intertwines
Documentation

Direct the completed theta-intertwining theorem second identity: theta^φ ∘ e_T = e_(uT) ∘ theta.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · statement
theorem equalCharacteristicDirectThetaSeries_intertwines
    (u : k⟦X⟧ˣ) :
    PowerSeries.subst
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
        (equalCharacteristicDirectThetaSeriesFrobenius u) =
      PowerSeries.subst (equalCharacteristicDirectThetaSeries u)
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (equalCharacteristicDirectCompletedTargetUniformizer u))
theorem

equalCharacteristicDirectThetaSeries_coeff_one

L300 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries_coeff_one
Documentation

The direct theta series has the semilinear leading unit as its linear coefficient.

Source context 6 commands

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

noncomputable section
open scoped PowerSeries
universe u
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} [Field k] [Finite k]
Lean source · full declaration
theorem equalCharacteristicDirectThetaSeries_coeff_one
    (u : k⟦X⟧ˣ) :
    PowerSeries.coeff 1 (equalCharacteristicDirectThetaSeries u) =
      equalCharacteristicSemilinearUnit (u : k⟦X⟧)
        (by
          intro hzero
          have hunit := PowerSeries.isUnit_constantCoeff (u : k⟦X⟧) u.isUnit
          apply hunit.ne_zero
          simpa [PowerSeries.coeff_zero_eq_constantCoeff_apply] using hzero) := by
  calc
    PowerSeries.coeff 1 (equalCharacteristicDirectThetaSeries u) =
        equalCharacteristicDirectThetaCoefficient u 0 := by
      simpa only [pow_zero] using
        equalCharacteristicDirectThetaSeries_coeff_pow u 0
    _ = _ := equalCharacteristicDirectThetaCoefficient_zero u

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