Module

HigherUnitFixedFieldEmbedding.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.HigherUnitFixedFieldEmbedding

2 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: the standard level embedded in the

higher-unit fixed field

For a coefficient unit in U^(n+1), the standard completed-level embedding lands in the completed theta-intertwining theorem fixed field. This leaf packages its canonical codomain restriction for the finite-dimensional comparison.

Imports2

Imported by4

def

equalCharacteristicLubinTateLevelFieldToFixedFieldOfHigherUnitRingHom

L45 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToFixedFieldOfHigherUnitRingHom

Documentation

The canonical standard-level embedding into the fixed field attached to a higher unit, regarded as a ring homomorphism. This lightweight helper keeps the codomain restriction independent of algebra-instance search.

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]
attribute [local instance]
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra
  equalCharacteristicLubinTateLevelFieldAlgebra
  equalCharacteristicLubinTateLevelFieldSMul
  equalCharacteristicLubinTateLevelFieldModule
  equalCharacteristicCompletedFrobeniusFixedFieldAlgebra
  equalCharacteristicCompletedFrobeniusFixedFieldSMul
  equalCharacteristicCompletedFrobeniusFixedFieldModule

Lean source · statement

def
    equalCharacteristicLubinTateLevelFieldToFixedFieldOfHigherUnitRingHom
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ)
    (ha : a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n) :
    equalCharacteristicLubinTateLevelField F n →+*
      equalCharacteristicCompletedFrobeniusFixedField F a n

def

equalCharacteristicLubinTateLevelFieldToFixedFieldOfHigherUnit

L60 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToFixedFieldOfHigherUnit