Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.HigherUnitsNorm

Module documentation

LubinTate the explicit norm-subgroup computation: higher units are norms from the standard level

The fixed-field norm N(-pi_delta) = aT from the completed theta-intertwining theorem is transported through the standard-level equivalence. Cancelling the already known norm T then puts every level-n+1 higher unit in the standard norm subgroup.

theorem

equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_mem_normSubgroup_of_mem_higherUnit

L47 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_mem_normSubgroup_of_mem_higherUnit

Documentation

The sharp higher-unit inclusion in LubinTate the explicit norm-subgroup computation.

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
open LocalFieldTheory
open LocalFieldTheory
variable {K : Type} [Field K]
attribute [local instance]
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra
  equalCharacteristicLubinTateLevelFieldAlgebra
  equalCharacteristicLubinTateLevelFieldSMul
  equalCharacteristicLubinTateLevelFieldModule
  equalCharacteristicCompletedFrobeniusFixedFieldAlgebra
  equalCharacteristicCompletedFrobeniusFixedFieldSMul
  equalCharacteristicCompletedFrobeniusFixedFieldModule

Lean source · statement

theorem
    equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_mem_normSubgroup_of_mem_higherUnit
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ)
    (ha : a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n) :
    equalCharacteristicPowerSeriesUnitToLaurentFieldUnit F a ∈
      equalCharacteristicLubinTateNormSubgroup F n

Module documentation

LubinTate the explicit norm-subgroup computation: higher units are norms from the standard level

Declarations

equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_mem_normSubgroup_of_mem_higherUnit