Module

HenselianDVF.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianDVF

1 declaration indexed from sourceView source ↗

Module documentation

Separable algebraic closedness in the completion of a Henselian DVF

The normed model comes from the given discrete valuation. Its unit ball is isomorphic to the original Henselian valuation ring, so the normed completion theorem applies to the actual valuation completion.

Imports5

Imported by3

theorem

exists_completion_eq_of_isSeparable

L29 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.exists_completion_eq_of_isSeparable

Documentation

A Henselian discretely valued field is separably algebraically closed in its valuation completion. No completeness or residue-field finiteness is assumed.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
universe u v
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_completion_eq_of_isSeparable (base : HenselianDVF.{u, v} K)
    (a : base.valuation.Completion) (ha : IsSeparable K a) :
    ∃ k : K, (k : base.valuation.Completion) = a

Module documentation

Separable algebraic closedness in the completion of a Henselian DVF

Declarations

exists_completion_eq_of_isSeparable