NYLL
Module

DirectThetaFirstIdentity.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.DirectThetaFirstIdentity
10 declarations indexed from sourceView source ↗

Module documentation

First theta identity for the completed change of parameter

For the standard source prime T and target prime uT, this file proves

theta^φ = theta ∘ [u].

The bracket [u] is the independently constructed endomorphism of the standard Lubin--Tate group from EqualCharacteristicDirectLubinTateBracket. The proof follows the uniqueness argument: both sides have the same linear coefficient and satisfy the same contracting coefficient recursion.

Imports3
Imported by4

Declarations

def

equalCharacteristicDirectThetaAfterBracketCoefficient

L40 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAfterBracketCoefficient
Documentation

Coefficients of the formal composite theta ∘ [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 equalCharacteristicDirectThetaAfterBracketCoefficient
    (u : k⟦X⟧ˣ) : ℕ → (AlgebraicClosure k)⟦X⟧
theorem

equalCharacteristicDirectThetaSeries_subst_directBracket

L47 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries_subst_directBracket
Documentation

The composite theta ∘ [u] written as a sparse q-additive 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_subst_directBracket
    (u : k⟦X⟧ˣ) :
    PowerSeries.subst
        (equalCharacteristicCompletedDirectBracket (u : k⟦X⟧))
        (equalCharacteristicDirectThetaSeries u) =
      equalCharacteristicQAdditiveSeries k
        (equalCharacteristicDirectThetaAfterBracketCoefficient u)
theorem

equalCharacteristicDirectThetaAfterBracketCoefficient_zero

L59 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAfterBracketCoefficient_zero
Documentation

The linear term of theta ∘ [u] is φ(b₀).

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 equalCharacteristicDirectThetaAfterBracketCoefficient_zero
    (u : k⟦X⟧ˣ) :
    equalCharacteristicDirectThetaAfterBracketCoefficient u 0 =
      equalCharacteristicPowerSeriesFrobenius k
        (equalCharacteristicDirectThetaCoefficient u 0)
theorem

equalCharacteristicDirectThetaSeries_subst_directBracket_intertwines

L79 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeries_subst_directBracket_intertwines
Documentation

Since [u] is Frobenius-fixed and commutes with e_T, the composite theta ∘ [u] satisfies theta's direct Frobenius-intertwining 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 equalCharacteristicDirectThetaSeries_subst_directBracket_intertwines
    (u : k⟦X⟧ˣ) :
    PowerSeries.subst
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
        (PowerSeries.map (equalCharacteristicPowerSeriesFrobenius k)
          (PowerSeries.subst
            (equalCharacteristicCompletedDirectBracket (u : k⟦X⟧))
            (equalCharacteristicDirectThetaSeries u))) =
      PowerSeries.subst
        (PowerSeries.subst
          (equalCharacteristicCompletedDirectBracket (u : k⟦X⟧))
          (equalCharacteristicDirectThetaSeries u))
        (equalCharacteristicCompletedLubinTateSeries (k := k)
          (equalCharacteristicDirectCompletedTargetUniformizer u))
theorem

equalCharacteristicDirectQAdditiveIntertwiner_succ_comparison

L141 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectQAdditiveIntertwiner_succ_comparison
Documentation

Coefficient form of a direct-orientation Frobenius intertwiner.

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 equalCharacteristicDirectQAdditiveIntertwiner_succ_comparison
    (u : k⟦X⟧ˣ)
    (c : ℕ → (AlgebraicClosure k)⟦X⟧)
    (hintertwines :
      PowerSeries.subst
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (PowerSeries.X : (AlgebraicClosure k)⟦X⟧))
          (equalCharacteristicQAdditiveSeries k
            (fun i ↦ equalCharacteristicPowerSeriesFrobenius k (c i))) =
        PowerSeries.subst (equalCharacteristicQAdditiveSeries k c)
          (equalCharacteristicCompletedLubinTateSeries (k := k)
            (equalCharacteristicDirectCompletedTargetUniformizer u)))
    (j : ℕ) :
    equalCharacteristicDirectCompletedTargetUniformizer u * c (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicPowerSeriesFrobenius k (c (j + 1)) =
      equalCharacteristicPowerSeriesFrobenius k (c j) -
        c j ^ Nat.card k := by
  rw [equalCharacteristicQAdditiveSeries_subst_completedLubinTateSeries,
    equalCharacteristicCompletedLubinTateSeries_subst_qAdditiveSeries]
    at hintertwines
  have hcoeff := congrArg
    (PowerSeries.coeff (Nat.card k ^ (j + 1))) hintertwines
  rw [equalCharacteristicQAdditiveSeries_coeff_pow,
    equalCharacteristicQAdditiveSeries_coeff_pow,
    equalCharacteristicLubinTateSubstitutionCoefficient,
    equalCharacteristicLubinTatePostcompositionCoefficient] at hcoeff
  linear_combination -hcoeff
theorem

equalCharacteristicDirectQAdditiveIntertwinerCoefficient_unique

L173 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectQAdditiveIntertwinerCoefficient_unique
Documentation

Direct-orientation intertwiners with the same linear coefficient are equal. At every higher coefficient this is exactly the uniqueness clause of the contracting Frobenius 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 equalCharacteristicDirectQAdditiveIntertwinerCoefficient_unique
    (u : k⟦X⟧ˣ)
    (c d : ℕ → (AlgebraicClosure k)⟦X⟧)
    (hzero : c 0 = d 0)
    (hc : ∀ j : ℕ,
      equalCharacteristicDirectCompletedTargetUniformizer u * c (j + 1) -
          PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
            equalCharacteristicPowerSeriesFrobenius k (c (j + 1)) =
        equalCharacteristicPowerSeriesFrobenius k (c j) -
          c j ^ Nat.card k)
    (hd : ∀ j : ℕ,
      equalCharacteristicDirectCompletedTargetUniformizer u * d (j + 1) -
          PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
            equalCharacteristicPowerSeriesFrobenius k (d (j + 1)) =
        equalCharacteristicPowerSeriesFrobenius k (d j) -
          d j ^ Nat.card k) :
    c = d
theorem

equalCharacteristicDirectCompletedTargetUniformizer_frobenius

L239 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectCompletedTargetUniformizer_frobenius
Documentation

The target prime uT is fixed by arithmetic Frobenius.

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 equalCharacteristicDirectCompletedTargetUniformizer_frobenius
    (u : k⟦X⟧ˣ) :
    equalCharacteristicPowerSeriesFrobenius k
        (equalCharacteristicDirectCompletedTargetUniformizer u) =
      equalCharacteristicDirectCompletedTargetUniformizer u
theorem

equalCharacteristicDirectThetaFrobeniusCoefficient_succ_comparison

L250 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaFrobeniusCoefficient_succ_comparison
Documentation

Applying Frobenius to theta's coefficient comparison gives the recursion for the coefficients of 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 equalCharacteristicDirectThetaFrobeniusCoefficient_succ_comparison
    (u : k⟦X⟧ˣ) (j : ℕ) :
    equalCharacteristicDirectCompletedTargetUniformizer u *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicDirectThetaCoefficient u (j + 1)) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicPowerSeriesFrobenius k
              (equalCharacteristicDirectThetaCoefficient u (j + 1))) =
      equalCharacteristicPowerSeriesFrobenius k
          (equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicDirectThetaCoefficient u j)) -
        equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicDirectThetaCoefficient u j) ^ Nat.card k
