Module

FiniteSeparableGenerator.lean

Nyll.ValuedFieldTheory.Valuation.Completion.FiniteSeparableGenerator

1 declaration indexed from sourceView source ↗

Module documentation

Generators of finite extensions over a dense subfield

Embed a finite separable extension into an algebraic closure of its base. The generator descended there belongs to the image of the extension, so it pulls back to a generator of the original field with the same degree.

Imports4

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableGeneratorDescent
Mathlib.FieldTheory.PrimitiveElement
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.RingTheory.PowerBasis

Imported by2

theorem

exists_isSeparable_generator_of_denseRange

L26 ↗

ValuationTheory.Completion.exists_isSeparable_generator_of_denseRange

Documentation

A finite separable extension of a complete nonarchimedean field has a generator separable over any dense subfield, of the same degree.

Source context 2 commands

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

namespace ValuationTheory.Completion
open IntermediateField

Lean source · statement

theorem exists_isSeparable_generator_of_denseRange
    {K A E : Type*} [Field K] [NontriviallyNormedField A] [Field E]
    [CompleteSpace A] [IsUltrametricDist A]
    [Algebra K A] [Algebra A E] [Algebra K E] [IsScalarTower K A E]
    [FiniteDimensional A E] [Algebra.IsSeparable A E]
    (hd : DenseRange (algebraMap K A)) :
    ∃ γ : E, IsSeparable K γ ∧ Algebra.adjoin A ({γ} : Set E) = ⊤ ∧
      (minpoly K γ).natDegree = Module.finrank A E

Module documentation

Generators of finite extensions over a dense subfield

Declarations

exists_isSeparable_generator_of_denseRange