Module

AlgebraicExtensionHenselian.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.AlgebraicExtensionHenselian

1 declaration indexed from sourceView source ↗

Module documentation

Henselianity of algebraic extension valuation rings

Chevalley's theorem supplies an extension over every further algebraic field. Uniqueness over the original Henselian base makes this extension unique. The valuation-ring criterion then supplies Henselianity upstairs.

Imports2

Imported by4

theorem

henselianRing_of_algebraic_extension

L27 ↗

ValuationTheory.Henselian.henselianRing_of_algebraic_extension

Documentation

An algebraic extension of a Henselian valuation ring is Henselian, without rank, discreteness, completeness, or separability assumptions.

Source context 3 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)]
  (W : ValuationSubring L) [V.valuation.HasExtension W.valuation]
include V in

Lean source · statement

theorem henselianRing_of_algebraic_extension :
    HenselianRing W (IsLocalRing.maximalIdeal W)

Module documentation

Henselianity of algebraic extension valuation rings

Declarations

henselianRing_of_algebraic_extension