Module

DVFSeparableClosedTensor.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFSeparableClosedTensor

3 declarations indexed from sourceView source ↗

Module documentation

The tensor map from an embedded separably closed field

Multiplication of the two given embeddings is surjective because the embedded separably closed field generates the separable extension of the valuation completion. No Henselian hypothesis is used for surjectivity.

Imports2

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

Imported by2

def

separableClosedTensorHom

L30 ↗

ValuationTheory.DiscreteValuationField.DVF.separableClosedTensorHom

Documentation

Multiplication of the completion embedding and a given K-embedding.

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 : 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

def separableClosedTensorHom (i : S →ₐ[K] E) :
    base.valuation.Completion ⊗[K] S →ₐ[base.valuation.Completion] E

theorem

separableClosedTensorHom_tmul

L36 ↗

ValuationTheory.DiscreteValuationField.DVF.separableClosedTensorHom_tmul

Documentation

The actual tensor map preserves the specified embeddings.

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 : 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 separableClosedTensorHom_tmul (i : S →ₐ[K] E)
    (a : base.valuation.Completion) (s : S) :
    base.separableClosedTensorHom i (a ⊗ₜ[K] s) =
      algebraMap base.valuation.Completion E a * i s

theorem

separableClosedTensorHom_surjective

L45 ↗

ValuationTheory.DiscreteValuationField.DVF.separableClosedTensorHom_surjective

Documentation

A separably closed image generates the whole separable extension of the completion, so its actual tensor map is surjective.

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 : 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 separableClosedTensorHom_surjective [IsSepClosed S]
    [Algebra.IsSeparable base.valuation.Completion E] (i : S →ₐ[K] E) :
    Function.Surjective (base.separableClosedTensorHom i)

Module documentation

The tensor map from an embedded separably closed field

Declarations

separableClosedTensorHom

separableClosedTensorHom_tmul

separableClosedTensorHom_surjective