Module

DVFFiniteSeparableImage.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFFiniteSeparableImage

1 declaration indexed from sourceView source ↗

Module documentation

Finite images over the actual valuation completion

The image of a finite extension is contained in the field generated by the images of a finite linear basis. Those images remain integral after extending the scalars to the completion. Neither Henselianity nor separability is needed.

Imports5

Nyll.ValuedFieldTheory.Valuation.Completion.WithValScalars
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Basic
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.LinearAlgebra.Dimension.Free
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Imported by1

Nyll.ValuedFieldTheory.Valuation.Completion.All

theorem

finiteDimensional_adjoin_image

L31 ↗

ValuationTheory.DiscreteValuationField.DVF.finiteDimensional_adjoin_image

Documentation

Adjoining the image of a finite intermediate field to the actual completion gives a finite extension of that completion.

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)
  {S E : Type*} [Field S] [Field E] [Algebra K S]
  [Algebra base.valuation.Completion E] [Algebra K E]
  [IsScalarTower K base.valuation.Completion E]

Lean source · statement

theorem finiteDimensional_adjoin_image (i : S →ₐ[K] E)
    (F : IntermediateField K S) [FiniteDimensional K F] :
    FiniteDimensional base.valuation.Completion
      (IntermediateField.adjoin base.valuation.Completion (i '' (F : Set S)))

Module documentation

Finite images over the actual valuation completion

Declarations

finiteDimensional_adjoin_image