theorem

equalCharacteristicDirectThetaAfterBracketCoefficient_succ_comparison

L271 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAfterBracketCoefficient_succ_comparison
Documentation

Coefficients of theta ∘ [u] obey the same direct 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
theorem equalCharacteristicDirectThetaAfterBracketCoefficient_succ_comparison
    (u : k⟦X⟧ˣ) (j : ℕ) :
    equalCharacteristicDirectCompletedTargetUniformizer u *
          equalCharacteristicDirectThetaAfterBracketCoefficient u (j + 1) -
        PowerSeries.X ^ (Nat.card k ^ (j + 1)) *
          equalCharacteristicPowerSeriesFrobenius k
            (equalCharacteristicDirectThetaAfterBracketCoefficient u (j + 1)) =
      equalCharacteristicPowerSeriesFrobenius k
          (equalCharacteristicDirectThetaAfterBracketCoefficient u j) -
        equalCharacteristicDirectThetaAfterBracketCoefficient u j ^ Nat.card k
theorem

equalCharacteristicDirectThetaSeriesFrobenius_eq_subst_directBracket

L291 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaSeriesFrobenius_eq_subst_directBracket
Documentation

The completed theta-intertwining theorem, first theta identity in the direct orientation: theta^φ = theta ∘ [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
theorem equalCharacteristicDirectThetaSeriesFrobenius_eq_subst_directBracket
    (u : k⟦X⟧ˣ) :
    equalCharacteristicDirectThetaSeriesFrobenius u =
      PowerSeries.subst
        (equalCharacteristicCompletedDirectBracket (u : k⟦X⟧))
        (equalCharacteristicDirectThetaSeries u)

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