Module

DirectThetaIteration.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.DirectThetaIteration

10 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: iterating the direct second theta identity

For the direct orientation T → uT, this file applies coefficient Frobenius repeatedly to the formal identity theta^φ ∘ e_T = e_(uT) ∘ theta.

Imports2

Imported by4

def

equalCharacteristicDirectThetaSeriesFrobeniusIterate

L29 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobeniusIterate

Documentation

The i-fold arithmetic-Frobenius twist of the direct theta series.

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · full declaration

def equalCharacteristicDirectThetaSeriesFrobeniusIterate
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) :
    ℕ → ((AlgebraicClosure k)⟦X⟧)⟦X⟧
  | 0 => equalCharacteristicDirectThetaSeries u
  | i + 1 => PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
      (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)

theorem

equalCharacteristicDirectThetaSeriesFrobeniusIterate_zero

L38 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobeniusIterate_zero

Documentation

States the theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_zero.

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_zero
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) :
    equalCharacteristicDirectThetaSeriesFrobeniusIterate u 0 =
      equalCharacteristicDirectThetaSeries u

theorem

equalCharacteristicDirectThetaSeriesFrobeniusIterate_succ

L46 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobeniusIterate_succ

Documentation

States the theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_succ.

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_succ
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) (i : ℕ) :
    equalCharacteristicDirectThetaSeriesFrobeniusIterate u (i + 1) =
      PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
        (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)

theorem

equalCharacteristicDirectThetaSeriesFrobeniusIterate_constantCoeff

L55 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobeniusIterate_constantCoeff

Documentation

States the theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_constantCoeff.

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_constantCoeff
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) (i : ℕ) :
    PowerSeries.constantCoeff
      (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i) = 0

theorem

equalCharacteristicDirectThetaSeriesFrobeniusIterate_hasSubst

L67 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobeniusIterate_hasSubst

Documentation

States the theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_hasSubst.

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_hasSubst
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) (i : ℕ) :
    PowerSeries.HasSubst
      (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)

theorem

equalCharacteristicDirectCompletedTargetUniformizer_frobenius

L74 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectCompletedTargetUniformizer_frobenius

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectCompletedTargetUniformizer_frobenius
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) :
    equalCharacteristicPowerSeriesFrobenius k
        (equalCharacteristicDirectCompletedTargetUniformizer u) =
      equalCharacteristicDirectCompletedTargetUniformizer u

theorem

equalCharacteristicDirectCompletedLubinTateSeries_map_frobenius

L82 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectCompletedLubinTateSeries_map_frobenius

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectCompletedLubinTateSeries_map_frobenius
    {k : Type*} [Field k] [Finite k]
    (pi : (AlgebraicClosure k)⟦X⟧) :
    PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
        (equalCharacteristicCompletedLubinTateSeries (k := k) pi) =
      equalCharacteristicCompletedLubinTateSeries (k := k)
        (equalCharacteristicPowerSeriesFrobenius k pi)

theorem

equalCharacteristicDirectSourceLubinTateSeries_frobenius

L91 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectSourceLubinTateSeries_frobenius

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectSourceLubinTateSeries_frobenius
    {k : Type*} [Field k] [Finite k] :
    PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧)) =
      equalCharacteristicCompletedLubinTateSeries (k := k) PowerSeries.X

theorem

equalCharacteristicDirectTargetLubinTateSeries_frobenius

L100 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectTargetLubinTateSeries_frobenius

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectTargetLubinTateSeries_frobenius
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) :
    PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (equalCharacteristicDirectCompletedTargetUniformizer u)) =
      equalCharacteristicCompletedLubinTateSeries (k := k)
        (equalCharacteristicDirectCompletedTargetUniformizer u)

theorem

equalCharacteristicDirectThetaSeriesFrobeniusIterate_intertwines

L112 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobeniusIterate_intertwines

Documentation

Every direct Frobenius twist intertwines the next source and target Lubin--Tate steps.

Source context 4 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic

Lean source · statement

theorem equalCharacteristicDirectThetaSeriesFrobeniusIterate_intertwines
    {k : Type*} [Field k] [Finite k] (u : k⟦X⟧ˣ) (i : ℕ) :
    PowerSeries.subst
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
        (equalCharacteristicDirectThetaSeriesFrobeniusIterate u (i + 1)) =
      PowerSeries.subst
        (equalCharacteristicDirectThetaSeriesFrobeniusIterate u i)
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (equalCharacteristicDirectCompletedTargetUniformizer u))

Module documentation

The completed theta-intertwining theorem: iterating the direct second theta identity

Declarations