Module

DVFHomExtension.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFHomExtension

3 declarations indexed from sourceView source ↗

Module documentation

Extending field homomorphisms to actual valuation completions

Scalar extension of the original homomorphism, transported through the actual tensor comparison, gives a homomorphism over the base completion. Only the source extension needs to be finite and separable.

Imports2

Nyll.ValuedFieldTheory.Valuation.Completion.DVFTensorMap
Mathlib.RingTheory.TensorProduct.Maps

Imported by3

instance

(anonymous instance)

L33 ↗

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : DVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.valuation.HasExtension targetL.valuation]
  [hM : base.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
  [HenselianRing base.valuationSubring base.maximalIdeal]

Lean source · statement

instance : Algebra base.valuation.Completion targetL.valuation.Completion

def

extendCompletionAlgHom

L38 ↗

ValuationTheory.DiscreteValuationField.DVF.extendCompletionAlgHom

Documentation

Extending a homomorphism from a finite separable extension of a Henselian DVF to the actual completions. The target extension need not be finite.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : DVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.valuation.HasExtension targetL.valuation]
  [hM : base.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
  [HenselianRing base.valuationSubring base.maximalIdeal]
local instance : Algebra base.valuation.Completion targetL.valuation.Completion :=
  completionAlgebra base targetL

Lean source · statement

def extendCompletionAlgHom (f : L →ₐ[K] M) :
    @AlgHom base.valuation.Completion targetL.valuation.Completion
      targetM.valuation.Completion _ _ _
      (completionAlgebra base targetL) (completionAlgebra base targetM)

theorem

extendCompletionAlgHom_coe

L48 ↗

ValuationTheory.DiscreteValuationField.DVF.extendCompletionAlgHom_coe

Documentation

The extended homomorphism agrees with the original homomorphism on its field.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : DVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.valuation.HasExtension targetL.valuation]
  [hM : base.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
  [HenselianRing base.valuationSubring base.maximalIdeal]
local instance : Algebra base.valuation.Completion targetL.valuation.Completion :=
  completionAlgebra base targetL

Lean source · statement

theorem extendCompletionAlgHom_coe (f : L →ₐ[K] M) (x : L) :
    extendCompletionAlgHom base targetL targetM f (x : targetL.valuation.Completion) =
      (f x : targetM.valuation.Completion)

Module documentation

Extending field homomorphisms to actual valuation completions

Declarations

(anonymous instance)

extendCompletionAlgHom

extendCompletionAlgHom_coe