Module

HenselianSeparableClosedTensor.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableClosedTensor

3 declarations indexed from sourceView source ↗

Module documentation

Comparing separable closures across Henselian completion

The actual tensor map is injective because its source is a field, and surjective by descent of finite separable generators. In particular it applies to the usual lift between the two separable closures.

Imports3

Nyll.ValuedFieldTheory.Valuation.Completion.DVFSeparableClosedTensor
Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableTensorField
Mathlib.Algebra.Algebra.Equiv

Imported by3

theorem

separableClosedTensorHom_injective

L32 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosedTensorHom_injective

Documentation

The tensor map of a separable extension of the Henselian base is injective into any field containing the two specified embeddings.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped TensorProduct
variable {K : Type*} [Field K] (base : HenselianDVF 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] [Algebra.IsSeparable K S]

Lean source · statement

theorem separableClosedTensorHom_injective (i : S →ₐ[K] E) :
    Function.Injective (base.toDVF.separableClosedTensorHom i)

def

separableClosedTensorEquiv

L41 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosedTensorEquiv

Documentation

Scalar extension of a separably closed separable extension of K is the given separable extension of its completion. The map retains the chosen embedding, rather than taking an unrelated field isomorphism.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped TensorProduct
variable {K : Type*} [Field K] (base : HenselianDVF 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] [Algebra.IsSeparable K S]

Lean source · statement

def separableClosedTensorEquiv [IsSepClosed S]
    [Algebra.IsSeparable base.valuation.Completion E] (i : S →ₐ[K] E) :
    base.valuation.Completion ⊗[K] S ≃ₐ[base.valuation.Completion] E

theorem

separableClosedTensorEquiv_tmul

L50 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.separableClosedTensorEquiv_tmul

Documentation

The comparison is the product of the actual completion embedding and the chosen embedding of the separably closed field.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped TensorProduct
variable {K : Type*} [Field K] (base : HenselianDVF 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] [Algebra.IsSeparable K S]

Lean source · statement

theorem separableClosedTensorEquiv_tmul [IsSepClosed S]
    [Algebra.IsSeparable base.valuation.Completion E] (i : S →ₐ[K] E)
    (a : base.valuation.Completion) (s : S) :
    base.separableClosedTensorEquiv i (a ⊗ₜ[K] s) =
      algebraMap base.valuation.Completion E a * i s

Module documentation

Comparing separable closures across Henselian completion

Declarations

separableClosedTensorHom_injective

separableClosedTensorEquiv

separableClosedTensorEquiv_tmul