Module

DirectLubinTateBracket.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.DirectLubinTateBracket

20 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: the standard equal-characteristic Lubin--Tate bracket

In the proof of the completed theta-intertwining theorem the standard Lubin--Tate series is

e_T(Y) = Y^q + T Y.

For a unit u, this file constructs the endomorphism [u] of this standard Lubin--Tate group. Its linear coefficient is u; the higher additive coefficients are the unique contracting solutions forced by commutation with e_T. This is the orientation used in the completed theta-intertwining theorem itself, as opposed to the normalization u⁻¹T -> T used in Corollary the Lubin–Tate endomorphism commutation law.

Imports2

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Theta.ThetaFirstIdentity

Imported by5

def

equalCharacteristicDirectBracketGamma

L41 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketGamma

Documentation

After division by T, the contracting coefficient in the recurrence for the coefficients of the standard bracket [u].

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 equalCharacteristicDirectBracketGamma
    (j : ℕ) : k⟦X⟧

theorem

equalCharacteristicDirectBracketGamma_constantCoeff

L46 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketGamma_constantCoeff

Documentation

Positive-index direct bracket 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 equalCharacteristicDirectBracketGamma_constantCoeff
    (j : ℕ) (hj : 0 < j) :
    PowerSeries.coeff 0 (equalCharacteristicDirectBracketGamma (k := k) j) = 0

def

equalCharacteristicDirectBracketBeta

L55 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketBeta

Documentation

Division of a-a^q by the standard prime T.

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 equalCharacteristicDirectBracketBeta
    (a : k⟦X⟧) : k⟦X⟧

def

equalCharacteristicDirectBracketCoefficient

L61 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketCoefficient

Documentation

Additive coefficients of the standard Lubin--Tate endomorphism [u].

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 equalCharacteristicDirectBracketCoefficient
    (u : k⟦X⟧) : ℕ → k⟦X⟧
  | 0 => u
  | j + 1 =>
      contractingFrobeniusEquationSolution (R := k)
        (RingHom.id k)
        (equalCharacteristicDirectBracketGamma (k := k) (j + 1))
        (equalCharacteristicDirectBracketBeta
          (equalCharacteristicDirectBracketCoefficient u j))

theorem

equalCharacteristicDirectBracketCoefficient_zero

L74 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketCoefficient_zero

Documentation

The zeroth direct bracket coefficient is the input power series.

Source context 7 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]
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicDirectBracketCoefficient_zero
    (u : k⟦X⟧) :
    equalCharacteristicDirectBracketCoefficient u 0 = u

theorem

equalCharacteristicDirectBracketCoefficient_succ_equation

L80 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketCoefficient_succ_equation

Documentation

Successive direct bracket coefficients satisfy the defining contraction equation.

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 equalCharacteristicDirectBracketCoefficient_succ_equation
    (u : k⟦X⟧) (j : ℕ) :
    equalCharacteristicDirectBracketCoefficient u (j + 1) -
        equalCharacteristicDirectBracketGamma (k := k) (j + 1) *
          equalCharacteristicDirectBracketCoefficient u (j + 1) =
      equalCharacteristicDirectBracketBeta
        (equalCharacteristicDirectBracketCoefficient u j)

theorem

equalCharacteristicDirectBracketCoefficient_succ_comparison

L100 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketCoefficient_succ_comparison

Documentation

