Module

StandardFormalGroup.lean

Nyll.ClassFieldTheory.LubinTate.FormalModule.StandardFormalGroup

40 declarations indexed from sourceView source ↗

Module documentation

The standard Lubin--Tate formal group

The recursive same-uniformizer intertwiner applied to the standard Lubin--Tate series produces the formal group law and all of its scalar endomorphisms. The structural identities are proved from the uniqueness of an intertwiner with prescribed linear term.

This file also records the substitution closure properties of SameUniformizer.Intertwines. They are useful independently of the standard series: intertwiners remain intertwiners after a change of variables, after substituting an intertwining family, and after one-variable power-series composition.

Imports3

Nyll.ClassFieldTheory.LubinTate.FormalModule.RecursiveIntertwiner
Nyll.ClassFieldTheory.LubinTate.FormalModule.StandardSeries
Mathlib.RingTheory.FormalGroup.Basic

Imported by5

theorem

coeff_eq_linearForm

L53 ↗

LubinTate.SameUniformizer.HasLinearTerm.coeff_eq_linearForm

Documentation

In total degree less than two, a series with prescribed linear term agrees coefficientwise with that linear form.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section LinearTerms
variable {R : Type*} [CommRing R]
variable {σ : Type w} [Fintype σ]
variable {τ : Type w'} [Fintype τ]
namespace HasLinearTerm

Lean source · statement

theorem coeff_eq_linearForm
    {H : MvPowerSeries σ R} {L : σ → R}
    (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : d.degree < 2) :
    MvPowerSeries.coeff d H =
      MvPowerSeries.coeff d (linearForm L)

theorem

coeff_single

L67 ↗

LubinTate.SameUniformizer.HasLinearTerm.coeff_single

Documentation

The coefficient of X_i is the prescribed coefficient L_i.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section LinearTerms
variable {R : Type*} [CommRing R]
variable {σ : Type w} [Fintype σ]
variable {τ : Type w'} [Fintype τ]
namespace HasLinearTerm

Lean source · statement

theorem coeff_single
    {H : MvPowerSeries σ R} {L : σ → R}
    (hH : HasLinearTerm H L) (i : σ) :
    MvPowerSeries.coeff (Finsupp.single i 1) H = L i

theorem

linearForm_weighted_sum

L75 ↗

LubinTate.SameUniformizer.HasLinearTerm.linearForm_weighted_sum

Source context 14 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section LinearTerms
variable {R : Type*} [CommRing R]
variable {σ : Type w} [Fintype σ]
variable {τ : Type w'} [Fintype τ]
namespace HasLinearTerm

Lean source · full declaration

theorem linearForm_weighted_sum
    (L : σ → R) (M : σ → τ → R) :
    (∑ i, MvPowerSeries.C (L i) * linearForm (M i)) =
      linearForm (fun j => ∑ i, L i * M i j) := by
  classical
  apply MvPowerSeries.ext
  intro d
  simp only [linearForm, map_sum, MvPowerSeries.coeff_C_mul,
    Finset.mul_sum, Finset.sum_mul]
  rw [Finset.sum_comm]
  simp only [mul_assoc]

theorem

subst

L89 ↗

LubinTate.SameUniformizer.HasLinearTerm.subst

Documentation

Substituting series with prescribed linear terms composes their linear coefficient matrices.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section LinearTerms
variable {R : Type*} [CommRing R]
variable {σ : Type w} [Fintype σ]
variable {τ : Type w'} [Fintype τ]
namespace HasLinearTerm

Lean source · full declaration

theorem subst
    {H : MvPowerSeries σ R} {L : σ → R}
    (hH : HasLinearTerm H L)
    {G : σ → MvPowerSeries τ R} {M : σ → τ → R}
    (hG : ∀ i, HasLinearTerm (G i) (M i)) :
    HasLinearTerm (MvPowerSeries.subst G H)
      (fun j => ∑ i, L i * M i j) := by
  have hGsubst : MvPowerSeries.HasSubst G :=
    MvPowerSeries.hasSubst_of_constantCoeff_zero
      (fun i => (hG i).constantCoeff_eq_zero)
  have hGorder : ∀ i, (1 : ℕ∞) ≤ (G i).order :=
    fun i =>
      MvPowerSeries.one_le_order_iff_constCoeff_eq_zero.mpr
        (hG i).constantCoeff_eq_zero
  have hinf : (1 : ℕ∞) ≤ ⨅ i, (G i).order :=
    le_iInf hGorder
  have houter :
      (2 : ℕ∞) ≤
        (MvPowerSeries.subst G (H - linearForm L)).order := by
    refine
      (show
        (2 : ℕ∞) ≤
          (⨅ i, (G i).order) * (H - linearForm L).order by
        calc
          (2 : ℕ∞) = 1 * 2 := by norm_num
          _ ≤ (⨅ i, (G i).order) *
              (H - linearForm L).order :=
            mul_le_mul hinf hH (by simp) (by simp)).trans
        (MvPowerSeries.le_order_subst hGsubst
          (H - linearForm L))
  have hsubstLinear :
      MvPowerSeries.subst G (linearForm L) =
        ∑ i, MvPowerSeries.C (L i) * G i := by
    classical
    rw [linearForm,
      ← MvPowerSeries.substAlgHom_apply hGsubst, map_sum]
    apply Finset.sum_congr rfl
    intro i _
    rw [map_mul, MvPowerSeries.substAlgHom_X]
    simp
  have hlinearIdentity :
      MvPowerSeries.subst G (linearForm L) -
          linearForm (fun j => ∑ i, L i * M i j) =
        ∑ i, MvPowerSeries.C (L i) *
          (G i - linearForm (M i)) := by
    rw [hsubstLinear, ← linearForm_weighted_sum L M,
      ← Finset.sum_sub_distrib]
    apply Finset.sum_congr rfl
    intro i _
    ring
  have hlinear :
      (2 : ℕ∞) ≤
        (MvPowerSeries.subst G (linearForm L) -
          linearForm (fun j => ∑ i, L i * M i j)).order := by
    rw [hlinearIdentity]
    apply MvPowerSeries.nat_le_order
    intro d hd
    rw [map_sum]
    apply Finset.sum_eq_zero
    intro i _
    rw [MvPowerSeries.coeff_C_mul]
    have hd' : (d.degree : ℕ∞) < (2 : ℕ∞) := by
      exact_mod_cast hd
    rw [MvPowerSeries.coeff_of_lt_order
      (hd'.trans_le (hG i)), mul_zero]
  rw [HasLinearTerm]
  have hdecompose :
      MvPowerSeries.subst G H -
          linearForm (fun j => ∑ i, L i * M i j) =
        MvPowerSeries.subst G (H - linearForm L) +
          (MvPowerSeries.subst G (linearForm L) -
            linearForm (fun j => ∑ i, L i * M i j)) := by
    rw [MvPowerSeries.subst_sub hGsubst]
    ring
  rw [hdecompose]
  exact
    (le_min houter hlinear).trans
      MvPowerSeries.min_order_le_add

theorem

linearForm_basis

L170 ↗

LubinTate.SameUniformizer.linearForm_basis

Source context 13 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section LinearTerms
variable {R : Type*} [CommRing R]
variable {σ : Type w} [Fintype σ]
variable {τ : Type w'} [Fintype τ]

Lean source · full declaration

theorem linearForm_basis (i : σ) :
    linearForm (R := R)
        (fun j : σ => if j = i then (1 : R) else 0) =
      (MvPowerSeries.X i : MvPowerSeries σ R) := by
  classical
  simp [linearForm]

theorem

hasLinearTerm_X

L178 ↗

LubinTate.SameUniformizer.hasLinearTerm_X

Documentation

A variable has the corresponding standard-basis linear term.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section LinearTerms
variable {R : Type*} [CommRing R]
variable {σ : Type w} [Fintype σ]
variable {τ : Type w'} [Fintype τ]

Lean source · full declaration

theorem hasLinearTerm_X (i : σ) :
    HasLinearTerm (MvPowerSeries.X i : MvPowerSeries σ R)
      (fun j => if j = i then (1 : R) else 0) := by
  rw [HasLinearTerm, linearForm_basis i, sub_self]
  simp

theorem

hasLinearTerm_zero

L185 ↗

LubinTate.SameUniformizer.hasLinearTerm_zero

Documentation

Zero has zero linear term.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section LinearTerms
variable {R : Type*} [CommRing R]
variable {σ : Type w} [Fintype σ]
variable {τ : Type w'} [Fintype τ]

Lean source · full declaration

theorem hasLinearTerm_zero :
    HasLinearTerm (0 : MvPowerSeries σ R) (fun _ => 0) := by
  simp [HasLinearTerm, linearForm]

theorem

subst_powerSeries_subst

L198 ↗

LubinTate.SameUniformizer.subst_powerSeries_subst

Documentation

Multivariable substitution commutes with substituting a multivariable series into a one-variable power series.

Source context 12 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section SubstitutionClosure
variable {σ : Type w}
variable {τ : Type w'}

Lean source · statement

theorem subst_powerSeries_subst
    {H : MvPowerSeries σ F.valuationSubring}
    (hH : PowerSeries.HasSubst H)
    {G : σ → MvPowerSeries τ F.valuationSubring}
    (hG : MvPowerSeries.HasSubst G)
    (f : PowerSeries F.valuationSubring) :
    MvPowerSeries.subst G (PowerSeries.subst H f) =
      PowerSeries.subst (MvPowerSeries.subst G H) f

theorem

subst_inVariable

L215 ↗

LubinTate.SameUniformizer.subst_inVariable

Documentation

Substituting a family into e(X_i) gives e evaluated at the corresponding member of that family.

Source context 12 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section SubstitutionClosure
variable {σ : Type w}
variable {τ : Type w'}

Lean source · statement

theorem subst_inVariable
    (e : LubinTateSeries F π)
    {G : σ → MvPowerSeries τ F.valuationSubring}
    (hG : MvPowerSeries.HasSubst G) (i : σ) :
    MvPowerSeries.subst G (inVariable e i) =
      PowerSeries.subst (G i) e.toPowerSeries

theorem

subst

L229 ↗

LubinTate.SameUniformizer.Intertwines.subst

Documentation

An intertwiner remains an intertwiner after substituting a family of intertwiners.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section SubstitutionClosure
variable {σ : Type w}
variable {τ : Type w'}
namespace Intertwines

Lean source · statement

theorem subst
    [Finite σ] [Finite τ]
    {e ebar ehat : LubinTateSeries F π}
    {H : MvPowerSeries σ F.valuationSubring}
    (hH : Intertwines e ebar H)
    (hHsubst : PowerSeries.HasSubst H)
    {G : σ → MvPowerSeries τ F.valuationSubring}
    (hGsubst : MvPowerSeries.HasSubst G)
    (hG : ∀ i, Intertwines ebar ehat (G i)) :
    Intertwines e ehat (MvPowerSeries.subst G H)

theorem

reindex

L275 ↗

LubinTate.SameUniformizer.Intertwines.reindex

Documentation

Reindexing variables preserves the intertwining equation.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section SubstitutionClosure
variable {σ : Type w}
variable {τ : Type w'}
namespace Intertwines

Lean source · full declaration

theorem reindex
    [Finite σ] [Finite τ]
    {e ebar : LubinTateSeries F π}
    {H : MvPowerSeries σ F.valuationSubring}
    (hH : Intertwines e ebar H)
    (hHsubst : PowerSeries.HasSubst H)
    (f : σ → τ) :
    Intertwines e ebar
      (MvPowerSeries.subst
        (fun i => MvPowerSeries.X (f i)) H) := by
  apply hH.subst hHsubst
    (MvPowerSeries.hasSubst_of_constantCoeff_zero
      (fun _ => by simp))
  intro i
  exact intertwines_X ebar (f i)

theorem

powerSeries_subst

L293 ↗

LubinTate.SameUniformizer.Intertwines.powerSeries_subst

Documentation

One-variable power-series composition is a special case of substitution by an intertwining family.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section SubstitutionClosure
variable {σ : Type w}
variable {τ : Type w'}
namespace Intertwines

Lean source · statement

theorem powerSeries_subst
    [Finite τ]
    {e ebar ehat : LubinTateSeries F π}
    {H : PowerSeries F.valuationSubring}
    (hH : Intertwines e ebar H)
    (hHsubst : PowerSeries.HasSubst H)
    {G : MvPowerSeries τ F.valuationSubring}
    (hG : Intertwines ebar ehat G)
    (hGsubst : PowerSeries.HasSubst G) :
    Intertwines e ehat (PowerSeries.subst G H)

theorem

intertwines_zero

L308 ↗

LubinTate.SameUniformizer.intertwines_zero

Documentation

Zero intertwines any two series with zero constant coefficient.

Source context 12 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section SubstitutionClosure
variable {σ : Type w}
variable {τ : Type w'}

Lean source · statement

theorem intertwines_zero
    [Finite σ]
    (e ebar : LubinTateSeries F π) :
    Intertwines e ebar
      (0 : MvPowerSeries σ F.valuationSubring)

abbrev

standardSeries

L333 ↗

LubinTate.SameUniformizer.standardSeries

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

abbrev standardSeries :
    LubinTateSeries F π

def

standardFormalGroupPowerSeries

L339 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries

Documentation

The unique two-variable series with linear term X + Y commuting with the standard Lubin--Tate series.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

def standardFormalGroupPowerSeries :
    MvPowerSeries (Fin 2) F.valuationSubring

theorem

standardFormalGroupPowerSeries_hasLinearTerm

L345 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_hasLinearTerm

Documentation

The standard formal-group series has linear term X + Y.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

theorem standardFormalGroupPowerSeries_hasLinearTerm :
    HasLinearTerm (standardFormalGroupPowerSeries hπ)
      (fun _ : Fin 2 => 1) :=
  recursiveIntertwiner_hasLinearTerm hπ
    (standardSeries hπ) (standardSeries hπ) (fun _ => 1)

theorem

standardFormalGroupPowerSeries_intertwines

L353 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_intertwines

Documentation

The standard formal-group series commutes with the standard Lubin--Tate series.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardFormalGroupPowerSeries_intertwines :
    Intertwines (standardSeries hπ) (standardSeries hπ)
      (standardFormalGroupPowerSeries hπ)

theorem

existsUnique_standardFormalGroupPowerSeries

L361 ↗

LubinTate.SameUniformizer.existsUnique_standardFormalGroupPowerSeries

Documentation

The standard formal-group series is the unique two-variable intertwiner with linear term X + Y.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

theorem existsUnique_standardFormalGroupPowerSeries :
    ∃! H : MvPowerSeries (Fin 2) F.valuationSubring,
      HasLinearTerm H (fun _ : Fin 2 => 1) ∧
        Intertwines (standardSeries hπ) (standardSeries hπ) H :=
  existsUnique_intertwiner hπ
    (standardSeries hπ) (standardSeries hπ) (fun _ => 1)

theorem

standardFormalGroupPowerSeries_subst_hasLinearTerm

L368 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_subst_hasLinearTerm

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

theorem standardFormalGroupPowerSeries_subst_hasLinearTerm
    {τ : Type w} [Fintype τ]
    {G₀ G₁ : MvPowerSeries τ F.valuationSubring}
    {M₀ M₁ : τ → F.valuationSubring}
    (hG₀ : HasLinearTerm G₀ M₀)
    (hG₁ : HasLinearTerm G₁ M₁) :
    HasLinearTerm
      (MvPowerSeries.subst ![G₀, G₁]
        (standardFormalGroupPowerSeries hπ))
      (fun j => M₀ j + M₁ j) := by
  have h :=
    (standardFormalGroupPowerSeries_hasLinearTerm hπ).subst
      (G := ![G₀, G₁]) (M := ![M₀, M₁])
      (by
        intro i
        fin_cases i
        · exact hG₀
        · exact hG₁)
  simpa [Fin.sum_univ_two] using h

theorem

standardFormalGroupPowerSeries_subst_intertwines

L388 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_subst_intertwines

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardFormalGroupPowerSeries_subst_intertwines
    {τ : Type w} [Fintype τ]
    {G₀ G₁ : MvPowerSeries τ F.valuationSubring}
    {M₀ M₁ : τ → F.valuationSubring}
    (hG₀ : HasLinearTerm G₀ M₀)
    (hG₁ : HasLinearTerm G₁ M₁)
    (hI₀ : Intertwines (standardSeries hπ)
      (standardSeries hπ) G₀)
    (hI₁ : Intertwines (standardSeries hπ)
      (standardSeries hπ) G₁) :
    Intertwines (standardSeries hπ) (standardSeries hπ)
      (MvPowerSeries.subst ![G₀, G₁]
        (standardFormalGroupPowerSeries hπ))

theorem

standardFormalGroupPowerSeries_subst_X_zero

L416 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_subst_X_zero

Documentation

The left identity law, proved by uniqueness of the linear-term-one intertwiner.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardFormalGroupPowerSeries_subst_X_zero :
    MvPowerSeries.subst
        ![(MvPowerSeries.X () :
            PowerSeries F.valuationSubring), 0]
        (standardFormalGroupPowerSeries hπ) =
      (MvPowerSeries.X () :
        PowerSeries F.valuationSubring)

theorem

standardFormalGroupPowerSeries_subst_zero_X

L460 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_subst_zero_X

Documentation

The right identity law, proved by uniqueness.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardFormalGroupPowerSeries_subst_zero_X :
    MvPowerSeries.subst
        ![0, (MvPowerSeries.X () :
            PowerSeries F.valuationSubring)]
        (standardFormalGroupPowerSeries hπ) =
      (MvPowerSeries.X () :
        PowerSeries F.valuationSubring)

theorem

standardFormalGroupPowerSeries_assoc

L505 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_assoc

Documentation

Associativity of the standard formal-group series, proved by comparing the two three-variable intertwiners with linear term X + Y + Z.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardFormalGroupPowerSeries_assoc :
    MvPowerSeries.subst
        ![
          MvPowerSeries.subst
            ![
              (MvPowerSeries.X 0 :
                MvPowerSeries (Fin 3) F.valuationSubring),
              MvPowerSeries.X 1]
            (standardFormalGroupPowerSeries hπ),
          MvPowerSeries.X 2]
        (standardFormalGroupPowerSeries hπ) =
      MvPowerSeries.subst
        ![
          (MvPowerSeries.X 0 :
            MvPowerSeries (Fin 3) F.valuationSubring),
          MvPowerSeries.subst
            ![MvPowerSeries.X 1, MvPowerSeries.X 2]
            (standardFormalGroupPowerSeries hπ)]
        (standardFormalGroupPowerSeries hπ)

theorem

standardFormalGroupPowerSeries_comm

L633 ↗

LubinTate.SameUniformizer.standardFormalGroupPowerSeries_comm

Documentation

Commutativity of the standard formal-group series, proved by uniqueness.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardFormalGroupPowerSeries_comm :
    standardFormalGroupPowerSeries hπ =
      MvPowerSeries.subst
        ![
          (MvPowerSeries.X 1 :
            MvPowerSeries (Fin 2) F.valuationSubring),
          MvPowerSeries.X 0]
        (standardFormalGroupPowerSeries hπ)

def

standardFormalGroup

L681 ↗

LubinTate.SameUniformizer.standardFormalGroup

Documentation

The formal group law attached to the standard Lubin--Tate series.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

def standardFormalGroup :
    FormalGroup F.valuationSubring where
  toPowerSeries := standardFormalGroupPowerSeries hπ
  zero_constantCoeff :=
    (standardFormalGroupPowerSeries_hasLinearTerm
      hπ).constantCoeff_eq_zero
  lin_coeff_X :=
    (standardFormalGroupPowerSeries_hasLinearTerm
      hπ).coeff_single 0
  lin_coeff_Y :=
    (standardFormalGroupPowerSeries_hasLinearTerm
      hπ).coeff_single 1
  assoc := standardFormalGroupPowerSeries_assoc hπ

instance

standardFormalGroup_isComm

L696 ↗

LubinTate.SameUniformizer.standardFormalGroup_isComm

Documentation

The standard Lubin--Tate formal group is commutative.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardFormalGroup
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

instance standardFormalGroup_isComm :
    (standardFormalGroup hπ).IsComm where
  comm := standardFormalGroupPowerSeries_comm hπ

abbrev

standardSeries'

L707 ↗

LubinTate.SameUniformizer.standardSeries'

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

abbrev standardSeries' :
    LubinTateSeries F π

def

standardLubinTateEndomorphism

L713 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism

Documentation

The one-variable standard Lubin--Tate endomorphism with linear coefficient a.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

def standardLubinTateEndomorphism
    (a : F.valuationSubring) :
    PowerSeries F.valuationSubring

theorem

standardLubinTateEndomorphism_hasLinearTerm

L720 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_hasLinearTerm

Documentation

The endomorphism [a] has linear coefficient a.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

theorem standardLubinTateEndomorphism_hasLinearTerm
    (a : F.valuationSubring) :
    HasLinearTerm (standardLubinTateEndomorphism hπ a)
      (fun _ : Unit => a) :=
  recursiveIntertwiner_hasLinearTerm hπ
    (standardSeries' hπ) (standardSeries' hπ)
    (fun _ : Unit => a)

theorem

standardLubinTateEndomorphism_intertwines

L730 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_intertwines

Documentation

The endomorphism [a] commutes with the standard Lubin--Tate series.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphism_intertwines
    (a : F.valuationSubring) :
    Intertwines (standardSeries' hπ) (standardSeries' hπ)
      (standardLubinTateEndomorphism hπ a)

theorem

existsUnique_standardLubinTateEndomorphism

L740 ↗

LubinTate.SameUniformizer.existsUnique_standardLubinTateEndomorphism

Documentation

[a] is the unique one-variable intertwiner with linear coefficient a.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

theorem existsUnique_standardLubinTateEndomorphism
    (a : F.valuationSubring) :
    ∃! f : PowerSeries F.valuationSubring,
      HasLinearTerm f (fun _ : Unit => a) ∧
        Intertwines (standardSeries' hπ) (standardSeries' hπ) f :=
  existsUnique_intertwiner hπ
    (standardSeries' hπ) (standardSeries' hπ)
    (fun _ : Unit => a)

theorem

standardLubinTateEndomorphism_coeff_one

L751 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_coeff_one

Documentation

The coefficient of X in [a] is a.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphism_coeff_one
    (a : F.valuationSubring) :
    PowerSeries.coeff 1
      (standardLubinTateEndomorphism hπ a) = a

theorem

standardLubinTateEndomorphism_one

L760 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_one

Documentation

The scalar 1 acts by the identity series.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphism_one :
    standardLubinTateEndomorphism hπ 1 =
      PowerSeries.X

theorem

standardLubinTateEndomorphism_zero

L779 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_zero

Documentation

The scalar 0 acts by the zero series.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphism_zero :
    standardLubinTateEndomorphism hπ 0 = 0

theorem

standardLubinTateEndomorphism_add

L792 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_add

Documentation

Addition of scalars is addition in the standard formal group.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphism_add
    (a b : F.valuationSubring) :
    standardLubinTateEndomorphism hπ (a + b) =
      MvPowerSeries.subst
        ![
          standardLubinTateEndomorphism hπ a,
          standardLubinTateEndomorphism hπ b]
        (standardFormalGroupPowerSeries hπ)

theorem

standardLubinTateEndomorphism_mul

L831 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_mul

Documentation

Multiplication of scalars is composition of endomorphisms: [ab](X) = [a]([b](X)).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphism_mul
    (a b : F.valuationSubring) :
    standardLubinTateEndomorphism hπ (a * b) =
      PowerSeries.subst
        (standardLubinTateEndomorphism hπ b)
        (standardLubinTateEndomorphism hπ a)

def

standardLubinTateEndomorphismInVariable

L868 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphismInVariable

Documentation

The series [a](X_i) in a chosen variable.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

def standardLubinTateEndomorphismInVariable
    {σ : Type w} (a : F.valuationSubring) (i : σ) :
    MvPowerSeries σ F.valuationSubring

theorem

standardLubinTateEndomorphismInVariable_hasLinearTerm

L875 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphismInVariable_hasLinearTerm

Documentation

The linear term of [a](X_i) is a X_i.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · full declaration

theorem standardLubinTateEndomorphismInVariable_hasLinearTerm
    {σ : Type w} [Fintype σ]
    (a : F.valuationSubring) (i : σ) :
    HasLinearTerm
      (standardLubinTateEndomorphismInVariable hπ a i)
      (fun j => if j = i then a else 0) := by
  have h :=
    (standardLubinTateEndomorphism_hasLinearTerm hπ a).subst
      (G := fun _ : Unit =>
        (MvPowerSeries.X i :
          MvPowerSeries σ F.valuationSubring))
      (M := fun _ : Unit =>
        fun j : σ => if j = i then 1 else 0)
      (fun _ =>
        hasLinearTerm_X (R := F.valuationSubring) i)
  simpa [standardLubinTateEndomorphismInVariable,
    PowerSeries.subst_def] using h

theorem

standardLubinTateEndomorphismInVariable_intertwines

L894 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphismInVariable_intertwines

Documentation

The reindexed series [a](X_i) remains an intertwiner.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphismInVariable_intertwines
    {σ : Type w} [Finite σ]
    (a : F.valuationSubring) (i : σ) :
    Intertwines (standardSeries' hπ) (standardSeries' hπ)
      (standardLubinTateEndomorphismInVariable hπ a i)

theorem

standardLubinTateEndomorphism_map_formalGroup

L909 ↗

LubinTate.SameUniformizer.standardLubinTateEndomorphism_map_formalGroup

Documentation

The full scalar endomorphism identity [a](F(X,Y)) = F([a](X),[a](Y)).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
attribute [local instance] Classical.propDecidable
universe u v w w'
namespace LubinTate
namespace SameUniformizer
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
section StandardEndomorphisms
variable (hπ :
  F.toCompleteDVF.valuation.IsUniformizer (π : K))

Lean source · statement

theorem standardLubinTateEndomorphism_map_formalGroup
    (a : F.valuationSubring) :
    PowerSeries.subst
        (standardFormalGroupPowerSeries hπ)
        (standardLubinTateEndomorphism hπ a) =
      MvPowerSeries.subst
        ![
          standardLubinTateEndomorphismInVariable hπ a
            (0 : Fin 2),
          standardLubinTateEndomorphismInVariable hπ a
            (1 : Fin 2)]
        (standardFormalGroupPowerSeries hπ)

Module documentation

The standard Lubin--Tate formal group

Declarations