Module

DVFFiniteExtensionDescent.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFFiniteExtensionDescent

3 declarations indexed from sourceView source ↗

Module documentation

Descending finite separable extensions of a valuation completion

A generator separable over the original field gives a finite separable intermediate field. Its scalar extension maps onto the given extension of the completion, and the equality of degrees makes this actual map injective.

Imports6

Nyll.ValuedFieldTheory.Valuation.Completion.DVFFiniteSeparableGenerator
Mathlib.FieldTheory.SeparableClosure
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

def

completionIntermediateFieldTensorHom

L33 ↗

ValuationTheory.DiscreteValuationField.DVF.completionIntermediateFieldTensorHom

Documentation

The tensor map obtained from the two given embeddings into E.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open IntermediateField
open scoped TensorProduct
variable {K : Type*} [Field K] (base : DVF K)

Lean source · statement

def completionIntermediateFieldTensorHom
    {E : Type*} [Field E] [Algebra base.valuation.Completion E]
    [Algebra K E] [IsScalarTower K base.valuation.Completion E]
    (F : IntermediateField K E) :
    base.valuation.Completion ⊗[K] F →ₐ[base.valuation.Completion] E

theorem

completionIntermediateFieldTensorHom_tmul

L42 ↗

ValuationTheory.DiscreteValuationField.DVF.completionIntermediateFieldTensorHom_tmul

Documentation

The tensor map multiplies the canonical images of the two factors.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open IntermediateField
open scoped TensorProduct
variable {K : Type*} [Field K] (base : DVF K)

Lean source · statement

theorem completionIntermediateFieldTensorHom_tmul
    {E : Type*} [Field E] [Algebra base.valuation.Completion E]
    [Algebra K E] [IsScalarTower K base.valuation.Completion E]
    (F : IntermediateField K E) (a : base.valuation.Completion) (x : F) :
    completionIntermediateFieldTensorHom base F (a ⊗ₜ[K] x) =
      algebraMap base.valuation.Completion E a * (x : E)

theorem

exists_finiteSeparable_completion_descent

L53 ↗

ValuationTheory.DiscreteValuationField.DVF.exists_finiteSeparable_completion_descent

Documentation

Every finite separable extension of the actual valuation completion is the scalar extension of a finite separable intermediate field over K.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
open IntermediateField
open scoped TensorProduct
variable {K : Type*} [Field K] (base : DVF K)

Lean source · statement

theorem exists_finiteSeparable_completion_descent
    (E : Type*) [Field E] [Algebra base.valuation.Completion E]
    [Algebra K E] [IsScalarTower K base.valuation.Completion E]
    [FiniteDimensional base.valuation.Completion E]
    [Algebra.IsSeparable base.valuation.Completion E] :
    ∃ F : IntermediateField K E, FiniteDimensional K F ∧ Algebra.IsSeparable K F ∧
      Function.Bijective (completionIntermediateFieldTensorHom base F)

Module documentation

Descending finite separable extensions of a valuation completion

Declarations

completionIntermediateFieldTensorHom

completionIntermediateFieldTensorHom_tmul

exists_finiteSeparable_completion_descent