NYLL
Module

ThetaCoefficients.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Theta.ThetaCoefficients
24 declarations indexed from sourceView source ↗

Module documentation

LubinTate the equal-characteristic theta construction: equal-characteristic theta coefficients

This file constructs the coefficient sources behind the power series theta in the equal-characteristic specialization of the equal-characteristic theta construction. For a finite field k, the completed maximal unramified coefficient ring of k((T)) is modeled by (AlgebraicClosure k)[[T]], with arithmetic Frobenius acting coefficientwise.

The first construction solves the exact semilinear equation

phi(epsilon) = u * epsilon

for every unit u in k[[T]]. This is the linear coefficient equation forced by theta^phi o e_bar = e o theta when pi = u * bar_pi.

Imports7
Imported by4

Declarations

theorem

exists_frobenius_eq_mul_add

L46 ↗
LubinTate.EqualCharacteristic.exists_frobenius_eq_mul_add
Source context 6 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
Lean source · statement
theorem exists_frobenius_eq_mul_add
    (a c : AlgebraicClosure k) :
    ∃ x : AlgebraicClosure k,
      x ^ Nat.card k = a * x + c
def

chosenEqualCharacteristicSemilinearLeadingCoefficient

L94 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicSemilinearLeadingCoefficient
Documentation

The constant coefficient chosen for a solution of phi(epsilon)=u*epsilon.

Source context 7 commands

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

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

chosenEqualCharacteristicSemilinearLeadingCoefficient_pow

L103 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicSemilinearLeadingCoefficient_pow
Documentation

The chosen leading coefficient is a (q - 1)st root of the source constant term.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
theorem chosenEqualCharacteristicSemilinearLeadingCoefficient_pow
    (u : k⟦X⟧) :
    chosenEqualCharacteristicSemilinearLeadingCoefficient u ^
        (Nat.card k - 1) =
      algebraMap k (AlgebraicClosure k) (PowerSeries.coeff 0 u)
theorem

chosenEqualCharacteristicSemilinearLeadingCoefficient_ne_zero

L114 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicSemilinearLeadingCoefficient_ne_zero
Documentation

A nonzero source constant term gives a nonzero chosen leading coefficient.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
theorem chosenEqualCharacteristicSemilinearLeadingCoefficient_ne_zero
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) :
    chosenEqualCharacteristicSemilinearLeadingCoefficient u ≠ 0
def

chosenEqualCharacteristicSemilinearCoefficient

L129 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicSemilinearCoefficient
Documentation

Coefficients of the exact semilinear solution. At stage n+1, the new coefficient is chosen as a root of the separable additive polynomial forced by the first n+1 coefficient equations.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · full declaration
def chosenEqualCharacteristicSemilinearCoefficient
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) :
    (n : ℕ) → AlgebraicClosure k
  | 0 => chosenEqualCharacteristicSemilinearLeadingCoefficient u
  | n + 1 =>
      Classical.choose
        (exists_frobenius_eq_mul_add k
          (algebraMap k (AlgebraicClosure k) (PowerSeries.coeff 0 u))
          (∑ j : Fin (n + 1),
            algebraMap k (AlgebraicClosure k)
                (PowerSeries.coeff (j + 1) u) *
              chosenEqualCharacteristicSemilinearCoefficient u hu (n - j)))
termination_by n => n
decreasing_by
  all_goals exact Nat.lt_succ_of_le (Nat.sub_le _ _)
theorem

chosenEqualCharacteristicSemilinearCoefficient_zero

L147 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicSemilinearCoefficient_zero
Documentation

The zeroth semilinear coefficient is the chosen leading coefficient.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
theorem chosenEqualCharacteristicSemilinearCoefficient_zero
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) :
    chosenEqualCharacteristicSemilinearCoefficient u hu 0 =
      chosenEqualCharacteristicSemilinearLeadingCoefficient u
theorem

chosenEqualCharacteristicSemilinearCoefficient_succ

L154 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicSemilinearCoefficient_succ
Documentation

Successive semilinear coefficients satisfy the defining Frobenius recursion.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
theorem chosenEqualCharacteristicSemilinearCoefficient_succ
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) (n : ℕ) :
    chosenEqualCharacteristicSemilinearCoefficient u hu (n + 1) ^ Nat.card k =
      algebraMap k (AlgebraicClosure k) (PowerSeries.coeff 0 u) *
          chosenEqualCharacteristicSemilinearCoefficient u hu (n + 1) +
        ∑ j : Fin (n + 1),
          algebraMap k (AlgebraicClosure k)
              (PowerSeries.coeff (j + 1) u) *
            chosenEqualCharacteristicSemilinearCoefficient u hu (n - j)
def

equalCharacteristicSemilinearUnit

L174 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSemilinearUnit
Documentation

The exact power-series solution of the semilinear Hilbert--90 equation in the completed maximal unramified coefficient ring.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
def equalCharacteristicSemilinearUnit
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) :
    (AlgebraicClosure k)⟦X⟧
theorem

equalCharacteristicSemilinearUnit_coeff

L181 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSemilinearUnit_coeff
Documentation

The semilinear unit records the recursively chosen coefficients.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
theorem equalCharacteristicSemilinearUnit_coeff
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) (n : ℕ) :
    PowerSeries.coeff n (equalCharacteristicSemilinearUnit u hu) =
      chosenEqualCharacteristicSemilinearCoefficient u hu n
theorem

