NYLL
Module

DirectLubinTateBracketRecursion.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.DirectLubinTateBracketRecursion
13 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: recursion for the standard Lubin--Tate bracket

The standard bracket constructed from its contracting coefficient equations agrees with the recursive T-adic bracket used in the finite Lubin–Tate bracket construction. At the formal series level the required identity is

[a](Y) = a₀ Y + [tail(a)](e_T(Y)).

This file proves the identity from uniqueness of the commuting q-additive series. It is the bridge from the formal bracket used in the theta identity to the finite brackets acting on division points.

Imports2
Imported by4

Declarations

def

equalCharacteristicDirectBracketScalarCoefficient

L40 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketScalarCoefficient
Documentation

The scalar-linear summand a₀Y, in sparse additive coordinates.

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 equalCharacteristicDirectBracketScalarCoefficient
    (a : k⟦X⟧) : ℕ → (AlgebraicClosure k)⟦X⟧
  | 0 => PowerSeries.C
      (algebraMap k (AlgebraicClosure k) (PowerSeries.coeff 0 a))
  | _ + 1 => 0
def

equalCharacteristicDirectBracketTailCompositionCoefficient

L47 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketTailCompositionCoefficient
Documentation

Coefficients of [tail(a)] ∘ e_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 equalCharacteristicDirectBracketTailCompositionCoefficient
    (a : k⟦X⟧) : ℕ → (AlgebraicClosure k)⟦X⟧
def

equalCharacteristicDirectBracketRecursiveCoefficient

L56 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketRecursiveCoefficient
Documentation

Coefficients of the recursive candidate a₀Y + [tail(a)] ∘ e_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 equalCharacteristicDirectBracketRecursiveCoefficient
    (a : k⟦X⟧) : ℕ → (AlgebraicClosure k)⟦X⟧
theorem

equalCharacteristicDirectBracketScalarSeries_eq

L61 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketScalarSeries_eq
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 equalCharacteristicDirectBracketScalarSeries_eq
    (a : k⟦X⟧) :
    equalCharacteristicQAdditiveSeries k
        (equalCharacteristicDirectBracketScalarCoefficient a) =
      PowerSeries.C (PowerSeries.C
          (algebraMap k (AlgebraicClosure k) (PowerSeries.coeff 0 a))) *
        PowerSeries.X
theorem

equalCharacteristicDirectBracketRecursiveSeries_eq

L96 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketRecursiveSeries_eq
Documentation

The recursive candidate is the sum of its scalar term and the genuine formal substitution [tail(a)] ∘ e_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
theorem equalCharacteristicDirectBracketRecursiveSeries_eq
    (a : k⟦X⟧) :
    equalCharacteristicQAdditiveSeries k
        (equalCharacteristicDirectBracketRecursiveCoefficient a) =
      PowerSeries.C (PowerSeries.C
          (algebraMap k (AlgebraicClosure k) (PowerSeries.coeff 0 a))) *
          PowerSeries.X +
        PowerSeries.subst
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
          (equalCharacteristicCompletedDirectBracket
            (equalCharacteristicPowerSeriesTail a))
theorem

equalCharacteristicDirectQAdditiveEndomorphism_succ_comparison

L119 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectQAdditiveEndomorphism_succ_comparison
Documentation

Coefficient recurrence read from commutation with e_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
theorem equalCharacteristicDirectQAdditiveEndomorphism_succ_comparison
    (c : ℕ → (AlgebraicClosure k)⟦X⟧)
    (hcommutes :
      PowerSeries.subst (equalCharacteristicQAdditiveSeries k c)
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (PowerSeries.X : (AlgebraicClosure k)⟦X⟧)) =
        PowerSeries.subst
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
          (equalCharacteristicQAdditiveSeries k c))
    (j : ℕ) :
    PowerSeries.X * c (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) * c (j + 1) =
      c j - c j ^ Nat.card k
theorem

equalCharacteristicDirectBracketScalarCoefficient_succ_comparison

