NYLL
Module

CompletedFrobeniusLift.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusLift
15 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: a prescribed Frobenius lift on the completed level

Arithmetic Frobenius on (AlgebraicClosure κ)((T)) fixes the primitive Lubin--Tate polynomial. Using its primitive power basis, we extend Frobenius to the completed level while prescribing the image of the primitive point to be a chosen unit bracket. The resulting semilinear field endomorphism is surjective because that bracket is again a primitive generator.

Imports1
Imported by4

Declarations

instance

equalCharacteristicCompletedFrobeniusLiftBaseAlgebra

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

equalCharacteristicCompletedLevelOriginalAlgebra

L45 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelOriginalAlgebra
Documentation

The ordinary completed-base algebra structure on the splitting field, named explicitly so it can coexist with its Frobenius twist.

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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedLevelOriginalAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
def

equalCharacteristicCompletedLevelFrobeniusAlgebra

L54 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelFrobeniusAlgebra
Documentation

The codomain algebra structure whose scalar map is arithmetic Frobenius followed by the ordinary scalar inclusion.

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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedLevelFrobeniusAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicCompletedLevelFrobeniusAlgebra_algebraMap

L65 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevelFrobeniusAlgebra_algebraMap
Documentation

The twisted level algebra map applies completed Frobenius before 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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedLevelFrobeniusAlgebra_algebraMap
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicCompletedUnramifiedField F.residueField) :
    @algebraMap
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)
        _ _ (equalCharacteristicCompletedLevelFrobeniusAlgebra F n) a =
      algebraMap
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)
        (equalCharacteristicCompletedUnramifiedFrobenius F.residueField a)
theorem

equalCharacteristicCompletedPrimitivePolynomial_frobenius

L80 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_frobenius
Documentation

Arithmetic Frobenius fixes the completed primitive polynomial because all of its coefficients descend to κ((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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedPrimitivePolynomial_frobenius
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedPrimitivePolynomial F n).map
        (equalCharacteristicCompletedUnramifiedFrobenius F.residueField).toAlgHom.toRingHom =
      equalCharacteristicCompletedPrimitivePolynomial F n
theorem

equalCharacteristicCompletedUnitRoot_aeval_minpoly_frobenius

L100 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnitRoot_aeval_minpoly_frobenius
Documentation

A unit bracket is a root of the primitive minimal polynomial for the Frobenius-twisted codomain algebra structure.

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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedUnitRoot_aeval_minpoly_frobenius
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    @Polynomial.aeval
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)
        _ _ (equalCharacteristicCompletedLevelFrobeniusAlgebra F n)
        (equalCharacteristicCompletedUnitRoot F n a)
        (minpoly (equalCharacteristicCompletedUnramifiedField F.residueField)
          (equalCharacteristicCompletedPrimitiveRoot F n)) = 0
def

equalCharacteristicCompletedFrobeniusLiftAlgHom

L126 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftAlgHom
Documentation

The semilinear algebra homomorphism extending arithmetic Frobenius and sending the primitive point to the prescribed unit bracket.

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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
def equalCharacteristicCompletedFrobeniusLiftAlgHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    @AlgHom
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
      (equalCharacteristicCompletedLevelField F n)
      _ _ _
      (equalCharacteristicCompletedLevelOriginalAlgebra F n)
      (equalCharacteristicCompletedLevelFrobeniusAlgebra F n)
theorem

equalCharacteristicCompletedFrobeniusLiftAlgHom_primitiveRoot

L150 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftAlgHom_primitiveRoot
Documentation

The semilinear Frobenius homomorphism sends the primitive root to its unit transform.

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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLiftAlgHom_primitiveRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicCompletedFrobeniusLiftAlgHom F n a
        (equalCharacteristicCompletedPrimitiveRoot F n) =
      equalCharacteristicCompletedUnitRoot F n a
def

equalCharacteristicCompletedFrobeniusLift

L170 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLift
Documentation

The underlying field homomorphism of the prescribed Frobenius lift.

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

equalCharacteristicCompletedFrobeniusLift_algebraMap

L187 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLift_algebraMap
Documentation

The Frobenius lift acts on base scalars by completed Frobenius.

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

equalCharacteristicCompletedFrobeniusLift_primitiveRoot

L218 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLift_primitiveRoot
Documentation

The Frobenius lift sends the primitive root to the corresponding unit 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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLift_primitiveRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicCompletedFrobeniusLift F n a
        (equalCharacteristicCompletedPrimitiveRoot F n) =
      equalCharacteristicCompletedUnitRoot F n a
theorem

equalCharacteristicCompletedFrobeniusLift_surjective

L233 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLift_surjective
Documentation

The prescribed semilinear Frobenius lift is onto: its range contains the whole completed base and the primitive generator given by the unit bracket.

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 equalCharacteristicCompletedFrobeniusLiftBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLift_surjective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    Function.Surjective (equalCharacteristicCompletedFrobeniusLift F n a)
def

equalCharacteristicCompletedFrobeniusLiftEquiv

L276 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftEquiv
Documentation

The actual field automorphism extending arithmetic Frobenius and acting on the primitive point by the prescribed unit bracket.

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

equalCharacteristicCompletedFrobeniusLiftEquiv_algebraMap

L288 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftEquiv_algebraMap
Documentation

The Frobenius lift equivalence acts on base scalars by completed Frobenius.

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

equalCharacteristicCompletedFrobeniusLiftEquiv_primitiveRoot

L303 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftEquiv_primitiveRoot
Documentation

The Frobenius lift equivalence sends the primitive root to its unit transform.

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

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