NYLL
Module

Norm.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.Norm
24 declarations indexed from sourceView source ↗

Module documentation

Norms in valued field extensions

Packages field norms as homomorphisms on units and restricts them to valuation rings and their unit groups under the appropriate integral hypotheses.

Imports6
Imported by8

Declarations

lemma

mulLeft_injective_of_ne_zero

L38 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.mulLeft_injective_of_ne_zero
Documentation

Left multiplication by a nonzero field element is injective as a linear map.

Source context 9 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section AlgebraNorm
variable [Field K] [Field L] [Algebra K L] [Module.Free K L] [Module.Finite K L]
omit [Module.Free K L] [Module.Finite K L] in
Lean source · statement
lemma mulLeft_injective_of_ne_zero {x : L} (hx : x ≠ 0) :
    Function.Injective (LinearMap.mulLeft K x)
lemma

mulLeft_surjective_of_ne_zero

L45 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.mulLeft_surjective_of_ne_zero
Documentation

Left multiplication by a nonzero field element is surjective as a linear map.

Source context 9 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section AlgebraNorm
variable [Field K] [Field L] [Algebra K L] [Module.Free K L] [Module.Finite K L]
omit [Module.Free K L] [Module.Finite K L] in
Lean source · statement
lemma mulLeft_surjective_of_ne_zero {x : L} (hx : x ≠ 0) :
    Function.Surjective (LinearMap.mulLeft K x)
lemma

det_ne_zero_of_bijective

L52 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.det_ne_zero_of_bijective
Documentation

A bijective linear endomorphism has nonzero determinant.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section AlgebraNorm
variable [Field K] [Field L] [Algebra K L] [Module.Free K L] [Module.Finite K L]
Lean source · statement
lemma det_ne_zero_of_bijective (f : L →ₗ[K] L) (hf : Function.Bijective f) :
    LinearMap.det f ≠ 0
def

mapBaseUnitsToExtensionUnits

L68 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnitsToExtensionUnits
Documentation

Base units embedded in an extension.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
def mapBaseUnitsToExtensionUnits
    (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L] :
    Kˣ →* Lˣ
lemma

mapBaseUnitsToExtensionUnits_apply_coe

L77 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnitsToExtensionUnits_apply_coe
Documentation

The inclusion of base-field units into extension-field units agrees with the algebra map on underlying elements.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma mapBaseUnitsToExtensionUnits_apply_coe (x : Kˣ) :
    ((mapBaseUnitsToExtensionUnits K L x : Lˣ) : L) = algebraMap K L (x : K)
lemma

normUnits_mapBaseUnitsToExtensionUnits_apply_coe

L83 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normUnits_mapBaseUnitsToExtensionUnits_apply_coe
Documentation

The norm of a base unit embedded in the extension is its underlying element raised to the extension degree.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma normUnits_mapBaseUnitsToExtensionUnits_apply_coe (x : Kˣ) :
    ((normUnits K L (mapBaseUnitsToExtensionUnits K L x) : Kˣ) : K) =
      (x : K) ^ Module.finrank K L
lemma

normUnits_algebraMap_base

L89 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normUnits_algebraMap_base
Documentation

The unit norm of an embedded base unit is the degree-th power of that base unit.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma normUnits_algebraMap_base (x : Kˣ) :
    normUnits K L (mapBaseUnitsToExtensionUnits K L x) =
      Units.map (MonoidHom.id K) (x ^ Module.finrank K L)
lemma

normUnits_algEquiv_apply

L96 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normUnits_algEquiv_apply
Documentation

The field norm is invariant under K-algebra automorphisms of the extension.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma normUnits_algEquiv_apply (σ : L ≃ₐ[K] L) (x : Lˣ) :
    normUnits K L (Units.mapEquiv σ.toMulEquiv x) = normUnits K L x
lemma

algebraNorm_mem_integers_of_mem_integers

L102 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.algebraNorm_mem_integers_of_mem_integers
Documentation