L144 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketScalarCoefficient_succ_comparison
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 equalCharacteristicDirectBracketScalarCoefficient_succ_comparison
    (a : k⟦X⟧) (j : ℕ) :
    PowerSeries.X *
          equalCharacteristicDirectBracketScalarCoefficient a (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicDirectBracketScalarCoefficient a (j + 1) =
      equalCharacteristicDirectBracketScalarCoefficient a j -
        equalCharacteristicDirectBracketScalarCoefficient a j ^ Nat.card k
theorem

equalCharacteristicDirectBracketTailCompositionSeries_commutes

L159 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketTailCompositionSeries_commutes
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 equalCharacteristicDirectBracketTailCompositionSeries_commutes
    (a : k⟦X⟧) :
    PowerSeries.subst
        (equalCharacteristicQAdditiveSeries k
          (equalCharacteristicDirectBracketTailCompositionCoefficient a))
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧)) =
      PowerSeries.subst
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
        (equalCharacteristicQAdditiveSeries k
          (equalCharacteristicDirectBracketTailCompositionCoefficient a))
theorem

equalCharacteristicDirectBracketTailCompositionCoefficient_succ_comparison

L210 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketTailCompositionCoefficient_succ_comparison
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
    equalCharacteristicDirectBracketTailCompositionCoefficient_succ_comparison
    (a : k⟦X⟧) (j : ℕ) :
    PowerSeries.X *
          equalCharacteristicDirectBracketTailCompositionCoefficient a (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicDirectBracketTailCompositionCoefficient a (j + 1) =
      equalCharacteristicDirectBracketTailCompositionCoefficient a j -
        equalCharacteristicDirectBracketTailCompositionCoefficient a j ^
          Nat.card k
theorem

equalCharacteristicDirectBracketRecursiveCoefficient_zero

L225 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketRecursiveCoefficient_zero
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 equalCharacteristicDirectBracketRecursiveCoefficient_zero
    (a : k⟦X⟧) :
    equalCharacteristicDirectBracketRecursiveCoefficient a 0 =
      PowerSeries.map (algebraMap k (AlgebraicClosure k)) a
theorem

equalCharacteristicDirectBracketRecursiveCoefficient_succ_comparison

L239 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectBracketRecursiveCoefficient_succ_comparison
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
    equalCharacteristicDirectBracketRecursiveCoefficient_succ_comparison
    (a : k⟦X⟧) (j : ℕ) :
    PowerSeries.X *
          equalCharacteristicDirectBracketRecursiveCoefficient a (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicDirectBracketRecursiveCoefficient a (j + 1) =
      equalCharacteristicDirectBracketRecursiveCoefficient a j -
        equalCharacteristicDirectBracketRecursiveCoefficient a j ^ Nat.card k
theorem

equalCharacteristicCompletedDirectEndomorphismCoefficient_unique

L279 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectEndomorphismCoefficient_unique
Documentation

Uniqueness of a standard commuting q-additive endomorphism from 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 · statement
theorem equalCharacteristicCompletedDirectEndomorphismCoefficient_unique
    (c d : ℕ → (AlgebraicClosure k)⟦X⟧)
    (hzero : c 0 = d 0)
    (hc : ∀ j : ℕ,
      PowerSeries.X * c (j + 1) -
          PowerSeries.X ^ (Nat.card k ^ (j + 1)) * c (j + 1) =
        c j - c j ^ Nat.card k)
    (hd : ∀ j : ℕ,
      PowerSeries.X * d (j + 1) -
          PowerSeries.X ^ (Nat.card k ^ (j + 1)) * d (j + 1) =
        d j - d j ^ Nat.card k) :
    c = d
theorem

equalCharacteristicCompletedDirectBracket_recursion

L333 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedDirectBracket_recursion
Documentation

Formal recursive identity for the standard 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_recursion
    (a : k⟦X⟧) :
    equalCharacteristicCompletedDirectBracket a =
      PowerSeries.C (PowerSeries.C
          (algebraMap k (AlgebraicClosure k) (PowerSeries.coeff 0 a))) *
          PowerSeries.X +
        PowerSeries.subst
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
          (equalCharacteristicCompletedDirectBracket
            (equalCharacteristicPowerSeriesTail a))

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