Module

LevelAlgebra.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.LevelAlgebra

4 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: canonical algebra and norm subgroup at a

finite level

This light leaf names the canonical base algebra and its norm subgroup once, so the later inclusion and index arguments do not repeat expensive fallback typeclass searches.

Imports2

Imported by4

instance

equalCharacteristicLaurentSeriesField

L33 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLaurentSeriesField

Source context 6 commands

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

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

Lean source · statement

instance equalCharacteristicLaurentSeriesField
    (F : LocalField K) : Field F.residueField⸨X⸩

instance

equalCharacteristicLaurentSeriesMonoid

L38 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLaurentSeriesMonoid

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicLaurentSeriesField
    (F : LocalField K) : Field F.residueField⸨X⸩ :=
  @HahnSeries.instField ℤ F.residueField Int.instAddCommGroup
    Int.instLinearOrder Int.instIsOrderedAddMonoid inferInstance

Lean source · statement

instance equalCharacteristicLaurentSeriesMonoid
    (F : LocalField K) : Monoid F.residueField⸨X⸩

def

equalCharacteristicLubinTateLevelAlgebra

L51 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelAlgebra

Documentation

The canonical base algebra on the explicit Lubin--Tate level field.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicLaurentSeriesField
    (F : LocalField K) : Field F.residueField⸨X⸩ :=
  @HahnSeries.instField ℤ F.residueField Int.instAddCommGroup
    Int.instLinearOrder Int.instIsOrderedAddMonoid inferInstance
noncomputable local instance equalCharacteristicLaurentSeriesMonoid
    (F : LocalField K) : Monoid F.residueField⸨X⸩ :=
  @CommMonoid.toMonoid F.residueField⸨X⸩
    (@CommRing.toCommMonoid F.residueField⸨X⸩
      (@Field.toCommRing F.residueField⸨X⸩
        (equalCharacteristicLaurentSeriesField F)))
attribute [local instance]
  equalCharacteristicLubinTateLevelFieldAlgebra
  equalCharacteristicLubinTateLevelFieldSMul
  equalCharacteristicLubinTateLevelFieldModule

Lean source · statement

def equalCharacteristicLubinTateLevelAlgebra
    (F : LocalField K) [CharP K F.residueCharacteristic] (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)

def

equalCharacteristicLubinTateNormSubgroup

L59 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateNormSubgroup

Documentation

The norm subgroup of the explicit Lubin--Tate level, with the canonical base algebra fixed once for downstream statements.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
noncomputable local instance equalCharacteristicLaurentSeriesField
    (F : LocalField K) : Field F.residueField⸨X⸩ :=
  @HahnSeries.instField ℤ F.residueField Int.instAddCommGroup
    Int.instLinearOrder Int.instIsOrderedAddMonoid inferInstance
noncomputable local instance equalCharacteristicLaurentSeriesMonoid
    (F : LocalField K) : Monoid F.residueField⸨X⸩ :=
  @CommMonoid.toMonoid F.residueField⸨X⸩
    (@CommRing.toCommMonoid F.residueField⸨X⸩
      (@Field.toCommRing F.residueField⸨X⸩
        (equalCharacteristicLaurentSeriesField F)))
attribute [local instance]
  equalCharacteristicLubinTateLevelFieldAlgebra
  equalCharacteristicLubinTateLevelFieldSMul
  equalCharacteristicLubinTateLevelFieldModule

Lean source · statement

def equalCharacteristicLubinTateNormSubgroup
    (F : LocalField K) [CharP K F.residueCharacteristic] (n : ℕ) :
    Subgroup F.residueField⸨X⸩ˣ

Module documentation

LubinTate the explicit norm-subgroup computation: canonical algebra and norm subgroup at a

Declarations

equalCharacteristicLaurentSeriesField

equalCharacteristicLaurentSeriesMonoid

equalCharacteristicLubinTateLevelAlgebra

equalCharacteristicLubinTateNormSubgroup