NYLL
Module

DVFTensorMap.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFTensorMap
15 declarations indexed from sourceView source ↗

Module documentation

The tensor map for an extension of discrete valuations

The map of completions supplies the scalar algebra. Multiplication then gives the actual tensor map to the completion of the extension field.

Class-valued statements specify this algebra's scalar action explicitly, avoiding a search through the completion's general scalar-action instance. The module-local algebra is the same data, used to elaborate the proofs.

Imports8
Imported by8

Declarations

def

completionAlgebra

L38 ↗
ValuationTheory.DiscreteValuationField.DVF.completionAlgebra
Documentation

The scalar algebra given by the actual map of valuation completions.

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 : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
Lean source · statement
def completionAlgebra :
    Algebra base.valuation.Completion target.valuation.Completion
instance

(anonymous instance)

L42 ↗
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 : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
Lean source · statement
instance : UniformContinuousConstSMul K (WithVal target.valuation)
instance

(anonymous instance)

L45 ↗
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 : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
Lean source · statement
instance : Algebra base.valuation.Completion target.valuation.Completion
theorem

completion_isScalarTower

L49 ↗
ValuationTheory.DiscreteValuationField.DVF.completion_isScalarTower
Documentation

The completion scalar map commutes with the original ground-field map.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem completion_isScalarTower :
    @IsScalarTower K base.valuation.Completion target.valuation.Completion
      _ (completionAlgebra base target).toSMul _
theorem

completion_continuousSMul

L60 ↗
ValuationTheory.DiscreteValuationField.DVF.completion_continuousSMul
Documentation

Scalar multiplication by the ground-field completion is continuous.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem completion_continuousSMul :
    @ContinuousSMul base.valuation.Completion target.valuation.Completion
      (completionAlgebra base target).toSMul _ _
def

toCompletionAlgHom

L69 ↗
ValuationTheory.DiscreteValuationField.DVF.toCompletionAlgHom
Documentation

The embedding of the extension field into its completion, over the original base.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · full declaration
def toCompletionAlgHom : L →ₐ[K] target.valuation.Completion where
  __ := algebraMap L target.valuation.Completion
  commutes' _ := rfl
def

completionMapAlgHom

L73 ↗
ValuationTheory.DiscreteValuationField.DVF.completionMapAlgHom
Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · full declaration
def completionMapAlgHom :
    base.valuation.Completion →ₐ[K] target.valuation.Completion where
  __ := completionMap base target
  commutes' k := completionMap_coe_base base target k
def

completionTensorHom

L79 ↗
ValuationTheory.DiscreteValuationField.DVF.completionTensorHom
Documentation

Multiplication defines the canonical tensor map into the extension completion.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · full declaration
def completionTensorHom :
    @AlgHom base.valuation.Completion (base.valuation.Completion ⊗[K] L)
      target.valuation.Completion _ _ _ _ (completionAlgebra base target) where
  __ := (Algebra.TensorProduct.lift (R := K) (S := K)
    (completionMapAlgHom base target) (toCompletionAlgHom (K := K) target)
    (fun a l => Commute.all (completionMap base target a)
      (toCompletionAlgHom (K := K) target l))).toRingHom
  commutes' a := by
    change Algebra.TensorProduct.lift (R := K) (S := K)
      (completionMapAlgHom base target) (toCompletionAlgHom (K := K) target)
      (fun b l => Commute.all (completionMap base target b)
        (toCompletionAlgHom (K := K) target l)) (a ⊗ₜ[K] 1) = completionMap base target a
    exact (Algebra.TensorProduct.lift_tmul (R := K) (S := K)
      (completionMapAlgHom base target) (toCompletionAlgHom (K := K) target)
      (fun b l => Commute.all (completionMap base target b)
        (toCompletionAlgHom (K := K) target l)) a 1).trans
      (by rw [map_one, mul_one]; rfl)
theorem

completionTensorHom_tmul

L98 ↗
ValuationTheory.DiscreteValuationField.DVF.completionTensorHom_tmul
Documentation

The tensor map sends a pure tensor to the product of the two canonical images.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem completionTensorHom_tmul (a : base.valuation.Completion) (l : L) :
    completionTensorHom base target (a ⊗ₜ[K] l) =
      completionMap base target a * (l : target.valuation.Completion)
theorem

completionTensorHom_surjective

L108 ↗
ValuationTheory.DiscreteValuationField.DVF.completionTensorHom_surjective
Documentation

The canonical tensor map is onto for every finite extension of discrete valuations. Only the ground-field completion is normed in the proof.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem completionTensorHom_surjective [FiniteDimensional K L] :
    Function.Surjective (completionTensorHom base target)
theorem

completion_finiteDimensional

L149 ↗
ValuationTheory.DiscreteValuationField.DVF.completion_finiteDimensional
Documentation

Every finite extension of discrete valuations gives a finite extension of their actual completions.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem completion_finiteDimensional [FiniteDimensional K L] :
    @FiniteDimensional base.valuation.Completion target.valuation.Completion _ _
      (completionAlgebra base target).toModule
theorem

completionTensorHom_injective

L157 ↗
ValuationTheory.DiscreteValuationField.DVF.completionTensorHom_injective
Documentation

For a finite separable extension of a Henselian DVF, the canonical tensor map is injective because its actual source is a field.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem completionTensorHom_injective [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [HenselianRing base.valuationSubring base.maximalIdeal] :
    Function.Injective (completionTensorHom base target)
def

completionTensorEquiv

L167 ↗
ValuationTheory.DiscreteValuationField.DVF.completionTensorEquiv
Documentation

Completing a finite separable extension of a Henselian DVF is scalar extension along the actual map of ground-field completions.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
def completionTensorEquiv [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [HenselianRing base.valuationSubring base.maximalIdeal] :
    @AlgEquiv base.valuation.Completion (base.valuation.Completion ⊗[K] L)
      target.valuation.Completion _ _ _ _ (completionAlgebra base target)
theorem

completionTensorEquiv_tmul

L175 ↗
ValuationTheory.DiscreteValuationField.DVF.completionTensorEquiv_tmul
Documentation

The completion equivalence retains the prescribed embeddings of both fields.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem completionTensorEquiv_tmul [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [HenselianRing base.valuationSubring base.maximalIdeal]
    (a : base.valuation.Completion) (l : L) :
    completionTensorEquiv base target (a ⊗ₜ[K] l) =
      completionMap base target a * (l : target.valuation.Completion)
theorem

finrank_completion

L184 ↗
ValuationTheory.DiscreteValuationField.DVF.finrank_completion
Documentation

A finite separable extension of a Henselian DVF has the same degree after completing both valued fields.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open scoped TensorProduct
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : DVF K) (target : DVF L)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : UniformContinuousConstSMul K (WithVal target.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra target.valuation
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  completionAlgebra base target
Lean source · statement
theorem finrank_completion [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [HenselianRing base.valuationSubring base.maximalIdeal] :
    @Module.finrank base.valuation.Completion target.valuation.Completion _ _
      (completionAlgebra base target).toModule =
      Module.finrank K L

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.