NYLL
Module

Localization.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Localization
7 declarations indexed from sourceView source ↗

Module documentation

Discrete valuations from localized finite integral closures

The actual localization constructed in LocalizationRing is a DVR in a finite separable extension. Its canonical fraction-field valuation extends the given base valuation, without completeness or Henselian assumptions.

Imports6
Imported by6

Declarations

theorem

normalization_isDedekindDomain

L34 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.normalization_isDedekindDomain
Documentation

The integral closure of a DVR in a finite separable extension is Dedekind.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
attribute [local instance] localization_isLocalization
Lean source · statement
theorem normalization_isDedekindDomain (base : DVF.{u, v} K) :
    IsDedekindDomain (Normalization (L := L) base)
theorem

normalization_isFractionRing

L44 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.normalization_isFractionRing
Documentation

The actual integral closure has the extension field as its fraction field.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
attribute [local instance] localization_isLocalization
omit [Algebra.IsSeparable K L] in
Lean source · statement
theorem normalization_isFractionRing (base : DVF.{u, v} K) :
    IsFractionRing (Normalization (L := L) base) L
theorem

localization_isDiscreteValuationRing

L51 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.localization_isDiscreteValuationRing
Documentation

Localization at the chosen nonzero prime produces a DVR.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
attribute [local instance] localization_isLocalization
Lean source · statement
theorem localization_isDiscreteValuationRing (base : DVF.{u, v} K) :
    IsDiscreteValuationRing (LocalizationRing (L := L) base)
theorem

localization_isFractionRing

L59 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.localization_isFractionRing
Documentation

The localization keeps the extension field as its fraction field.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
attribute [local instance] localization_isLocalization
omit [Algebra.IsSeparable K L] in
Lean source · statement
theorem localization_isFractionRing (base : DVF.{u, v} K) :
    IsFractionRing (LocalizationRing (L := L) base) L
def

dvf

L69 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.dvf
Documentation

A finite separable extension carries the discrete valuation of the localized integral closure.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
attribute [local instance] localization_isLocalization
attribute [local instance] localization_isDiscreteValuationRing localization_isFractionRing
Lean source · full declaration
def dvf (base : DVF.{u, v} K) : DVF.{w, 0} L where
  ValueGroup := WithZero (Multiplicative ℤ)
  valuation := (IsDiscreteValuationRing.maximalIdeal (LocalizationRing (L := L) base)).valuation L
theorem

dvf_valuation

L74 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.dvf_valuation
Documentation

The constructed valuation is the normalized valuation of the chosen localization.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
attribute [local instance] localization_isLocalization
attribute [local instance] localization_isDiscreteValuationRing localization_isFractionRing
Lean source · statement
theorem dvf_valuation (base : DVF.{u, v} K) :
    (dvf (L := L) base).valuation =
      (IsDiscreteValuationRing.maximalIdeal (LocalizationRing (L := L) base)).valuation L
theorem

dvf_hasExtension

L80 ↗
ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.dvf_hasExtension
Documentation

The constructed discrete valuation extends the original valuation on the base field.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization
universe u v w
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
attribute [local instance] localization_isLocalization
attribute [local instance] localization_isDiscreteValuationRing localization_isFractionRing
Lean source · statement
theorem dvf_hasExtension (base : DVF.{u, v} K) :
    base.valuation.HasExtension (dvf (L := L) base).valuation

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