Module

ChangedCompletedPrimitiveAction.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ChangedCompletedPrimitiveAction

38 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: primitive action for the changed completed level

The theta relation in the completed theta-intertwining theorem uses the source parameter u⁻¹T. We first prove, genuinely by Eisenstein over (AlgebraicClosure κ)[[T]], that its primitive polynomial stays irreducible over the completed maximal-unramified Laurent field. We then enumerate its roots by source Lubin--Tate unit brackets and show that every such primitive point generates the splitting field.

The theta unit u and a source Lubin--Tate bracket unit a are deliberately kept as distinct parameters. Repository index n is division level n + 1.

Imports5

Mathlib.RingTheory.Adjoin.PowerBasis
Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ChangedCompletedLevel
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedPrimitiveIrreducible
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.FiniteParameters

Imported by4

instance

equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra

L44 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)

def

equalCharacteristicChangedCompletedSourceUnit

L52 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedSourceUnit

Documentation

The image of the source unit u⁻¹ in (AlgebraicClosure κ)[[T]].

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedSourceUnit
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) :
    (AlgebraicClosure F.residueField)⟦X⟧ˣ

def

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial

L62 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial

Documentation

The integral primitive polynomial for source parameter u⁻¹T, after coefficientwise extension to (AlgebraicClosure κ)[[T]].

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedIntegralPrimitivePolynomial
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Polynomial (AlgebraicClosure F.residueField)⟦X⟧

theorem

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_monic

L71 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_monic

Documentation

The changed integral primitive polynomial remains monic after scalar extension.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedIntegralPrimitivePolynomial F u n).Monic

theorem

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_natDegree

L78 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_natDegree

Documentation

The completed integral primitive polynomial has degree (q - 1) * q ^ n.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedIntegralPrimitivePolynomial F u n).natDegree =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

theorem

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_map

L89 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_map

Documentation

Passage from the changed integral polynomial to Laurent series agrees with the completed coefficientwise base change.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_map
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedIntegralPrimitivePolynomial F u n).map
        (algebraMap (AlgebraicClosure F.residueField)⟦X⟧
          (equalCharacteristicCompletedUnramifiedField F.residueField)) =
      equalCharacteristicChangedCompletedPrimitivePolynomial F u n

theorem

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_map_constantCoeff

L103 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_map_constantCoeff

Documentation

Modulo T, the completed changed primitive polynomial is its single leading monomial.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_map_constantCoeff
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedIntegralPrimitivePolynomial F u n).map
        (PowerSeries.constantCoeff
          (R := AlgebraicClosure F.residueField)) =
      Polynomial.X ^
        ((Nat.card F.residueField - 1) * Nat.card F.residueField ^ n)

theorem

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_coeff_zero

L129 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_coeff_zero

Documentation

The constant coefficient is the mapped unit times T, rather than merely T; this is the point at which the source u⁻¹T matters.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_coeff_zero
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedIntegralPrimitivePolynomial F u n).coeff 0 =
      (equalCharacteristicChangedCompletedSourceUnit F u :
        (AlgebraicClosure F.residueField)⟦X⟧) * PowerSeries.X

theorem

equalCharacteristicChangedCompletedIntegralUniformizer_notMem_span_X_sq

L140 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralUniformizer_notMem_span_X_sq

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralUniformizer_notMem_span_X_sq
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedCompletedSourceUnit F u :
        (AlgebraicClosure F.residueField)⟦X⟧) * PowerSeries.X ∉
      (Ideal.span
        ({PowerSeries.X} :
          Set (AlgebraicClosure F.residueField)⟦X⟧)) ^ 2

theorem

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_isEisensteinAt

L167 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_isEisensteinAt

Documentation

The completed integral source polynomial is genuinely Eisenstein at (T).

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_isEisensteinAt
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedIntegralPrimitivePolynomial F u n).IsEisensteinAt
      (Ideal.span
        ({PowerSeries.X} :
          Set (AlgebraicClosure F.residueField)⟦X⟧))

theorem

equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_irreducible

L201 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_irreducible

Documentation

The completed integral primitive polynomial is irreducible by Eisenstein's criterion.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedIntegralPrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Irreducible
      (equalCharacteristicChangedCompletedIntegralPrimitivePolynomial F u n)

theorem

equalCharacteristicChangedCompletedPrimitivePolynomial_irreducible

L219 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial_irreducible

Documentation

The source primitive polynomial remains irreducible over the completed maximal-unramified Laurent field.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Irreducible (equalCharacteristicChangedCompletedPrimitivePolynomial F u n)

def

equalCharacteristicChangedCompletedLevelBaseHom

L234 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelBaseHom

Documentation

The coefficientwise Laurent base map into the changed completed level.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedLevelBaseHom
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    F.residueField⸨X⸩ →+*
      equalCharacteristicChangedCompletedLevelField F u n

