Module

MultiplicativeIntertwiner.lean

Nyll.ClassFieldTheory.LubinTate.Padic.MultiplicativeIntertwiner

14 declarations indexed from sourceView source ↗

Module documentation

Comparing the standard and multiplicative Lubin--Tate series over `ℚ_p`

The characteristic-independent same-uniformizer recursion supplies the canonical series with linear coefficient 1 satisfying

[(1 + X)^p - 1](H(X)) = H([pX + X^p](X)).

Consequently, evaluation of H carries standard Lubin--Tate division points to multiplicative division points. This file constructs that series directly; it does not identify the two actions from equality of their kernels.

Imports2

Imported by3

def

padicStandardToMultiplicativeIntertwiner

L35 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner

Documentation

The canonical linear-term-one intertwiner carrying standard Lubin--Tate division points over ℚ_p to multiplicative division points.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

def padicStandardToMultiplicativeIntertwiner
    (p : ℕ) [Fact p.Prime] :
    PowerSeries (padicLocalField p).valuationSubring

theorem

padicStandardToMultiplicativeIntertwiner_hasLinearTerm

L47 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner_hasLinearTerm

Documentation

The standard-to-multiplicative intertwiner has linear coefficient 1 and no constant term.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · full declaration

theorem padicStandardToMultiplicativeIntertwiner_hasLinearTerm
    (p : ℕ) [Fact p.Prime] :
    HasLinearTerm (padicStandardToMultiplicativeIntertwiner p)
      (fun _ : Unit =>
        (1 : (padicLocalField p).valuationSubring)) :=
  recursiveIntertwiner_hasLinearTerm
    (padicMultiplicativeLubinTateSeries_isUniformizer p)
    (padicMultiplicativeLubinTateSeries p)
    (standardLubinTateSeries
      (padicMultiplicativeLubinTateSeries_isUniformizer p))
    (fun _ : Unit => 1)

theorem

padicStandardToMultiplicativeIntertwiner_intertwines

L61 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner_intertwines

Documentation

The canonical series satisfies the literal same-uniformizer equation from the multiplicative series to the standard series.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicStandardToMultiplicativeIntertwiner_intertwines
    (p : ℕ) [Fact p.Prime] :
    Intertwines
      (padicMultiplicativeLubinTateSeries p)
      (standardLubinTateSeries
        (padicMultiplicativeLubinTateSeries_isUniformizer p))
      (padicStandardToMultiplicativeIntertwiner p)

theorem

padicStandardToMultiplicativeIntertwiner_functionalEquation

L77 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner_functionalEquation

Documentation

One-variable form of the intertwining equation: the multiplicative series after H equals H after the standard series.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicStandardToMultiplicativeIntertwiner_functionalEquation
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.subst
        (padicStandardToMultiplicativeIntertwiner p)
        (padicMultiplicativeLubinTateSeries p).toPowerSeries =
      PowerSeries.subst
        (standardLubinTateSeries
          (padicMultiplicativeLubinTateSeries_isUniformizer p)).toPowerSeries
        (padicStandardToMultiplicativeIntertwiner p)

theorem

padicStandardToMultiplicativeIntertwiner_hasSubst

L115 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner_hasSubst

Documentation

The intertwiner has zero constant coefficient, hence admits formal substitution.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicStandardToMultiplicativeIntertwiner_hasSubst
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.HasSubst
      (padicStandardToMultiplicativeIntertwiner p)

theorem

padicStandardToMultiplicativeIntertwiner_coeff_one

L123 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner_coeff_one

Documentation

The coefficient of X in the canonical intertwiner is 1.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicStandardToMultiplicativeIntertwiner_coeff_one
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.coeff 1
        (padicStandardToMultiplicativeIntertwiner p) =
      1

theorem

padicStandardToMultiplicativeIntertwiner_endomorphism

L133 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner_endomorphism

Documentation

