Module

CompletedFrobeniusFixedFieldDegree.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedFieldDegree

9 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: degree of the completed Frobenius fixed field

The direct theta value has the changed primitive polynomial over k((T)). Together with the fixed-field generation theorem this gives the exact extension degree (q - 1) q^n.

Imports2

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedFieldGeneration

Imported by5

instance

equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra

L33 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra

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

instance

equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra

L40 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra

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

Lean source · statement

instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower

L51 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower

Source context 9 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
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))

Lean source · statement

instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra

L59 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra

Source context 10 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
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n)

instance

equalCharacteristicCompletedFrobeniusFixedFieldDegreeSMul

L69 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldDegreeSMul

Source context 11 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
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  Subalgebra.algebra
    (equalCharacteristicCompletedFrobeniusFixedField F a n).toSubalgebra

Lean source · statement

instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n)

instance

equalCharacteristicCompletedFrobeniusFixedFieldDegreeModule

L79 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldDegreeModule

Source context 12 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
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  Subalgebra.algebra
    (equalCharacteristicCompletedFrobeniusFixedField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra F a n)

Lean source · statement

instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n)

theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isIntegral_laurentBase

L89 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isIntegral_laurentBase

Source context 13 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
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  Subalgebra.algebra
    (equalCharacteristicCompletedFrobeniusFixedField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra F a n)

Lean source · statement

theorem
    equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_isIntegral_laurentBase
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsIntegral F.residueField⸨X⸩
      (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
        equalCharacteristicCompletedLevelField F n)

theorem

equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_minpoly_laurentBase

L102 ↗

LubinTate.EqualCharacteristic.equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_minpoly_laurentBase

Source context 13 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
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  Subalgebra.algebra
    (equalCharacteristicCompletedFrobeniusFixedField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra F a n)

Lean source · statement

theorem
    equalCharacteristicDirectThetaAtCompletedPrimitiveRoot_minpoly_laurentBase
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    minpoly F.residueField⸨X⸩
        (equalCharacteristicDirectThetaAtCompletedPrimitiveRoot F a n :
          equalCharacteristicCompletedLevelField F n) =
      equalCharacteristicChangedPrimitivePolynomial F a n

theorem

equalCharacteristicCompletedFrobeniusFixedField_finrank

L125 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedField_finrank

Documentation

The fixed field has the exact degree of the target division level n + 1: [Sigma : k((T))] = (q - 1) q^n.

Source context 13 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
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeLevelAlgebra
    (F : LocalField.{u, v} K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  RingHom.toAlgebra
    ((algebraMap (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)).comp
      (algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedUnramifiedField F.residueField)))
local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeScalarTower
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  Subalgebra.algebra
    (equalCharacteristicCompletedFrobeniusFixedField F a n).toSubalgebra
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  @Algebra.toSMul _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra F a n)
noncomputable local instance
    equalCharacteristicCompletedFrobeniusFixedFieldDegreeModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n) :=
  @Algebra.toModule _ _ _ _
    (equalCharacteristicCompletedFrobeniusFixedFieldDegreeAlgebra F a n)

Lean source · statement

theorem equalCharacteristicCompletedFrobeniusFixedField_finrank
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module.finrank F.residueField⸨X⸩
        (equalCharacteristicCompletedFrobeniusFixedField F a n) =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

Module documentation

The completed theta-intertwining theorem: degree of the completed Frobenius fixed field

Declarations