ValuationTheory.DiscreteValuationField.DVF.adjoin_range_eq_top_of_isSepClosed
An embedded separably closed extension of the original field generates every separable extension of the valuation completion containing its image. The original field need not be Henselian.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K : Type*} [Field K] (base : DVF K)Lean source · statement
theorem adjoin_range_eq_top_of_isSepClosed
{S E : Type*} [Field S] [Field E] [Algebra K S]
[Algebra base.valuation.Completion E] [Algebra K E]
[IsScalarTower K base.valuation.Completion E] [IsSepClosed S]
[Algebra.IsSeparable base.valuation.Completion E] (i : S →ₐ[K] E) :
Algebra.adjoin base.valuation.Completion (Set.range i) = ⊤