The norm of an element integral over the base valuation ring lies in the base valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma algebraNorm_mem_integers_of_mem_integers [ValuativeRel K] [ValuativeRel L]
    [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]) :
    Algebra.norm K (x : L) ∈ 𝒪[K]
lemma

integer_element_isIntegral_over_base_integer_of_isIntegralClosure

L110 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.integer_element_isIntegral_over_base_integer_of_isIntegralClosure
Documentation

An element of an integral-closure valuation ring is integral over the base valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma integer_element_isIntegral_over_base_integer_of_isIntegralClosure [ValuativeRel K]
    [ValuativeRel L] [IsIntegralClosure 𝒪[L] 𝒪[K] L] (x : 𝒪[L]) :
    IsIntegral 𝒪[K] (x : L)
lemma

algebraNorm_mem_integers_of_mem_integers_of_isIntegralClosure

L117 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.algebraNorm_mem_integers_of_mem_integers_of_isIntegralClosure
Documentation

Under an integral-closure identification, the norm of a target valuation-ring element lies in the base valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma algebraNorm_mem_integers_of_mem_integers_of_isIntegralClosure [ValuativeRel K]
    [ValuativeRel L] [IsIntegralClosure 𝒪[L] 𝒪[K] L] (x : 𝒪[L]) :
    Algebra.norm K (x : L) ∈ 𝒪[K]
lemma

integer_element_isIntegral_over_base_integer

L126 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.integer_element_isIntegral_over_base_integer
Documentation

A target valuation-ring element is integral over the base valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma integer_element_isIntegral_over_base_integer [ValuativeRel K] [ValuativeRel L]
    [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]) :
    IsIntegral 𝒪[K] (x : L)
lemma

integer_element_isIntegral_over_base_integer_of_valuativeExtension

L133 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.integer_element_isIntegral_over_base_integer_of_valuativeExtension
Documentation

A valuation-ring element in a finite valuative extension is integral over the base valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma integer_element_isIntegral_over_base_integer_of_valuativeExtension [ValuativeRel K]
    [ValuativeRel L] [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]) :
    IsIntegral 𝒪[K] (x : L)
lemma

algebraNorm_isIntegral_of_isIntegral

L139 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.algebraNorm_isIntegral_of_isIntegral
Documentation

The algebra norm of an element integral over the base ring is integral over that ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma algebraNorm_isIntegral_of_isIntegral
    {R : Type u} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L]
    {x : L} (hx : IsIntegral R x) :
    IsIntegral R (Algebra.norm K x)
lemma

mem_integers_of_isIntegral_base

L146 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.mem_integers_of_isIntegral_base
Documentation

An element of the base field integral over its valuation ring belongs to that valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma mem_integers_of_isIntegral_base [ValuativeRel K] {x : K}
    (hx : IsIntegral 𝒪[K] x) :
    x ∈ 𝒪[K]
lemma

algebraNorm_mem_integers_of_isIntegral

L154 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.algebraNorm_mem_integers_of_isIntegral
Documentation

The norm of an element integral over the base valuation ring belongs to the base valuation ring. The norm of an element integral over the base valuation ring belongs to the base valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma algebraNorm_mem_integers_of_isIntegral [ValuativeRel K]
    {x : L} (hx : IsIntegral 𝒪[K] x) :
    Algebra.norm K x ∈ 𝒪[K]
lemma

valuation_norm_le_one_of_integer

L161 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.valuation_norm_le_one_of_integer
Documentation

The norm of a target valuation-ring element has base valuation at most one.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma valuation_norm_le_one_of_integer [ValuativeRel K] {x : K}
    (hx : x ∈ 𝒪[K]) :
    ValuativeRel.valuation K x ≤ 1
lemma

algebraNorm_inv_mem_integers_of_unit

L167 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.algebraNorm_inv_mem_integers_of_unit
Documentation

