NYLL
Module

HigherUnitFrobeniusFixed.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.HigherUnitFrobeniusFixed
2 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: higher units fix the primitive point

If a is congruent to one modulo T^(n+1), the completed the completed theta-intertwining theorem Frobenius attached to a acts trivially on the standard primitive (n+1)-division point.

Imports2
Imported by4

Declarations

instance

equalCharacteristicHigherUnitFixedBaseAlgebra

L32 ↗
LubinTate.EqualCharacteristic.equalCharacteristicHigherUnitFixedBaseAlgebra
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 equalCharacteristicHigherUnitFixedBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
theorem

equalCharacteristicCompletedFrobeniusAlgEquiv_primitiveRoot_fixed_of_mem_higherUnit

L40 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusAlgEquiv_primitiveRoot_fixed_of_mem_higherUnit
Documentation

States the theorem equalCharacteristicCompletedFrobeniusAlgEquiv_primitiveRoot_fixed_of_mem_higherUnit.

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 equalCharacteristicHigherUnitFixedBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedFrobeniusFixedBaseAlgebra F
Lean source · statement
theorem
    equalCharacteristicCompletedFrobeniusAlgEquiv_primitiveRoot_fixed_of_mem_higherUnit
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ)
    (ha : a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n) :
    equalCharacteristicCompletedFrobeniusAlgEquiv F a n
        (equalCharacteristicCompletedPrimitiveRoot F n) =
      equalCharacteristicCompletedPrimitiveRoot F n

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.