Coefficient comparison equivalent to commutation of [u] with e_T(Y)=Y^q+TY.

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 equalCharacteristicDirectBracketCoefficient_succ_comparison
    (u : k⟦X⟧) (j : ℕ) :
    PowerSeries.X *
          equalCharacteristicDirectBracketCoefficient u (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicDirectBracketCoefficient u (j + 1) =
      equalCharacteristicDirectBracketCoefficient u j -
        equalCharacteristicDirectBracketCoefficient u j ^ Nat.card k

def

equalCharacteristicDirectBracket

L143 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracket

Documentation

The standard Lubin--Tate endomorphism [u] over k[[T]].

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 equalCharacteristicDirectBracket
    (u : k⟦X⟧) : (k⟦X⟧)⟦X⟧

theorem

equalCharacteristicDirectBracket_coeff_pow

L150 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracket_coeff_pow

Documentation

The direct bracket 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 equalCharacteristicDirectBracket_coeff_pow
    (u : k⟦X⟧) (j : ℕ) :
    PowerSeries.coeff (Nat.card k ^ j)
        (equalCharacteristicDirectBracket u) =
      equalCharacteristicDirectBracketCoefficient u j

theorem

equalCharacteristicDirectBracket_constantCoeff

L159 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracket_constantCoeff

Documentation

The direct bracket 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 equalCharacteristicDirectBracket_constantCoeff
    (u : k⟦X⟧) :
    PowerSeries.constantCoeff (equalCharacteristicDirectBracket u) = 0

theorem

equalCharacteristicDirectBracket_hasSubst

L165 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectBracket_hasSubst

Documentation

The direct bracket 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 equalCharacteristicDirectBracket_hasSubst
    (u : k⟦X⟧) :
    PowerSeries.HasSubst (equalCharacteristicDirectBracket u)

def

equalCharacteristicCompletedDirectBracketCoefficient

L173 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracketCoefficient

Documentation

Coefficients after extension to the completed maximal unramified integer 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 equalCharacteristicCompletedDirectBracketCoefficient
    (u : k⟦X⟧) (j : ℕ) : (AlgebraicClosure k)⟦X⟧

def

equalCharacteristicCompletedDirectBracket

L179 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracket

Documentation

The standard bracket over the completed maximal unramified integer 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 equalCharacteristicCompletedDirectBracket
    (u : k⟦X⟧) : ((AlgebraicClosure k)⟦X⟧)⟦X⟧

theorem

equalCharacteristicCompletedDirectBracket_coeff_pow

L186 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracket_coeff_pow

Documentation

The completed direct bracket records its jth coefficient at exponent 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 equalCharacteristicCompletedDirectBracket_coeff_pow
    (u : k⟦X⟧) (j : ℕ) :
    PowerSeries.coeff (Nat.card k ^ j)
        (equalCharacteristicCompletedDirectBracket u) =
      equalCharacteristicCompletedDirectBracketCoefficient u j

theorem

equalCharacteristicCompletedDirectBracket_constantCoeff

L195 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracket_constantCoeff

Documentation

The completed direct bracket 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 equalCharacteristicCompletedDirectBracket_constantCoeff
    (u : k⟦X⟧) :
    PowerSeries.constantCoeff
        (equalCharacteristicCompletedDirectBracket u) = 0

theorem

equalCharacteristicCompletedDirectBracket_hasSubst

L202 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracket_hasSubst

Documentation

The completed direct bracket 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 equalCharacteristicCompletedDirectBracket_hasSubst
    (u : k⟦X⟧) :
    PowerSeries.HasSubst (equalCharacteristicCompletedDirectBracket u)

theorem

equalCharacteristicCompletedDirectBracketCoefficient_zero

L211 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracketCoefficient_zero

Documentation

The zeroth completed direct coefficient is the scalar extension of the input.

Source context 7 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]
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedDirectBracketCoefficient_zero
    (u : k⟦X⟧) :
    equalCharacteristicCompletedDirectBracketCoefficient u 0 =
      PowerSeries.map (algebraMap k (AlgebraicClosure k)) u

theorem

equalCharacteristicCompletedDirectBracket_frobenius

L219 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracket_frobenius

Documentation

Every coefficient of the standard bracket is defined over k[[T]], so coefficient Frobenius fixes the bracket.

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 equalCharacteristicCompletedDirectBracket_frobenius
    (u : k⟦X⟧) :
    PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
        (equalCharacteristicCompletedDirectBracket u) =
      equalCharacteristicCompletedDirectBracket u

theorem

equalCharacteristicCompletedDirectBracketCoefficient_succ_comparison

L233 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracketCoefficient_succ_comparison

Documentation

The standard coefficient recurrence after extension to the completed maximal unramified integer 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

theorem equalCharacteristicCompletedDirectBracketCoefficient_succ_comparison
    (u : k⟦X⟧) (j : ℕ) :
    PowerSeries.X *
          equalCharacteristicCompletedDirectBracketCoefficient u (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicCompletedDirectBracketCoefficient u (j + 1) =
      equalCharacteristicCompletedDirectBracketCoefficient u j -
        equalCharacteristicCompletedDirectBracketCoefficient u j ^ Nat.card k

theorem

equalCharacteristicCompletedDirectBracket_commutes

L248 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracket_commutes

Documentation

The standard [u] commutes with e_T(Y)=Y^q+TY.

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 equalCharacteristicCompletedDirectBracket_commutes
    (u : k⟦X⟧) :
    PowerSeries.subst (equalCharacteristicCompletedDirectBracket u)
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧)) =
      PowerSeries.subst
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
        (equalCharacteristicCompletedDirectBracket u)

Module documentation

The completed theta-intertwining theorem: the standard equal-characteristic Lubin--Tate bracket

Declarations