The inverse norm of a target valuation-ring unit also belongs to the base valuation ring.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma algebraNorm_inv_mem_integers_of_unit [ValuativeRel K] [ValuativeRel L]
    [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]ˣ) :
    Algebra.norm K (((x⁻¹ : 𝒪[L]ˣ) : 𝒪[L]) : L) ∈ 𝒪[K]
def

normIntegerUnitsValue

L173 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normIntegerUnitsValue
Documentation

Defines normIntegerUnitsValue.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
def normIntegerUnitsValue [ValuativeRel K] [ValuativeRel L]
    [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]ˣ) : 𝒪[K]
lemma

normIntegerUnitsValue_mul_inv

L179 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normIntegerUnitsValue_mul_inv
Documentation

The norm value constructed from an integer unit multiplied by its inverse is one.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma normIntegerUnitsValue_mul_inv [ValuativeRel K] [ValuativeRel L]
    [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]ˣ) :
    normIntegerUnitsValue (K := K) (L := L) x *
      normIntegerUnitsValue (K := K) (L := L) x⁻¹ = 1
lemma

normIntegerUnitsValue_inv_mul

L194 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normIntegerUnitsValue_inv_mul
Documentation

The inverse norm value multiplied by the norm value of an integer unit is one.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma normIntegerUnitsValue_inv_mul [ValuativeRel K] [ValuativeRel L]
    [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]ˣ) :
    normIntegerUnitsValue (K := K) (L := L) x⁻¹ *
      normIntegerUnitsValue (K := K) (L := L) x = 1
def

normIntegerUnits

L209 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normIntegerUnits
Documentation

Norm restricted to valuation-integer units.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def normIntegerUnits
    (K : Type u) (L : Type v)
    [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L] [LocalFieldTheory.ValuativeExtension K L] : 𝒪[L]ˣ →* 𝒪[K]ˣ where
  toFun := fun x => {
    val := normIntegerUnitsValue (K := K) (L := L) x
    inv := normIntegerUnitsValue (K := K) (L := L) x⁻¹
    val_inv := normIntegerUnitsValue_mul_inv (K := K) (L := L) x
    inv_val := normIntegerUnitsValue_inv_mul (K := K) (L := L) x
  }
  map_one' := by
    ext
    simp [normIntegerUnitsValue]
  map_mul' := by
    intro x y
    ext
    simp [normIntegerUnitsValue]
lemma

normIntegerUnits_apply_coe

L229 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.normIntegerUnits_apply_coe
Documentation

Coercing the integer-unit norm to the base field yields the algebra norm of the original unit.

Source context 8 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section UnitNorm
variable [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma normIntegerUnits_apply_coe [ValuativeRel K] [ValuativeRel L]
    [LocalFieldTheory.ValuativeExtension K L] (x : 𝒪[L]ˣ) :
    (((normIntegerUnits K L x : 𝒪[K]ˣ) : 𝒪[K]) : K) =
      Algebra.norm K (((x : 𝒪[L]ˣ) : 𝒪[L]) : L)
lemma

mapBaseUnits_normUnits_eq_prod_gal

L247 ↗
LocalFieldTheory.IsNonarchimedeanLocalField.mapBaseUnits_normUnits_eq_prod_gal
Documentation

For a finite Galois extension, embedding the unit norm back into the extension equals the product of all Galois conjugates.

Source context 11 commands

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

namespace LocalFieldTheory
noncomputable section
universe u v
namespace IsNonarchimedeanLocalField
open scoped BigOperators ValuativeRel
variable {K : Type u} {L : Type v}
section Valuation
variable [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable [Algebra K L]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] in
Lean source · statement
lemma mapBaseUnits_normUnits_eq_prod_gal [FiniteDimensional K L] [IsGalois K L]
    (x : Lˣ) :
    mapBaseUnitsToExtensionUnits K L (normUnits K L x) =
      ∏ σ : L ≃ₐ[K] L, Units.mapEquiv σ.toMulEquiv x

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