NYLL
Module

UnitTransport.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.UnitTransport
7 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: power-series units as Laurent field units

This file packages the genuine composite

k[[T]]ˣ ≃ 𝒪[k((T))]ˣ → k((T))ˣ

used in the sharp norm-subgroup calculation. Its range is the full valuation-zero unit subgroup, and it carries the explicit Lubin--Tate kernel to the higher-unit subgroup U^(n+1). The same composite is definitionally the Laurent unit multiplying T in the changed uniformizer of the completed theta-intertwining theorem.

Imports5
Imported by4

Declarations

def

equalCharacteristicPowerSeriesUnitToLaurentFieldUnit

L48 ↗
LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesUnitToLaurentFieldUnit
Documentation

The canonical inclusion of a power-series unit into the Laurent field unit group, through the actual valuation ring.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicPowerSeriesUnitToLaurentFieldUnit
    (F : LocalField.{u, v} K) :
    F.residueField⟦X⟧ˣ →* F.residueField⸨X⸩ˣ
theorem

equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_apply

L61 ↗
LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_apply
Documentation

The canonical unit inclusion is the Laurent unit used in the changed uniformizer uT of the completed theta-intertwining theorem.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_apply
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicPowerSeriesUnitToLaurentFieldUnit F a =
      equalCharacteristicChangedLaurentUnit F a
theorem

equalCharacteristicChangedLaurentUniformizerUnit_eq_unit_mul

L70 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerUnit_eq_unit_mul
Documentation

In the field unit group, the changed uniformizer is the product of its power-series unit factor and T.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicChangedLaurentUniformizerUnit_eq_unit_mul
    (F : LocalField.{u, v} K) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedLaurentUniformizerUnit F a =
      equalCharacteristicChangedLaurentUnit F a *
        equalCharacteristicLaurentUniformizerUnit F
theorem

equalCharacteristicChangedLaurentUniformizerUnit_mem_normSubgroup_iff

L82 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerUnit_mem_normSubgroup_iff
Documentation

Multiplication by T does not change norm membership for a Lubin--Tate level, because both T⁻¹ and T are already norms. Thus the prime norm uT used in the completed theta-intertwining theorem detects exactly whether the unit u is a norm.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicChangedLaurentUniformizerUnit_mem_normSubgroup_iff
    {K₀ : Type} [Field K₀]
    (F : LocalField K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicChangedLaurentUniformizerUnit F a ∈
        equalCharacteristicLubinTateNormSubgroup F n ↔
      equalCharacteristicChangedLaurentUnit F a ∈
        equalCharacteristicLubinTateNormSubgroup F n
theorem

equalCharacteristicChangedLaurentUniformizerUnit_inv_mem_normSubgroup_iff

L111 ↗
LubinTate.EqualCharacteristic.equalCharacteristicChangedLaurentUniformizerUnit_inv_mem_normSubgroup_iff
Documentation

The positive-valuation inverse prime norm used by the normalized normalized additive valuation has the same norm-membership test.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicChangedLaurentUniformizerUnit_inv_mem_normSubgroup_iff
    {K₀ : Type} [Field K₀]
    (F : LocalField K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicChangedLaurentUniformizerUnit F a)⁻¹ ∈
        equalCharacteristicLubinTateNormSubgroup F n ↔
      equalCharacteristicChangedLaurentUnit F a ∈
        equalCharacteristicLubinTateNormSubgroup F n
theorem

equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_range

L134 ↗
LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_range
Documentation

Every valuation-zero Laurent field unit, and only such a unit, comes from a power-series unit under the canonical inclusion.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable {K : Type u} [Field K]
Lean source · full declaration
theorem equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_range
    (F : LocalField.{u, v} K) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    MonoidHom.range (equalCharacteristicPowerSeriesUnitToLaurentFieldUnit F) =
      LocalFieldTheory.localBaseUnitSubgroup F.residueField⸨X⸩ := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  let e := equalCharacteristicPowerSeriesUnitsEquivLaurentInteger
    F.residueField
  change MonoidHom.range
      ((integerUnitsToFieldUnits F.residueField⸨X⸩).comp e.toMonoidHom) =
    MonoidHom.range (integerUnitsToFieldUnits F.residueField⸨X⸩)
  ext x
  constructor
  · rintro ⟨a, rfl⟩
    exact ⟨e a, rfl⟩
  · rintro ⟨b, rfl⟩
    refine ⟨e.symm b, ?_⟩
    simp [e]
theorem

equalCharacteristicLubinTateHigherUnitSubgroup_map_toLaurentField_eq

L157 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateHigherUnitSubgroup_map_toLaurentField_eq
Documentation

The explicit Lubin--Tate higher-unit kernel maps to the canonical field principal-unit group U^(n+1) in one step.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable {K : Type u} [Field K]
Lean source · full declaration
theorem equalCharacteristicLubinTateHigherUnitSubgroup_map_toLaurentField_eq
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    (equalCharacteristicLubinTateHigherUnitSubgroup F n).map
        (equalCharacteristicPowerSeriesUnitToLaurentFieldUnit F) =
      LocalFieldTheory.fieldPrincipalUnits F.residueField⸨X⸩ (n + 1) := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  simpa only [equalCharacteristicPowerSeriesUnitToLaurentFieldUnit,
    Subgroup.map_map] using
    (equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_fieldPrincipalUnits
      F n)

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