NYLL
Module

CompletedPrimitiveAction.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedPrimitiveAction
26 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: primitive division points in the completed level

The completed level used in the proof of the completed theta-intertwining theorem is the splitting field of the base-changed primitive division polynomial. This file records that its chosen root is genuinely primitive of level n + 1: it is killed by the next Lubin--Tate iterate, but not by the preceding one. These statements are the algebraic input for extending arithmetic Frobenius to the completed level.

Imports4
Imported by6

Declarations

instance

equalCharacteristicCompletedPrimitiveActionBaseAlgebra

L42 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveActionBaseAlgebra
Documentation

The coefficientwise Laurent-series algebra used by the completed unramified base. It is kept local so importing this file does not change global type-class search.

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 equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
def

equalCharacteristicCompletedLevelBaseHom

L49 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelBaseHom
Documentation

The coefficientwise Laurent base map into 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedLevelBaseHom
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.residueField⸨X⸩ →+*
      equalCharacteristicCompletedLevelField F n
def

equalCharacteristicCompletedLevelResidueHom

L60 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelResidueHom
Documentation

The residue-field coefficient map into the 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedLevelResidueHom
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.residueField →+* equalCharacteristicCompletedLevelField F n
theorem

equalCharacteristicCompletedLevelBaseHom_uniformizer

L68 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelBaseHom_uniformizer
Documentation

States the theorem equalCharacteristicCompletedLevelBaseHom_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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedLevelBaseHom_uniformizer
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicCompletedLevelBaseHom F n
        (equalCharacteristicLaurentUniformizer F) =
      equalCharacteristicCompletedLevelUniformizer F n
theorem

equalCharacteristicCompletedPrimitiveRoot_torsion

L79 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_torsion
Documentation

The chosen root in the completed splitting field is killed at level n + 1.

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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRoot_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicCompletedLevelUniformizer F n) (n + 1)
      (equalCharacteristicCompletedPrimitiveRoot F n)
theorem

equalCharacteristicCompletedPrimitiveRoot_not_torsion_pred

L106 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_not_torsion_pred
Documentation

The chosen completed root is not already killed at level 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRoot_not_torsion_pred
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ¬ IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicCompletedLevelUniformizer F n) n
      (equalCharacteristicCompletedPrimitiveRoot F n)
theorem

equalCharacteristicCompletedPrimitiveRoot_ne_zero

L127 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_ne_zero
Documentation

In particular, the chosen 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRoot_ne_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicCompletedPrimitiveRoot F n ≠ 0
def

equalCharacteristicCompletedUnitRoot

L141 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitRoot
Documentation

The bracket image of the completed primitive point attached to a power-series unit.

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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedUnitRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicCompletedLevelField F n
theorem

equalCharacteristicCompletedUnitRoot_isRoot

L154 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitRoot_isRoot
Documentation

Every unit bracket of the chosen completed point is again a root of the 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitRoot_isRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    ((equalCharacteristicCompletedPrimitivePolynomial F n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n))).IsRoot
      (equalCharacteristicCompletedUnitRoot F n a)
theorem

equalCharacteristicCompletedAmbientBracket_mem_adjoin

L210 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedAmbientBracket_mem_adjoin
Documentation

A truncated 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedAmbientBracket_mem_adjoin
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n m : ℕ) (a : F.residueField⟦X⟧)
    (z : equalCharacteristicCompletedLevelField F n) :
    equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicCompletedLevelResidueHom F n)
        (equalCharacteristicCompletedLevelUniformizer F n) m a z ∈
      Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({z} : Set (equalCharacteristicCompletedLevelField F n))
def

equalCharacteristicCompletedUnitParameterRoot

L250 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitParameterRoot
Documentation

The image of the completed primitive point attached to a visible unit parameter.

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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedUnitParameterRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicCompletedLevelField F n
theorem

equalCharacteristicCompletedUnitParameterRoot_injective

L260 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitParameterRoot_injective
Documentation

Distinct visible unit parameters give distinct completed primitive points.

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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitParameterRoot_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Injective (equalCharacteristicCompletedUnitParameterRoot F n)
theorem

equalCharacteristicCompletedUnitParameterRoot_isRoot

L278 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitParameterRoot_isRoot
Documentation

Every visible unit bracket of the chosen completed point is again a root of the 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitParameterRoot_isRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    ((equalCharacteristicCompletedPrimitivePolynomial F n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n))).IsRoot
      (equalCharacteristicCompletedUnitParameterRoot F n a)
theorem

equalCharacteristicCompletedPrimitivePolynomial_separable