equalCharacteristicSemilinearUnit_constantCoeff_ne_zero

L188 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSemilinearUnit_constantCoeff_ne_zero
Documentation

The semilinear unit has nonzero constant coefficient.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
theorem equalCharacteristicSemilinearUnit_constantCoeff_ne_zero
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) :
    PowerSeries.coeff 0 (equalCharacteristicSemilinearUnit u hu) ≠ 0
theorem

equalCharacteristicPowerSeriesFrobenius_semilinearUnit

L197 ↗
LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesFrobenius_semilinearUnit
Documentation

The completed theta-intertwining theorem, linear theta-coefficient equation: phi(epsilon) = u * epsilon.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
Lean source · statement
theorem equalCharacteristicPowerSeriesFrobenius_semilinearUnit
    (u : k⟦X⟧) (hu : PowerSeries.coeff 0 u ≠ 0) :
    equalCharacteristicPowerSeriesFrobenius k
        (equalCharacteristicSemilinearUnit u hu) =
      PowerSeries.map (algebraMap k (AlgebraicClosure k)) u *
        equalCharacteristicSemilinearUnit u hu
def

equalCharacteristicCompletedUnit

L241 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnit
Documentation

The image in the completed maximal-unramified coefficient ring of the unit relating the two prime elements.

Source context 9 commands

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

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

equalCharacteristicCompletedSourceUniformizer

L247 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedSourceUniformizer
Documentation

We normalize the target prime to T; the source prime is therefore bar_pi = u^{-1} T.

Source context 9 commands

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

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

equalCharacteristicThetaGamma

L254 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaGamma
Documentation

The contracting coefficient gamma_j = bar_pi^(q^j) / T in the j-th theta recursion.

Source context 9 commands

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

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

equalCharacteristicThetaGamma_constantCoeff

L261 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaGamma_constantCoeff
Documentation

Positive-index theta gamma terms have zero constant coefficient.

Source context 9 commands

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

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

equalCharacteristicThetaGamma_mul_X

L270 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaGamma_mul_X
Documentation

Multiplying theta gamma by X gives the corresponding source-uniformizer power.

Source context 9 commands

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

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

equalCharacteristicThetaBetaNumerator

L298 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaBetaNumerator
Documentation

The numerator occurring on the right of the j-th theta recursion.

Source context 9 commands

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

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

equalCharacteristicThetaBetaNumerator_constantCoeff

L304 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaBetaNumerator_constantCoeff
Documentation

The theta beta numerator has zero constant coefficient.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
section ThetaRecursion
variable (u : k⟦X⟧ˣ)
Lean source · statement
theorem equalCharacteristicThetaBetaNumerator_constantCoeff
    (b : (AlgebraicClosure k)⟦X⟧) :
    PowerSeries.coeff 0 (equalCharacteristicThetaBetaNumerator b) = 0
def

equalCharacteristicThetaBeta

L313 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaBeta
Documentation

The quotient beta(b) = (phi(b) - b^q) / T.

Source context 9 commands

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

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

equalCharacteristicThetaBeta_mul_X

L320 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaBeta_mul_X
Documentation

Multiplying theta beta by X recovers its numerator.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
section ThetaRecursion
variable (u : k⟦X⟧ˣ)
Lean source · statement
theorem equalCharacteristicThetaBeta_mul_X
    (b : (AlgebraicClosure k)⟦X⟧) :
    PowerSeries.X * equalCharacteristicThetaBeta b =
      equalCharacteristicThetaBetaNumerator b
def

equalCharacteristicThetaCoefficient

L334 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaCoefficient
Documentation

The coefficients b_j of the additive theta series theta(X)=sum_j b_j X^(q^j). The leading coefficient is the exact semilinear unit constructed above; every later coefficient is the unique contracting solution supplied by the contracting Frobenius equation.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
section ThetaRecursion
variable (u : k⟦X⟧ˣ)
Lean source · full declaration
def equalCharacteristicThetaCoefficient :
    ℕ → (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
        (equalCharacteristicThetaGamma u (j + 1))
        (equalCharacteristicThetaBeta
          (equalCharacteristicThetaCoefficient j))
theorem

equalCharacteristicThetaCoefficient_zero

L351 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaCoefficient_zero
Documentation

The zeroth theta coefficient is the semilinear source unit.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
section ThetaRecursion
variable (u : k⟦X⟧ˣ)
Lean source · full declaration
theorem equalCharacteristicThetaCoefficient_zero :
    equalCharacteristicThetaCoefficient 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

equalCharacteristicThetaCoefficient_succ_equation

L363 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaCoefficient_succ_equation
Documentation

The canonical contracting recursion for the non-leading theta coefficients.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries Polynomial
universe u
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
variable {k}
section ThetaRecursion
variable (u : k⟦X⟧ˣ)
Lean source · statement
theorem equalCharacteristicThetaCoefficient_succ_equation (j : ℕ) :
    equalCharacteristicThetaCoefficient u (j + 1) -
        equalCharacteristicThetaGamma u (j + 1) *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicThetaCoefficient u (j + 1)) =
      equalCharacteristicThetaBeta
        (equalCharacteristicThetaCoefficient u j)
theorem

equalCharacteristicThetaCoefficient_succ_comparison

L383 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaCoefficient_succ_comparison
Documentation

Clearing the factor T gives the coefficient comparison in theta^phi o e_bar = e_T o theta.

Source context 9 commands

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

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

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