Module

HigherUnitFixedFieldSurjective.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.HigherUnitFixedFieldSurjective

2 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: surjectivity of the higher-unit fixed-field

embedding

The standard level and the fixed field have the same finite degree (q - 1) q^n; hence the canonical injective embedding is surjective.

Imports2

Imported by4

theorem

ringHom_surjective_of_finrank_eq

L38 ↗

LubinTate.EqualCharacteristic.ringHom_surjective_of_finrank_eq

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
  equalCharacteristicCompletedFrobeniusFixedFieldAlgebra
  equalCharacteristicCompletedFrobeniusFixedFieldSMul
  equalCharacteristicCompletedFrobeniusFixedFieldModule

Lean source · statement

theorem ringHom_surjective_of_finrank_eq
    {B E L : Type*}
    [Field B] [Field E] [Field L]
    [Algebra B E] [Algebra B L]
    [FiniteDimensional B E] [FiniteDimensional B L]
    (f : E →+* L)
    (hcomm : ∀ b : B,
      f (algebraMap B E b) = algebraMap B L b)
    (hdim : Module.finrank B E = Module.finrank B L) :
    Function.Surjective f

theorem

equalCharacteristicLubinTateLevelFieldToFixedFieldOfHigherUnit_surjective

L56 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToFixedFieldOfHigherUnit_surjective

Documentation

The canonical standard-level embedding onto the higher-unit fixed field is surjective.