Module

BaseNorm.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.BaseNorm

4 declarations indexed from sourceView source ↗

Module documentation

Norms of base units in Neu1999 local fields

This file supplies concrete elements of field-norm subgroups coming from base units. It is an element-level source for later ramification-image comparisons.

Imports1

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValueGroup.NonarchimedeanLocalField.Invariants

Imported by3

theorem

fieldNormUnits_mapBaseUnitsToExtensionUnits

L32 ↗

TameAbhyankar.NAField.fieldNormUnits_mapBaseUnitsToExtensionUnits

Documentation

The field norm of a base unit embedded into the extension is the [L : K]-th power of that base unit.

Source context 8 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem fieldNormUnits_mapBaseUnitsToExtensionUnits
    (x : Kˣ) :
    normUnits K L
        (LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnitsToExtensionUnits K L x) =
      x ^ Module.finrank K L

theorem

pow_finrank_mem_fieldNormSubgroup

L43 ↗

TameAbhyankar.NAField.pow_finrank_mem_fieldNormSubgroup

Documentation

Every [L : K]-th power of a base unit lies in the field-norm subgroup from L/K.

Source context 8 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem pow_finrank_mem_fieldNormSubgroup (x : Kˣ) :
    x ^ Module.finrank K L ∈ fieldNormSubgroup K L

theorem

exists_mem_fieldNormSubgroup_val_finrank_of_uniformizer

L57 ↗

TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_finrank_of_uniformizer

Documentation

A base uniformizer gives a concrete field-norm subgroup element whose valuation is the field degree [L : K].

Source context 11 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section Valuation
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]

Lean source · statement

theorem exists_mem_fieldNormSubgroup_val_finrank_of_uniformizer
    {ϖ : Kˣ} (hϖ : (multiplicativeIntegerValuation K).IsUniformizer ϖ) :
    ∃ x : Kˣ, x ∈ fieldNormSubgroup K L ∧
      (multiplicativeIntegerValuation K).val x =
        (Module.finrank K L : ℤ)

theorem

exists_mem_fieldNormSubgroup_val_finrank

L75 ↗

TameAbhyankar.NAField.exists_mem_fieldNormSubgroup_val_finrank

Documentation

A Neu1999 base local field supplies a concrete field-norm subgroup element whose valuation is the field degree [L : K].

Source context 11 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
namespace NAField
variable {K L : Type u}
variable [Field K] [Field L] [Algebra K L]
section Valuation
variable [ValuativeRel K] [TopologicalSpace K]
variable [IsNonarchimedeanLocalField K]

Lean source · statement

theorem exists_mem_fieldNormSubgroup_val_finrank :
    ∃ x : Kˣ, x ∈ fieldNormSubgroup K L ∧
      (multiplicativeIntegerValuation K).val x =
        (Module.finrank K L : ℤ)

Module documentation

Norms of base units in Neu1999 local fields

Declarations

fieldNormUnits_mapBaseUnitsToExtensionUnits

pow_finrank_mem_fieldNormSubgroup

exists_mem_fieldNormSubgroup_val_finrank_of_uniformizer

exists_mem_fieldNormSubgroup_val_finrank