def

equalCharacteristicChangedCompletedLevelResidueHom

L245 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelResidueHom

Documentation

The residue-field coefficient map into the changed completed level.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedLevelResidueHom
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    F.residueField →+*
      equalCharacteristicChangedCompletedLevelField F u n

theorem

equalCharacteristicChangedCompletedLevelBaseHom_sourceUniformizer

L254 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedLevelBaseHom_sourceUniformizer

Documentation

The completed base map sends the changed source uniformizer to the level uniformizer.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedLevelBaseHom_sourceUniformizer
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedLevelBaseHom F u n
        (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u)) =
      equalCharacteristicChangedCompletedLevelUniformizer F u n

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_ne_zero

L264 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_ne_zero

Documentation

The chosen changed completed primitive point is nonzero.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_ne_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedPrimitiveRoot F u n ≠ 0

def

equalCharacteristicChangedCompletedUnitRoot

L278 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitRoot

Documentation

The source LT bracket image attached to a bracket unit a. The theta unit is the separate parameter u.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedUnitRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedCompletedLevelField F u n

theorem

equalCharacteristicChangedActionPiPolynomial_eval₂

L290 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedActionPiPolynomial_eval₂

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedActionPiPolynomial_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (f : F.residueField⸨X⸩ →+* A) (x : A) :
    Polynomial.eval₂ f x
        (equalCharacteristicChangedPiPolynomial F
          (equalCharacteristicThetaSourceUnit u)) =
      equalCharacteristicLubinTateAmbientPiEnd F
        (f (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u))) x

theorem

equalCharacteristicChangedActionPiPolynomialIterate_eval₂

L305 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedActionPiPolynomialIterate_eval₂

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedActionPiPolynomialIterate_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (f : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ f x
        (equalCharacteristicChangedPiPolynomialIterate F
          (equalCharacteristicThetaSourceUnit u) n) =
      equalCharacteristicLubinTateAmbientPiIterate F
        (f (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u))) n x

theorem

equalCharacteristicChangedActionPrimitivePolynomial_eval₂

L346 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedActionPrimitivePolynomial_eval₂

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedActionPrimitivePolynomial_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (f : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ f x
        (equalCharacteristicChangedPrimitivePolynomial F
          (equalCharacteristicThetaSourceUnit u) n) =
      equalCharacteristicLubinTateAmbientPiIterate F
          (f (equalCharacteristicChangedLaurentUniformizer F
            (equalCharacteristicThetaSourceUnit u))) n x ^
          (Nat.card F.residueField - 1) +
        f (equalCharacteristicChangedLaurentUniformizer F
          (equalCharacteristicThetaSourceUnit u))

theorem

equalCharacteristicChangedCompletedUnitRoot_isRoot

L368 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitRoot_isRoot

Documentation

Every source LT unit bracket of the chosen point is again a root of the completed source primitive polynomial.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedUnitRoot_isRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (a : F.residueField⟦X⟧ˣ) :
    ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicChangedCompletedLevelField F u n))).IsRoot
      (equalCharacteristicChangedCompletedUnitRoot F u n a)

theorem

equalCharacteristicChangedCompletedAmbientBracket_mem_adjoin

L425 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedAmbientBracket_mem_adjoin

Documentation

A source LT bracket is a polynomial expression in its input over the completed-unramified base.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedAmbientBracket_mem_adjoin
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n m : ℕ)
    (a : F.residueField⟦X⟧)
    (z : equalCharacteristicChangedCompletedLevelField F u n) :
    equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicChangedCompletedLevelResidueHom F u n)
        (equalCharacteristicChangedCompletedLevelUniformizer F u n) m a z ∈
      Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({z} : Set (equalCharacteristicChangedCompletedLevelField F u n))

def

equalCharacteristicChangedCompletedUnitParameterRoot

L465 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitParameterRoot

Documentation

The visible source unit parameter root.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedUnitParameterRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicChangedCompletedLevelField F u n

theorem

equalCharacteristicChangedCompletedUnitParameterRoot_injective

L475 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitParameterRoot_injective

Documentation

Distinct visible source unit parameters give distinct roots.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedUnitParameterRoot_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Function.Injective
      (equalCharacteristicChangedCompletedUnitParameterRoot F u n)

theorem

equalCharacteristicChangedCompletedUnitParameterRoot_isRoot

L493 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitParameterRoot_isRoot

Documentation

Each unit parameter produces a root of the changed completed primitive polynomial.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedUnitParameterRoot_isRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicChangedCompletedLevelField F u n))).IsRoot
      (equalCharacteristicChangedCompletedUnitParameterRoot F u n a)

theorem

equalCharacteristicChangedCompletedPrimitivePolynomial_separable

L507 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePolynomial_separable

Documentation

