NYLL
Module

HigherUnitLevelMapFixed.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.HigherUnitLevelMapFixed
14 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: higher-unit Frobenius fixes the standard

level map

Imports3
Imported by4

Declarations

theorem

ringHom_apply_eq_of_powerBasis

L32 ↗
LubinTate.EqualCharacteristic.ringHom_apply_eq_of_powerBasis
Documentation

Two ring homomorphisms out of a power-basis extension agree pointwise once they agree on the base field and on the power-basis generator.

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
theorem ringHom_apply_eq_of_powerBasis
    {B L C : Type*} [Field B] [Field L] [Algebra B L] [Field C]
    (pb : PowerBasis B L) (delta : C →+* C) (f : L →+* C)
    (hgen : delta (f pb.gen) = f pb.gen)
    (hbase : ∀ b : B,
      delta (f (algebraMap B L b)) = f (algebraMap B L b))
    (x : L) :
    delta (f x) = f x
instance

equalCharacteristicHigherUnitMapBaseAlgebra

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

equalCharacteristicHigherUnitMapLevelAlgebra

L55 ↗
LubinTate.EqualCharacteristic.equalCharacteristicHigherUnitMapLevelAlgebra
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]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
Lean source · statement
instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n)
instance

equalCharacteristicHigherUnitMapScalarTower

L61 ↗
LubinTate.EqualCharacteristic.equalCharacteristicHigherUnitMapScalarTower
Source context 8 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]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
Lean source · statement
instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n)
def

higherUnitLevelMapRingHom

L68 ↗
LubinTate.EqualCharacteristic.higherUnitLevelMapRingHom
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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
def higherUnitLevelMapRingHom
    (F : LocalField K) [CharP K F.residueCharacteristic] (n : ℕ) :
    equalCharacteristicLubinTateLevelField F n →+*
      equalCharacteristicCompletedLevelField F n
theorem

higherUnitLevelMapRingHom_apply

L74 ↗
LubinTate.EqualCharacteristic.higherUnitLevelMapRingHom_apply
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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem higherUnitLevelMapRingHom_apply
    (F : LocalField K) [CharP K F.residueCharacteristic] (n : ℕ)
    (x : equalCharacteristicLubinTateLevelField F n) :
    higherUnitLevelMapRingHom F n x =
      equalCharacteristicLubinTateLevelFieldToCompleted F n x
def

equalCharacteristicLubinTateLevelFieldToCompletedRingHom

L84 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToCompletedRingHom
Documentation

The canonical finite-level embedding into the completed level, regarded as a ring homomorphism. This is the lightweight interface used by consumers that do not need to reconstruct its concrete algebra structures.

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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
def equalCharacteristicLubinTateLevelFieldToCompletedRingHom
    (F : LocalField K) [CharP K F.residueCharacteristic] (n : ℕ) :
    equalCharacteristicLubinTateLevelField F n →+*
      equalCharacteristicCompletedLevelField F n
theorem

equalCharacteristicLubinTateLevelFieldToCompletedRingHom_algebraMap

L92 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldToCompletedRingHom_algebraMap
Documentation

States the theorem equalCharacteristicLubinTateLevelFieldToCompletedRingHom_algebraMap.

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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem equalCharacteristicLubinTateLevelFieldToCompletedRingHom_algebraMap
    (F : LocalField K) [CharP K F.residueCharacteristic]
    (n : ℕ) (b : F.residueField⸨X⸩) :
    equalCharacteristicLubinTateLevelFieldToCompletedRingHom F n
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n) b) =
      algebraMap F.residueField⸨X⸩
        (equalCharacteristicCompletedLevelField F n) b
def

higherUnitFrobeniusRingHom

L105 ↗
LubinTate.EqualCharacteristic.higherUnitFrobeniusRingHom
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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
def higherUnitFrobeniusRingHom
    (F : LocalField K) [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) :
    equalCharacteristicCompletedLevelField F n →+*
      equalCharacteristicCompletedLevelField F n
theorem

higherUnitFrobeniusRingHom_apply

L112 ↗
LubinTate.EqualCharacteristic.higherUnitFrobeniusRingHom_apply
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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem higherUnitFrobeniusRingHom_apply
    (F : LocalField K) [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x : equalCharacteristicCompletedLevelField F n) :
    higherUnitFrobeniusRingHom F a n x =
      equalCharacteristicCompletedFrobeniusAlgEquiv F a n x
theorem

higherUnitLevelMapRingHom_gen

L120 ↗
LubinTate.EqualCharacteristic.higherUnitLevelMapRingHom_gen
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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem higherUnitLevelMapRingHom_gen
    (F : LocalField K) [CharP K F.residueCharacteristic] (n : ℕ) :
    higherUnitLevelMapRingHom F n
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicCompletedPrimitiveRoot F n
theorem

higherUnitFrobeniusRingHom_levelMap_algebraMap

L131 ↗
LubinTate.EqualCharacteristic.higherUnitFrobeniusRingHom_levelMap_algebraMap
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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem higherUnitFrobeniusRingHom_levelMap_algebraMap
    (F : LocalField K) [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ) (b : F.residueField⸨X⸩) :
    higherUnitFrobeniusRingHom F a n
        (higherUnitLevelMapRingHom F n
          (algebraMap F.residueField⸨X⸩
            (equalCharacteristicLubinTateLevelField F n) b)) =
      higherUnitLevelMapRingHom F n
        (algebraMap F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelField F n) b)
theorem

higherUnitLevelMap_fixed_core

L146 ↗
LubinTate.EqualCharacteristic.higherUnitLevelMap_fixed_core
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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem higherUnitLevelMap_fixed_core
    (F : LocalField K) [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ)
    (ha : a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n)
    (x : equalCharacteristicLubinTateLevelField F n) :
    higherUnitFrobeniusRingHom F a n (higherUnitLevelMapRingHom F n x) =
      higherUnitLevelMapRingHom F n x
theorem

equalCharacteristicCompletedFrobeniusAlgEquiv_comp_levelFieldToCompleted_of_mem_higherUnit

L166 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusAlgEquiv_comp_levelFieldToCompleted_of_mem_higherUnit
Documentation

States the theorem equalCharacteristicCompletedFrobeniusAlgEquiv_comp_levelFieldToCompleted_of_mem_higherUnit.

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
variable {K : Type} [Field K]
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapBaseAlgebra
    (F : LocalField K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  equalCharacteristicCompletedLevelBaseAlgebra F
@[reducible] noncomputable local instance equalCharacteristicHigherUnitMapLevelAlgebra
    (F : LocalField K) (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelLaurentAlgebra F n
local instance equalCharacteristicHigherUnitMapScalarTower
    (F : LocalField K) (n : ℕ) :
    IsScalarTower F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
theorem
    equalCharacteristicCompletedFrobeniusAlgEquiv_comp_levelFieldToCompleted_of_mem_higherUnit
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (a : F.residueField⟦X⟧ˣ) (n : ℕ)
    (ha : a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n)
    (x : equalCharacteristicLubinTateLevelField F n) :
    equalCharacteristicCompletedFrobeniusAlgEquiv F a n
        (equalCharacteristicLubinTateLevelFieldToCompleted F n x) =
      equalCharacteristicLubinTateLevelFieldToCompleted F n x

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