NYLL
Module

StandardSubgroupNorm.lean

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

Module documentation

LubinTate the explicit norm-subgroup computation: the sharp standard subgroup consists of norms

The higher-unit norm calculation and the uniformizer norm combine to give the division-level inclusion (T⁻¹) × U^(n+1) ≤ N(L_n/K).

Imports2
Imported by4

Declarations

theorem

equalCharacteristicLubinTate_fieldPrincipalUnits_le_normSubgroup

L35 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTate_fieldPrincipalUnits_le_normSubgroup
Documentation

The canonical field principal-unit subgroup U^(n+1) consists of norms from the standard level.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
Lean source · full declaration
theorem equalCharacteristicLubinTate_fieldPrincipalUnits_le_normSubgroup
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    LocalFieldTheory.fieldPrincipalUnits F.residueField⸨X⸩ (n + 1) ≤
      equalCharacteristicLubinTateNormSubgroup F n := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  rw [← equalCharacteristicLubinTateHigherUnitSubgroup_map_toLaurentField_eq]
  rintro x ⟨a, ha, rfl⟩
  exact
    equalCharacteristicPowerSeriesUnitToLaurentFieldUnit_mem_normSubgroup_of_mem_higherUnit
      F n a ha
theorem

equalCharacteristicLubinTate_uniformizerPrincipalSubgroup_le_normSubgroup

L53 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTate_uniformizerPrincipalSubgroup_le_normSubgroup
Documentation

The sharp standard subgroup (T⁻¹) × U^(n+1) is contained in the norm subgroup.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
variable {K : Type} [Field K]
Lean source · full declaration
theorem
    equalCharacteristicLubinTate_uniformizerPrincipalSubgroup_le_normSubgroup
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    LocalFieldTheory.uniformizerPrincipalSubgroup F.residueField⸨X⸩
        ((equalCharacteristicLaurentUniformizerUnit F)⁻¹) 1 (n + 1) ≤
      equalCharacteristicLubinTateNormSubgroup F n := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  rw [LocalFieldTheory.uniformizerPrincipalSubgroup]
  apply sup_le
  · simpa using
      equalCharacteristicLubinTate_normalizedUniformizer_zpowers_le_normSubgroup
        F n
  · exact
      equalCharacteristicLubinTate_fieldPrincipalUnits_le_normSubgroup F n

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