Module

DVFCompletedExtensionRealization.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFCompletedExtensionRealization

2 declarations indexed from sourceView source ↗

Module documentation

Realizing finite extensions as actual valuation completions

The descended intermediate field receives the discrete valuation of its localized integral closure. The two actual tensor maps identify its completion with the prescribed extension, preserving both embeddings.

Imports4

Imported by1

Nyll.ValuedFieldTheory.Valuation.Completion.All

theorem

completion_equiv_of_tensor_equiv

L29 ↗

ValuationTheory.DiscreteValuationField.DVF.completion_equiv_of_tensor_equiv

Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
universe u v w
variable {K : Type u} [Field K] (base : DVF.{u, v} K)

Lean source · statement

theorem completion_equiv_of_tensor_equiv
    {L E : Type*} [Field L] [Field E] [Algebra K L] [FiniteDimensional K L]
    [Algebra base.valuation.Completion E]
    (target : DVF L) [hExtension : base.valuation.HasExtension target.valuation]
    (e : base.valuation.Completion ⊗[K] L ≃ₐ[base.valuation.Completion] E) :
    ∃ c : @AlgEquiv base.valuation.Completion target.valuation.Completion E _ _ _
        (completionAlgebra base target) _,
      ∀ x : L, c (x : target.valuation.Completion) = e (1 ⊗ₜ[K] x)

theorem

exists_completed_extension_realization

L56 ↗

ValuationTheory.DiscreteValuationField.DVF.exists_completed_extension_realization

Documentation

A finite separable extension of a valuation completion is the actual completion of a finite separable intermediate field with an extending DVF. The isomorphism is over the base completion and fixes that intermediate field.