L292 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_separable
Documentation

Base change to the completed maximal-unramified field preserves separability of the 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitivePolynomial_separable
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedPrimitivePolynomial F n).Separable
def

equalCharacteristicCompletedUnitParameterRootSet

L300 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitParameterRootSet
Documentation

A visible unit parameter, regarded as an element of the full root set in the 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedUnitParameterRootSet
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    (equalCharacteristicCompletedPrimitivePolynomial F n).rootSet
      (equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicCompletedUnitParameterRootSet_injective

L314 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitParameterRootSet_injective
Documentation

States the theorem equalCharacteristicCompletedUnitParameterRootSet_injective.

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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitParameterRootSet_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Injective (equalCharacteristicCompletedUnitParameterRootSet F n)
theorem

equalCharacteristicCompletedPrimitiveRootSet_natCard

L325 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRootSet_natCard
Documentation

The completed primitive polynomial has precisely 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRootSet_natCard
    (F : LocalField.{u, v} K) (n : ℕ) :
    Nat.card
        ((equalCharacteristicCompletedPrimitivePolynomial F n).rootSet
          (equalCharacteristicCompletedLevelField F n)) =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n
theorem

equalCharacteristicCompletedUnitParameterRootSet_bijective

L339 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitParameterRootSet_bijective
Documentation

Visible unit parameters enumerate every root after passage to 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitParameterRootSet_bijective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Bijective
      (equalCharacteristicCompletedUnitParameterRootSet F n)
theorem

equalCharacteristicCompletedUnitParameterRoot_mem_adjoin

L353 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitParameterRoot_mem_adjoin
Documentation

Every parameter root is a polynomial expression in the chosen completed primitive point, with coefficients in 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitParameterRoot_mem_adjoin
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicCompletedUnitParameterRoot F n a ∈
      Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicCompletedPrimitiveRoot F n} :
          Set (equalCharacteristicCompletedLevelField F n))
theorem

equalCharacteristicCompletedPrimitiveRootSet_subset_adjoin

L396 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRootSet_subset_adjoin
Documentation

All roots of the completed primitive polynomial lie in the field 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRootSet_subset_adjoin
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ((equalCharacteristicCompletedPrimitivePolynomial F n).rootSet
        (equalCharacteristicCompletedLevelField F n) :
      Set (equalCharacteristicCompletedLevelField F n)) ⊆
      Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicCompletedPrimitiveRoot F n} :
          Set (equalCharacteristicCompletedLevelField F n))
theorem

equalCharacteristicCompletedPrimitiveRoot_adjoin_eq_top

L421 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_adjoin_eq_top
Documentation

The chosen completed primitive point generates the 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRoot_adjoin_eq_top
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicCompletedPrimitiveRoot F n} :
          Set (equalCharacteristicCompletedLevelField F n)) = ⊤
theorem

equalCharacteristicCompletedUnitRoot_adjoin_eq_top

L446 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitRoot_adjoin_eq_top
Documentation

Every unit bracket of a primitive point is again 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitRoot_adjoin_eq_top
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    Algebra.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({equalCharacteristicCompletedUnitRoot F n a} :
          Set (equalCharacteristicCompletedLevelField F n)) = ⊤
theorem

equalCharacteristicCompletedPrimitiveRoot_isIntegral

L510 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_isIntegral
Documentation

The chosen completed primitive point is integral 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRoot_isIntegral
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsIntegral
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedPrimitiveRoot F n)
theorem

equalCharacteristicCompletedPrimitiveRoot_minpoly

L522 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveRoot_minpoly
Documentation

The completed 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitiveRoot_minpoly
    (F : LocalField.{u, v} K) (n : ℕ) :
    minpoly (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedPrimitiveRoot F n) =
      equalCharacteristicCompletedPrimitivePolynomial F n
def

equalCharacteristicCompletedPrimitivePowerBasis

L539 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePowerBasis
Documentation

The power basis generated by the completed primitive division 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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedPrimitivePowerBasis
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    PowerBasis
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicCompletedPrimitivePowerBasis_gen

L552 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePowerBasis_gen
Documentation

States the theorem equalCharacteristicCompletedPrimitivePowerBasis_gen.

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]
/-- The coefficientwise Laurent-series algebra used by the completed
unramified base.  It is kept local so importing this file does not change
global type-class search. -/
noncomputable local instance equalCharacteristicCompletedPrimitiveActionBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitivePowerBasis_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicCompletedPrimitivePowerBasis F n).gen =
      equalCharacteristicCompletedPrimitiveRoot F n

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