Conjugating a standard scalar endomorphism through the canonical comparison gives the unique multiplicative-series endomorphism with the same scalar linear coefficient.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · full declaration

theorem padicStandardToMultiplicativeIntertwiner_endomorphism
    (p : ℕ) [Fact p.Prime]
    (a : (padicLocalField p).valuationSubring) :
    PowerSeries.subst
        (standardLubinTateEndomorphism
          (padicMultiplicativeLubinTateSeries_isUniformizer p) a)
        (padicStandardToMultiplicativeIntertwiner p) =
      PowerSeries.subst
        (padicStandardToMultiplicativeIntertwiner p)
        (recursiveIntertwiner
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          (padicMultiplicativeLubinTateSeries p)
          (padicMultiplicativeLubinTateSeries p)
          (fun _ : Unit => a)) := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let E := padicMultiplicativeLubinTateSeries p
  let Ebar := standardLubinTateSeries hπ
  let H := padicStandardToMultiplicativeIntertwiner p
  let S := standardLubinTateEndomorphism hπ a
  let M :=
    recursiveIntertwiner hπ E E (fun _ : Unit => a)
  have hH :
      HasLinearTerm H
        (fun _ : Unit =>
          (1 : (padicLocalField p).valuationSubring)) :=
    padicStandardToMultiplicativeIntertwiner_hasLinearTerm p
  have hS :
      HasLinearTerm S (fun _ : Unit => a) :=
    standardLubinTateEndomorphism_hasLinearTerm hπ a
  have hM :
      HasLinearTerm M (fun _ : Unit => a) :=
    recursiveIntertwiner_hasLinearTerm hπ E E (fun _ : Unit => a)
  have hleftLinearRaw :=
    hH.subst
      (G := fun _ : Unit => S)
      (M := fun _ : Unit => fun _ : Unit => a)
      (fun _ => hS)
  have hleftLinear :
      HasLinearTerm (PowerSeries.subst S H)
        (fun _ : Unit => a) := by
    simpa [PowerSeries.subst_def] using hleftLinearRaw
  have hrightLinearRaw :=
    hM.subst
      (G := fun _ : Unit => H)
      (M := fun _ : Unit => fun _ : Unit =>
        (1 : (padicLocalField p).valuationSubring))
      (fun _ => hH)
  have hrightLinear :
      HasLinearTerm (PowerSeries.subst H M)
        (fun _ : Unit => a) := by
    simpa [PowerSeries.subst_def] using hrightLinearRaw
  have hHIntertwines :
      Intertwines E Ebar H :=
    padicStandardToMultiplicativeIntertwiner_intertwines p
  have hSIntertwines :
      Intertwines Ebar Ebar S :=
    standardLubinTateEndomorphism_intertwines hπ a
  have hMIntertwines :
      Intertwines E E M :=
    recursiveIntertwiner_intertwines hπ E E (fun _ : Unit => a)
  have hleftIntertwines :
      Intertwines E Ebar (PowerSeries.subst S H) :=
    hHIntertwines.powerSeries_subst hH.hasSubst
      hSIntertwines hS.hasSubst
  have hrightIntertwines :
      Intertwines E Ebar (PowerSeries.subst H M) :=
    hMIntertwines.powerSeries_subst hM.hasSubst
      hHIntertwines hH.hasSubst
  exact
    eq_of_hasLinearTerm_of_intertwines hπ E Ebar
      (fun _ : Unit => a)
      hleftLinear hleftIntertwines
      hrightLinear hrightIntertwines

def

padicMultiplicativeToStandardIntertwiner

L209 ↗

LubinTate.padicMultiplicativeToStandardIntertwiner

Documentation

The canonical inverse-direction intertwiner carrying multiplicative division points to standard Lubin--Tate division points.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

def padicMultiplicativeToStandardIntertwiner
    (p : ℕ) [Fact p.Prime] :
    PowerSeries (padicLocalField p).valuationSubring

theorem

