Module

ContractingEquation.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.ContractingEquation

8 declarations indexed from sourceView source ↗

Module documentation

LubinTate the contracting Frobenius equation: the contracting Frobenius equation

The coefficient recursion in the proof of the contracting Frobenius equation repeatedly solves

α - γ φ(α) = β

in a complete discrete valuation ring, where γ has positive valuation. For an equal-characteristic power-series ring, positive valuation is exactly the vanishing of the constant coefficient. The equation can therefore be solved algebraically, coefficient by coefficient: the coefficient of degree n on the right only involves coefficients of α of degree strictly less than n.

This file records that source-producing recursion directly. No completeness or external existence assumption is needed.

Imports2

Mathlib.RingTheory.PowerSeries.Basic
Mathlib.Algebra.BigOperators.NatAntidiagonal

Imported by4

def

contractingFrobeniusEquationCoeff

L41 ↗

LubinTate.EqualCharacteristic.contractingFrobeniusEquationCoeff

Documentation

The recursively determined coefficients of the solution of α = β + γ * φ(α) when γ(0)=0.

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

def contractingFrobeniusEquationCoeff
    (φ : R →+* R) (γ β : R⟦X⟧) : ℕ → R

theorem

contractingFrobeniusEquationCoeff_eq

L50 ↗

LubinTate.EqualCharacteristic.contractingFrobeniusEquationCoeff_eq

Documentation

States the theorem contractingFrobeniusEquationCoeff_eq.

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

theorem contractingFrobeniusEquationCoeff_eq
    (φ : R →+* R) (γ β : R⟦X⟧) (n : ℕ) :
    contractingFrobeniusEquationCoeff φ γ β n =
      PowerSeries.coeff n β +
        ∑ k : Fin n,
          PowerSeries.coeff (k.1 + 1) γ *
            φ (contractingFrobeniusEquationCoeff φ γ β (n - 1 - k.1))

def

contractingFrobeniusEquationSolution

L61 ↗

LubinTate.EqualCharacteristic.contractingFrobeniusEquationSolution

Documentation

The power series obtained from the contracting coefficient recursion.

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

def contractingFrobeniusEquationSolution
    (φ : R →+* R) (γ β : R⟦X⟧) : R⟦X⟧

theorem

contractingFrobeniusEquationSolution_coeff

L67 ↗

LubinTate.EqualCharacteristic.contractingFrobeniusEquationSolution_coeff

Documentation

States the theorem contractingFrobeniusEquationSolution_coeff.

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

theorem contractingFrobeniusEquationSolution_coeff
    (φ : R →+* R) (γ β : R⟦X⟧) (n : ℕ) :
    PowerSeries.coeff n
        (contractingFrobeniusEquationSolution φ γ β) =
      contractingFrobeniusEquationCoeff φ γ β n

theorem

sum_range_succ_convolution_of_constantCoeff_eq_zero

L74 ↗

LubinTate.EqualCharacteristic.sum_range_succ_convolution_of_constantCoeff_eq_zero

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

theorem sum_range_succ_convolution_of_constantCoeff_eq_zero
    (φ : R →+* R) (γ α : R⟦X⟧)
    (hγ : PowerSeries.coeff 0 γ = 0) (n : ℕ) :
    ∑ k ∈ Finset.range (n + 1),
        PowerSeries.coeff k γ * φ (PowerSeries.coeff (n - k) α) =
      ∑ k ∈ Finset.range n,
        PowerSeries.coeff (k + 1) γ *
          φ (PowerSeries.coeff (n - 1 - k) α)

theorem

contractingFrobeniusEquationSolution_spec

L91 ↗

LubinTate.EqualCharacteristic.contractingFrobeniusEquationSolution_spec

Documentation

The recursively constructed series solves the contracting Frobenius equation from the contracting Frobenius equation.

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

theorem contractingFrobeniusEquationSolution_spec
    (φ : R →+* R) (γ β : R⟦X⟧)
    (hγ : PowerSeries.coeff 0 γ = 0) :
    contractingFrobeniusEquationSolution φ γ β =
      β + γ * PowerSeries.map φ
        (contractingFrobeniusEquationSolution φ γ β)

theorem

contractingFrobeniusEquationSolution_unique

L110 ↗

LubinTate.EqualCharacteristic.contractingFrobeniusEquationSolution_unique

Documentation

Uniqueness of the contracting Frobenius equation. This is the coefficientwise replacement for a global valuation argument.

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

theorem contractingFrobeniusEquationSolution_unique
    (φ : R →+* R) (γ β α : R⟦X⟧)
    (hγ : PowerSeries.coeff 0 γ = 0)
    (hα : α = β + γ * PowerSeries.map φ α) :
    α = contractingFrobeniusEquationSolution φ γ β

theorem

existsUnique_contractingFrobeniusEquation

L136 ↗

LubinTate.EqualCharacteristic.existsUnique_contractingFrobeniusEquation

Documentation

traditional notation form: the unique solution of α - γ φ(α) = β.

Source context 5 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
namespace EqualCharacteristic
variable {R : Type*} [CommRing R]

Lean source · statement

theorem existsUnique_contractingFrobeniusEquation
    (φ : R →+* R) (γ β : R⟦X⟧)
    (hγ : PowerSeries.coeff 0 γ = 0) :
    ∃! α : R⟦X⟧, α - γ * PowerSeries.map φ α = β

Module documentation

LubinTate the contracting Frobenius equation: the contracting Frobenius equation

Declarations