Module

SeparableGeneratorDescent.lean

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableGeneratorDescent

1 declaration indexed from sourceView source ↗

Module documentation

Descending separable generators to a dense subfield

A nearby root supplied by polynomial approximation generates the same extension as the original separable element. Comparing the degrees also shows that the new generator is separable over the dense subfield, with the original extension degree.

Imports8

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableRootApproximation
Mathlib.FieldTheory.IntermediateField.Algebraic
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.Minpoly.Field
Mathlib.FieldTheory.Separable
Mathlib.FieldTheory.SeparableClosure
Mathlib.Algebra.Polynomial.Div
Mathlib.Algebra.Polynomial.Lifts

Imported by2

theorem

exists_isSeparable_adjoin_eq_of_denseRange

L31 ↗

ValuationTheory.Completion.exists_isSeparable_adjoin_eq_of_denseRange

Documentation

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

Source context 2 commands

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

namespace ValuationTheory.Completion
open Polynomial IntermediateField

Lean source · statement

theorem exists_isSeparable_adjoin_eq_of_denseRange
    {K A : Type*} [Field K] [NontriviallyNormedField A]
    [CompleteSpace A] [IsUltrametricDist A] [Algebra K A]
    (hd : DenseRange (algebraMap K A)) (α : AlgebraicClosure A)
    (hα : IsSeparable A α) :
    ∃ β : AlgebraicClosure A, IsSeparable K β ∧ A⟮β⟯ = A⟮α⟯ ∧
      (minpoly K β).natDegree = (minpoly A α).natDegree

Module documentation

Descending separable generators to a dense subfield

Declarations

exists_isSeparable_adjoin_eq_of_denseRange