The completed source primitive polynomial is separable.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitivePolynomial_separable
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedPrimitivePolynomial F u n).Separable

def

equalCharacteristicChangedCompletedUnitParameterRootSet

L515 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitParameterRootSet

Documentation

A visible source unit parameter as an element of the full root set.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedUnitParameterRootSet
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    (equalCharacteristicChangedCompletedPrimitivePolynomial F u n).rootSet
      (equalCharacteristicChangedCompletedLevelField F u n)

theorem

equalCharacteristicChangedCompletedUnitParameterRootSet_injective

L530 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitParameterRootSet_injective

Documentation

Distinct unit parameters give distinct completed primitive roots.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedUnitParameterRootSet_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Function.Injective
      (equalCharacteristicChangedCompletedUnitParameterRootSet F u n)

theorem

equalCharacteristicChangedCompletedPrimitiveRootSet_natCard

L542 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRootSet_natCard

Documentation

The completed changed primitive polynomial has the expected number of roots in its splitting field.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRootSet_natCard
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Nat.card
        ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).rootSet
          (equalCharacteristicChangedCompletedLevelField F u n)) =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

theorem

equalCharacteristicChangedCompletedUnitParameterRootSet_bijective

L555 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitParameterRootSet_bijective

Documentation

Visible source LT unit parameters enumerate every primitive root.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedUnitParameterRootSet_bijective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Function.Bijective
      (equalCharacteristicChangedCompletedUnitParameterRootSet F u n)

theorem

equalCharacteristicChangedCompletedUnitParameterRoot_mem_adjoin

L570 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitParameterRoot_mem_adjoin

Documentation

Every visible parameter root is a source bracket polynomial in the chosen primitive point.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedUnitParameterRoot_mem_adjoin
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicChangedCompletedUnitParameterRoot F u n a ∈
      Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicChangedCompletedPrimitiveRoot F u n} :
          Set (equalCharacteristicChangedCompletedLevelField F u n))

theorem

equalCharacteristicChangedCompletedPrimitiveRootSet_subset_adjoin

L613 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRootSet_subset_adjoin

Documentation

Every root lies in the subfield generated by the chosen primitive point.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRootSet_subset_adjoin
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ((equalCharacteristicChangedCompletedPrimitivePolynomial F u n).rootSet
        (equalCharacteristicChangedCompletedLevelField F u n) :
      Set (equalCharacteristicChangedCompletedLevelField F u n)) ⊆
      Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicChangedCompletedPrimitiveRoot F u n} :
          Set (equalCharacteristicChangedCompletedLevelField F u n))

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_adjoin_eq_top

L638 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_adjoin_eq_top

Documentation

The chosen primitive source point generates its completed splitting field.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_adjoin_eq_top
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicChangedCompletedPrimitiveRoot F u n} :
          Set (equalCharacteristicChangedCompletedLevelField F u n)) = ⊤

theorem

equalCharacteristicChangedCompletedUnitRoot_adjoin_eq_top

L663 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedUnitRoot_adjoin_eq_top

Documentation

Every source LT unit bracket of the primitive point is itself a primitive generator of the completed level field.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedUnitRoot_adjoin_eq_top
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (a : F.residueField⟦X⟧ˣ) :
    Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicChangedCompletedUnitRoot F u n a} :
          Set (equalCharacteristicChangedCompletedLevelField F u n)) = ⊤

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_isIntegral

L722 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_isIntegral

Documentation

The chosen changed primitive point is integral over the completed maximal-unramified base.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_isIntegral
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsIntegral
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedPrimitiveRoot F u n)

theorem

equalCharacteristicChangedCompletedPrimitiveRoot_minpoly

L734 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitiveRoot_minpoly

Documentation

The completed source primitive polynomial is the minimal polynomial of the chosen primitive point.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitiveRoot_minpoly
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    minpoly (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicChangedCompletedPrimitiveRoot F u n) =
      equalCharacteristicChangedCompletedPrimitivePolynomial F u n

def

equalCharacteristicChangedCompletedPrimitivePowerBasis

L752 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePowerBasis

Documentation

The power basis generated by the completed primitive source point.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicChangedCompletedPrimitivePowerBasis
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    PowerBasis
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicChangedCompletedLevelField F u n)

theorem

equalCharacteristicChangedCompletedPrimitivePowerBasis_gen

L765 ↗

LubinTate.EqualCharacteristic.equalCharacteristicChangedCompletedPrimitivePowerBasis_gen

Documentation

The completed primitive power basis has the distinguished root as generator.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicChangedCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicChangedCompletedPrimitivePowerBasis_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    (equalCharacteristicChangedCompletedPrimitivePowerBasis F u n).gen =
      equalCharacteristicChangedCompletedPrimitiveRoot F u n

Module documentation

The completed theta-intertwining theorem: primitive action for the changed completed level

Declarations