Module

HenselianFiniteImageCompletion.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianFiniteImageCompletion

6 declarations indexed from sourceView source ↗

Module documentation

Completing the same finite intermediate field

The range of the actual tensor map is the field generated by the image of an algebraic intermediate field. For a finite separable intermediate field of a Henselian DVF, this identifies its own valuation completion with that field, preserving every element of the prescribed intermediate field.

Imports5

Nyll.ValuedFieldTheory.Valuation.Completion.DVFTensorMap
Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableClosedTensor
Mathlib.Algebra.Algebra.Subalgebra.Basic
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Imported by1

Nyll.ValuedFieldTheory.Valuation.Completion.All

theorem

separableClosedTensorHom_range_adjoin_image

L36 ↗

ValuationTheory.DiscreteValuationField.DVF.separableClosedTensorHom_range_adjoin_image

Documentation

The actual tensor map has exactly the field generated by the prescribed intermediate-field image as its range. Algebraicity suffices here.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace ValuationTheory.DiscreteValuationField.DVF
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_range_adjoin_image (i : S →ₐ[K] E)
    (F : IntermediateField K S) [Algebra.IsAlgebraic K F] :
    (base.separableClosedTensorHom (i.comp F.val)).range =
      (IntermediateField.adjoin base.valuation.Completion (i '' (F : Set S))).toSubalgebra

def

completionTensorImageEquiv

L79 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionTensorImageEquiv

Documentation

Scalar extension of a prescribed separable intermediate field is the field generated by its image under the given embedding.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
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]
  (i : S →ₐ[K] E) (F : IntermediateField K S) [Algebra.IsSeparable K F]

Lean source · statement

def completionTensorImageEquiv :
    base.valuation.Completion ⊗[K] F ≃ₐ[base.valuation.Completion]
      IntermediateField.adjoin base.valuation.Completion (i '' (F : Set S))

theorem

completionTensorImageEquiv_tmul

L88 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionTensorImageEquiv_tmul

Documentation

This range identification is multiplication of the two specified maps.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
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]
  (i : S →ₐ[K] E) (F : IntermediateField K S) [Algebra.IsSeparable K F]

Lean source · statement

theorem completionTensorImageEquiv_tmul (a : base.valuation.Completion) (x : F) :
    (base.completionTensorImageEquiv i F (a ⊗ₜ[K] x) : E) =
      algebraMap base.valuation.Completion E a * i (x : S)

instance

(anonymous instance)

L96 ↗

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
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]
  (i : S →ₐ[K] E) (F : IntermediateField K S) [Algebra.IsSeparable K F]
variable [FiniteDimensional K F] (target : DVF F)
  [hExtension : base.valuation.HasExtension target.valuation]

Lean source · statement

instance : Algebra base.valuation.Completion target.valuation.Completion

def

completionAdjoinImageEquiv

L101 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionAdjoinImageEquiv

Documentation

The completion of the same finite intermediate field is its image field. The source algebra is supplied by the actual map of valuation completions.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
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]
  (i : S →ₐ[K] E) (F : IntermediateField K S) [Algebra.IsSeparable K F]
variable [FiniteDimensional K F] (target : DVF F)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  DVF.completionAlgebra base.toDVF target

Lean source · statement

def completionAdjoinImageEquiv :
    @AlgEquiv base.valuation.Completion target.valuation.Completion
      (IntermediateField.adjoin base.valuation.Completion (i '' (F : Set S)))
      _ _ _ (DVF.completionAlgebra base.toDVF target) _

theorem

completionAdjoinImageEquiv_coe

L109 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionAdjoinImageEquiv_coe

Documentation

The comparison preserves the original inclusion of each element of F.

Source context 6 commands

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

noncomputable section
open scoped TensorProduct
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
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]
  (i : S →ₐ[K] E) (F : IntermediateField K S) [Algebra.IsSeparable K F]
variable [FiniteDimensional K F] (target : DVF F)
  [hExtension : base.valuation.HasExtension target.valuation]
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  DVF.completionAlgebra base.toDVF target

Lean source · statement

theorem completionAdjoinImageEquiv_coe (x : F) :
    (base.completionAdjoinImageEquiv i F target (x : target.valuation.Completion) : E) =
      i (x : S)

Module documentation

Completing the same finite intermediate field

Declarations

separableClosedTensorHom_range_adjoin_image

completionTensorImageEquiv

completionTensorImageEquiv_tmul

(anonymous instance)

completionAdjoinImageEquiv

completionAdjoinImageEquiv_coe