Module

Henselian.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.Henselian

3 declarations indexed from sourceView source ↗

Module documentation

Actual Henselian discrete valuation extensions

The localized integral closure constructs a discrete extension valuation. Henselianity follows from the simple-root condition on the base valuation ring and uniqueness along algebraic field towers.

Imports3

Imported by9

theorem

henselianRing_of_hasExtension

L27 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.henselianRing_of_hasExtension

Documentation

Any discrete valuation extending a Henselian valuation across an algebraic field extension has a Henselian valuation ring.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v w x
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem HenselianDVF.henselianRing_of_hasExtension [Algebra.IsAlgebraic K L]
    (base : HenselianDVF.{u, v} K) (target : DVF.{w, x} L)
    [base.toDVF.valuation.HasExtension target.valuation] :
    HenselianRing target.valuationSubring target.maximalIdeal

def

henselianDVF

L48 ↗

ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.henselianDVF

Documentation

A finite separable extension of a Henselian DVF has an actual Henselian discrete valuation, obtained from its localized integral closure.

Source context 5 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v w x
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
namespace FiniteExtensionLocalization
variable [FiniteDimensional K L] [Algebra.IsSeparable K L]

Lean source · full declaration

def henselianDVF (base : HenselianDVF.{u, v} K) : HenselianDVF.{w, 0} L where
  toDVF := dvf base.toDVF
  instHenselian := by
    have : base.toDVF.valuation.HasExtension (dvf (L := L) base.toDVF).valuation :=
      dvf_hasExtension base.toDVF
    exact base.henselianRing_of_hasExtension (dvf base.toDVF)

theorem

henselianDVF_hasExtension

L56 ↗

ValuationTheory.DiscreteValuationField.FiniteExtensionLocalization.henselianDVF_hasExtension

Documentation

The constructed Henselian discrete valuation extends the base valuation.

Source context 5 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v w x
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
namespace FiniteExtensionLocalization
variable [FiniteDimensional K L] [Algebra.IsSeparable K L]

Lean source · statement

theorem henselianDVF_hasExtension (base : HenselianDVF.{u, v} K) :
    base.toDVF.valuation.HasExtension (henselianDVF (L := L) base).toDVF.valuation

Module documentation

Actual Henselian discrete valuation extensions

Declarations

henselianRing_of_hasExtension

henselianDVF

henselianDVF_hasExtension