Valuation rings and Henselian rings

Discrete valuation rings and general valuation rings, their completions and finite extensions, residue fields, Hensel's lemma and the Krull–Akizuki theorem.

• Discrete valuation rings as power series quotients
• Discrete valuation rings at height-one primes
• Henselian rings and Hensel's lemma
• Finite extensions of complete discrete valuation rings
• Krull–Akizuki theorem
• Residue fields of valuation rings

TheoremValuation rings of one-variable function fields are PIDs#✓fully proved

A valuation subring of a function field in one variable over K, containing K and different from the whole field, is a principal ideal ring.

theorem ValuationSubring.isPrincipalIdealRing_of_finiteDimensional_adjoin {K F : Type*} [Field K]
    [Field F] [Algebra K F] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (O : ValuationSubring F) (hK : ∀ a : K, algebraMap K F a ∈ O) (hO : O ≠ ⊤) :
    IsPrincipalIdealRing O

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.