NYLL
Module

HenselianCompletionHomEquiv.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianCompletionHomEquiv
5 declarations indexed from sourceView source ↗

Module documentation

Correspondence of homomorphisms before and after completion

The actual extension map is bijective: the original field is embedded in its completion, and separable elements descend uniquely to a Henselian target. The inverse correspondence retains the original field embeddings.

Imports4
Imported by2

Declarations

instance

(anonymous instance)

L32 ↗
Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : HenselianDVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.toDVF.valuation.HasExtension targetL.valuation]
  [hM : base.toDVF.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra.IsAlgebraic K M]
Lean source · statement
instance : UniformContinuousConstSMul K (WithVal targetL.valuation)
instance

(anonymous instance)

L35 ↗
Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : HenselianDVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.toDVF.valuation.HasExtension targetL.valuation]
  [hM : base.toDVF.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra.IsAlgebraic K M]
local instance : UniformContinuousConstSMul K (WithVal targetL.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra targetL.valuation
Lean source · statement
instance : Algebra base.valuation.Completion targetL.valuation.Completion
theorem

extendCompletionAlgHom_bijective

L40 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.extendCompletionAlgHom_bijective
Documentation

Extending homomorphisms to the actual completions is bijective for a finite separable source and an algebraic target over a Henselian DVF.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : HenselianDVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.toDVF.valuation.HasExtension targetL.valuation]
  [hM : base.toDVF.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra.IsAlgebraic K M]
local instance : UniformContinuousConstSMul K (WithVal targetL.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra targetL.valuation
local instance : Algebra base.valuation.Completion targetL.valuation.Completion :=
  DVF.completionAlgebra base.toDVF targetL
Lean source · statement
theorem extendCompletionAlgHom_bijective :
    Function.Bijective (DVF.extendCompletionAlgHom base.toDVF targetL targetM)
def

completionAlgHomEquiv

L65 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.completionAlgHomEquiv
Documentation

The actual correspondence between original and completed homomorphisms.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : HenselianDVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.toDVF.valuation.HasExtension targetL.valuation]
  [hM : base.toDVF.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra.IsAlgebraic K M]
local instance : UniformContinuousConstSMul K (WithVal targetL.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra targetL.valuation
local instance : Algebra base.valuation.Completion targetL.valuation.Completion :=
  DVF.completionAlgebra base.toDVF targetL
Lean source · statement
def completionAlgHomEquiv :
    (L →ₐ[K] M) ≃
      @AlgHom base.valuation.Completion targetL.valuation.Completion
        targetM.valuation.Completion _ _ _
        (DVF.completionAlgebra base.toDVF targetL)
        (DVF.completionAlgebra base.toDVF targetM)
theorem

completionAlgHomEquiv_symm_coe

L75 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.completionAlgHomEquiv_symm_coe
Documentation

The inverse correspondence is the original homomorphism obtained by descent.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L M : Type*} [Field K] [Field L] [Field M]
  [Algebra K L] [Algebra K M]
  (base : HenselianDVF K) (targetL : DVF L) (targetM : DVF M)
  [hL : base.toDVF.valuation.HasExtension targetL.valuation]
  [hM : base.toDVF.valuation.HasExtension targetM.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra.IsAlgebraic K M]
local instance : UniformContinuousConstSMul K (WithVal targetL.valuation) :=
  WithVal.uniformContinuousConstSMul_algebra targetL.valuation
local instance : Algebra base.valuation.Completion targetL.valuation.Completion :=
  DVF.completionAlgebra base.toDVF targetL
Lean source · statement
theorem completionAlgHomEquiv_symm_coe
    (φ : @AlgHom base.valuation.Completion targetL.valuation.Completion
      targetM.valuation.Completion _ _ _
      (DVF.completionAlgebra base.toDVF targetL)
      (DVF.completionAlgebra base.toDVF targetM)) (x : L) :
    ((completionAlgHomEquiv base targetL targetM).symm φ x :
        targetM.valuation.Completion) = φ (x : targetL.valuation.Completion)

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