Module

UniformizerNorm.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.UniformizerNorm

3 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: the uniformizer factor is a norm

The normalized Laurent uniformizer T⁻¹ is the inverse of the norm of the negative primitive Lubin--Tate division point. This light leaf isolates the valuation factor of the norm-subgroup calculation from the later openness and index arguments.

Imports2

Imported by6

theorem

inverse_mem_normSubgroup_of_normUnits_eq

L35 ↗

LubinTate.EqualCharacteristic.inverse_mem_normSubgroup_of_normUnits_eq

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped LaurentSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
universe u

Lean source · statement

theorem inverse_mem_normSubgroup_of_normUnits_eq
    {B E : Type u} [Field B] [Field E] [Algebra B E]
    [FiniteDimensional B E] (y : Eˣ) (pi : Bˣ)
    (hyNorm : LocalFieldTheory.normUnits B E y = pi) :
    pi⁻¹ ∈ LocalFieldTheory.localNormSubgroup B E

theorem

equalCharacteristicLubinTate_normalizedUniformizer_mem_normSubgroup

L49 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTate_normalizedUniformizer_mem_normSubgroup

Documentation

The normalized Laurent uniformizer T⁻¹ is an actual norm from every explicit Lubin--Tate level field.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped LaurentSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
universe u

Lean source · statement

theorem equalCharacteristicLubinTate_normalizedUniformizer_mem_normSubgroup
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLaurentUniformizerUnit F)⁻¹ ∈
      equalCharacteristicLubinTateNormSubgroup F n

theorem

equalCharacteristicLubinTate_normalizedUniformizer_zpowers_le_normSubgroup

L71 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTate_normalizedUniformizer_zpowers_le_normSubgroup

Documentation

Every integral power of the normalized Laurent uniformizer is a norm.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped LaurentSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
universe u

Lean source · statement

theorem equalCharacteristicLubinTate_normalizedUniformizer_zpowers_le_normSubgroup
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Subgroup.zpowers ((equalCharacteristicLaurentUniformizerUnit F)⁻¹) ≤
      equalCharacteristicLubinTateNormSubgroup F n

Module documentation

LubinTate the explicit norm-subgroup computation: the uniformizer factor is a norm

Declarations

inverse_mem_normSubgroup_of_normUnits_eq

equalCharacteristicLubinTate_normalizedUniformizer_mem_normSubgroup

equalCharacteristicLubinTate_normalizedUniformizer_zpowers_le_normSubgroup