padicMultiplicativeToStandardIntertwiner_hasLinearTerm

L221 ↗

LubinTate.padicMultiplicativeToStandardIntertwiner_hasLinearTerm

Documentation

The multiplicative-to-standard intertwiner also has linear coefficient 1 and no constant term.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · full declaration

theorem padicMultiplicativeToStandardIntertwiner_hasLinearTerm
    (p : ℕ) [Fact p.Prime] :
    HasLinearTerm (padicMultiplicativeToStandardIntertwiner p)
      (fun _ : Unit =>
        (1 : (padicLocalField p).valuationSubring)) :=
  recursiveIntertwiner_hasLinearTerm
    (padicMultiplicativeLubinTateSeries_isUniformizer p)
    (standardLubinTateSeries
      (padicMultiplicativeLubinTateSeries_isUniformizer p))
    (padicMultiplicativeLubinTateSeries p)
    (fun _ : Unit => 1)

theorem

padicMultiplicativeToStandardIntertwiner_intertwines

L235 ↗

LubinTate.padicMultiplicativeToStandardIntertwiner_intertwines

Documentation

The inverse-direction canonical series satisfies its literal same-uniformizer equation.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicMultiplicativeToStandardIntertwiner_intertwines
    (p : ℕ) [Fact p.Prime] :
    Intertwines
      (standardLubinTateSeries
        (padicMultiplicativeLubinTateSeries_isUniformizer p))
      (padicMultiplicativeLubinTateSeries p)
      (padicMultiplicativeToStandardIntertwiner p)

theorem

padicMultiplicativeToStandardIntertwiner_functionalEquation

L250 ↗

LubinTate.padicMultiplicativeToStandardIntertwiner_functionalEquation

Documentation

One-variable form of the inverse-direction intertwining equation.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicMultiplicativeToStandardIntertwiner_functionalEquation
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.subst
        (padicMultiplicativeToStandardIntertwiner p)
        (standardLubinTateSeries
          (padicMultiplicativeLubinTateSeries_isUniformizer p)).toPowerSeries =
      PowerSeries.subst
        (padicMultiplicativeLubinTateSeries p).toPowerSeries
        (padicMultiplicativeToStandardIntertwiner p)

theorem

padicMultiplicativeToStandardIntertwiner_hasSubst

L284 ↗

LubinTate.padicMultiplicativeToStandardIntertwiner_hasSubst

Documentation

The inverse-direction intertwiner admits formal substitution.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicMultiplicativeToStandardIntertwiner_hasSubst
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.HasSubst
      (padicMultiplicativeToStandardIntertwiner p)

theorem

padicStandardToMultiplicativeIntertwiner_subst_reverse

L292 ↗

LubinTate.padicStandardToMultiplicativeIntertwiner_subst_reverse

Documentation

Composing the standard-to-multiplicative comparison after its reverse is the identity on the multiplicative coordinate.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicStandardToMultiplicativeIntertwiner_subst_reverse
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.subst
        (padicMultiplicativeToStandardIntertwiner p)
        (padicStandardToMultiplicativeIntertwiner p) =
      PowerSeries.X

theorem

padicMultiplicativeToStandardIntertwiner_subst_reverse

L338 ↗

LubinTate.padicMultiplicativeToStandardIntertwiner_subst_reverse

Documentation

Composing the reverse comparison after the standard-to-multiplicative series is the identity on the standard coordinate.

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open SameUniformizer

Lean source · statement

theorem padicMultiplicativeToStandardIntertwiner_subst_reverse
    (p : ℕ) [Fact p.Prime] :
    PowerSeries.subst
        (padicStandardToMultiplicativeIntertwiner p)
        (padicMultiplicativeToStandardIntertwiner p) =
      PowerSeries.X

Module documentation

Comparing the standard and multiplicative Lubin--Tate series over ℚ_p

Declarations

Comparing the standard and multiplicative Lubin--Tate series over `ℚ_p`