Module

AlgebraicExtensionUniqueness.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.AlgebraicExtensionUniqueness

2 declarations indexed from sourceView source ↗

Module documentation

Uniqueness over an algebraic extension of a Henselian valued field

The integral closure is an actual valuation ring. Every extension valuation has this ring of integers, so any two extension valuations are equivalent.

Imports2

Imported by7

theorem

valuationSubring_eq_integralClosure_of_henselianRing

L24 ↗

ValuationTheory.Henselian.valuationSubring_eq_integralClosure_of_henselianRing

Documentation

The valuation ring of any algebraic extension valuation is the actual integral closure of the Henselian base valuation ring.

Source context 2 commands

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

namespace ValuationTheory.Henselian
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L]
  (V : ValuationSubring K) [HenselianRing V (IsLocalRing.maximalIdeal V)]

Lean source · statement

theorem valuationSubring_eq_integralClosure_of_henselianRing
    {Γ : Type*} [LinearOrderedCommGroupWithZero Γ]
    (w : _root_.Valuation L Γ) [V.valuation.HasExtension w] :
    w.valuationSubring.toSubring = (integralClosure V L).toSubring

theorem

valuationSubring_eq_of_henselianRing

L42 ↗

ValuationTheory.Henselian.valuationSubring_eq_of_henselianRing