NYLL
Module

CompletedFrobeniusFixedFieldPrimitive.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedFieldPrimitive
7 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: the fixed-field primitive point over the completed base

The direct theta value has the changed completed primitive polynomial as its minimal polynomial over the completed maximal-unramified Laurent field. Comparing degrees shows that this point generates the whole completed level.

Imports3
Imported by4

Declarations

instance

equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra

L35 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
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
    equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
instance

equalCharacteristicCompletedFrobeniusIdentificationLevelCharP

L43 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusIdentificationLevelCharP
Documentation

Provides the instance equalCharacteristicCompletedFrobeniusIdentificationLevelCharP.

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
    equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
instance equalCharacteristicCompletedFrobeniusIdentificationLevelCharP
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic] (n : ℕ) :
    CharP (equalCharacteristicCompletedLevelField F n)
      F.residueCharacteristic
theorem

equalCharacteristicDirectTargetCompletedPrimitivePolynomial_eq

L53 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectTargetCompletedPrimitivePolynomial_eq
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
    equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicDirectTargetCompletedPrimitivePolynomial_eq
    (F : LocalField.{u, v} K)
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicChangedCompletedPrimitivePolynomial F a⁻¹ n =
      (equalCharacteristicChangedPrimitivePolynomial F a n).map
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicCompletedUnramifiedField F.residueField))
theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isRoot_targetCompleted

L63 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isRoot_targetCompleted
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
    equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem
    equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isRoot_targetCompleted
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    ((equalCharacteristicChangedCompletedPrimitivePolynomial F a⁻¹ n).map
      (algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n))).IsRoot
      (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
        equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isIntegral_completedBase

L80 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isIntegral_completedBase
Documentation

States the theorem equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isIntegral_completedBase.

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
    equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem
    equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isIntegral_completedBase
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsIntegral (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
        equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_minpoly_completedBase

L95 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_minpoly_completedBase
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
    equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem
    equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_minpoly_completedBase
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    minpoly (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
          equalCharacteristicCompletedLevelField F n) =
      equalCharacteristicChangedCompletedPrimitivePolynomial F a⁻¹ n
theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_adjoin_completedBase_eq_top

L121 ↗
LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_adjoin_completedBase_eq_top
Documentation

The fixed target primitive point generates the standard completed level 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
    equalCharacteristicCompletedFrobeniusFixedFieldCompletedPrimitiveBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem
    equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_adjoin_completedBase_eq_top
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IntermediateField.adjoin
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        ({(equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
          equalCharacteristicCompletedLevelField F n)} :
          Set (equalCharacteristicCompletedLevelField F n)) = ⊤

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