Module

DVFFiniteSeparableGenerator.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFFiniteSeparableGenerator

1 declaration indexed from sourceView source ↗

Module documentation

Descending generators from the actual completion of a DVF

The original valuation supplies a norm with the same uniformity on WithVal. Its completion is therefore the given valuation completion. Density of the canonical ground-field map then descends finite separable generators.

Imports6

Nyll.ValuedFieldTheory.Valuation.Completion.FiniteSeparableGenerator
Nyll.ValuedFieldTheory.Valuation.Completion.WithValScalars
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.NormedModel
Mathlib.Analysis.Normed.Algebra.Ultra
Mathlib.Analysis.Normed.Module.Completion
Mathlib.Topology.Algebra.Valued.NormedValued

Imported by3

theorem

exists_completion_extension_generator

L31 ↗

ValuationTheory.DiscreteValuationField.DVF.exists_completion_extension_generator

Documentation

Every finite separable extension of the actual valuation completion has a generator separable over the original field, with the same degree. The ground field need not be Henselian or complete.

Source context 3 commands

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

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

Lean source · statement

theorem exists_completion_extension_generator (base : DVF.{u, v} K)
    (E : Type w) [Field E] [Algebra base.valuation.Completion E]
    [Algebra K E] [IsScalarTower K base.valuation.Completion E]
    [FiniteDimensional base.valuation.Completion E]
    [Algebra.IsSeparable base.valuation.Completion E] :
    ∃ γ : E, IsSeparable K γ ∧
      Algebra.adjoin base.valuation.Completion ({γ} : Set E) = ⊤ ∧
      (minpoly K γ).natDegree = Module.finrank base.valuation.Completion E

Module documentation

Descending generators from the actual completion of a DVF

Declarations

exists_completion_extension_generator