Module

CompletedFrobeniusFixedFieldAlgebra.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedFieldAlgebra

7 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: the canonical base algebra on the fixed field

This light leaf names the base algebra already determined by the completed Frobenius action. Naming it prevents repeated fallback searches through generic scalar-action instances in later norm calculations.

Imports1

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusFixedField

Imported by4

instance

equalCharacteristicFixedFieldAlgebraBaseAlgebra

L31 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFixedFieldAlgebraBaseAlgebra

Source context 6 commands

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

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

Lean source · statement

instance equalCharacteristicFixedFieldAlgebraBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)

instance

equalCharacteristicFixedFieldAlgebraLevelAlgebra

L37 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFixedFieldAlgebraLevelAlgebra

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicFixedFieldAlgebraBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F

Lean source · statement

instance equalCharacteristicFixedFieldAlgebraLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n)

instance

equalCharacteristicFixedFieldAlgebraScalarTower

L43 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFixedFieldAlgebraScalarTower

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicFixedFieldAlgebraBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
noncomputable local instance equalCharacteristicFixedFieldAlgebraLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedFrobeniusFixedLevelAlgebra F n

Lean source · statement

instance equalCharacteristicFixedFieldAlgebraScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)

def

equalCharacteristicCompletedFrobeniusFixedFieldSubring

L53 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldSubring

Documentation

The completed Frobenius fixed field, viewed only as a subring of the completed level. This lightweight projection lets ring-homomorphism consumers avoid reconstructing the ambient Laurent-base algebra.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicFixedFieldAlgebraBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
noncomputable local instance equalCharacteristicFixedFieldAlgebraLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedFrobeniusFixedLevelAlgebra F n
local instance equalCharacteristicFixedFieldAlgebraScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

def equalCharacteristicCompletedFrobeniusFixedFieldSubring
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Subring (equalCharacteristicCompletedLevelField F n)

def

equalCharacteristicCompletedFrobeniusFixedFieldAlgebra

L63 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldAlgebra

Documentation

The canonical k((T))-algebra structure on the completed theta-intertwining theorem fixed field.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicFixedFieldAlgebraBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
noncomputable local instance equalCharacteristicFixedFieldAlgebraLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedFrobeniusFixedLevelAlgebra F n
local instance equalCharacteristicFixedFieldAlgebraScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

def equalCharacteristicCompletedFrobeniusFixedFieldAlgebra
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n)

def

equalCharacteristicCompletedFrobeniusFixedFieldSMul

L76 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldSMul

Documentation

The scalar action induced by the canonical k((T))-algebra structure on the completed Frobenius fixed field. Naming it lets downstream files reuse the same structure without asking typeclass search to unfold the fixed field.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicFixedFieldAlgebraBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
noncomputable local instance equalCharacteristicFixedFieldAlgebraLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedFrobeniusFixedLevelAlgebra F n
local instance equalCharacteristicFixedFieldAlgebraScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

def equalCharacteristicCompletedFrobeniusFixedFieldSMul
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    SMul F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n)

def

equalCharacteristicCompletedFrobeniusFixedFieldModule

L88 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusFixedFieldModule

Documentation

The module structure induced by the canonical k((T))-algebra structure on the completed Frobenius fixed field.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicFixedFieldAlgebraBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
noncomputable local instance equalCharacteristicFixedFieldAlgebraLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedFrobeniusFixedLevelAlgebra F n
local instance equalCharacteristicFixedFieldAlgebraScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl

Lean source · statement

def equalCharacteristicCompletedFrobeniusFixedFieldModule
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Module F.residueField⸨X⸩
      (equalCharacteristicCompletedFrobeniusFixedField F a n)

Module documentation

The completed theta-intertwining theorem: the canonical base algebra on the fixed field

Declarations

equalCharacteristicFixedFieldAlgebraBaseAlgebra

equalCharacteristicFixedFieldAlgebraLevelAlgebra

equalCharacteristicFixedFieldAlgebraScalarTower

equalCharacteristicCompletedFrobeniusFixedFieldSubring

equalCharacteristicCompletedFrobeniusFixedFieldAlgebra

equalCharacteristicCompletedFrobeniusFixedFieldSMul

equalCharacteristicCompletedFrobeniusFixedFieldModule