Module

DVFHomFunctor.lean

Nyll.ValuedFieldTheory.Valuation.Completion.DVFHomFunctor

3 declarations indexed from sourceView source ↗

Module documentation

Functoriality of homomorphisms on valuation completions

The extension formula on original field elements and extensionality over the base completion imply preservation of identities and composition.

Imports2

Imported by2

instance

(anonymous instance)

L30 ↗

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L M N : Type*} [Field K] [Field L] [Field M] [Field N]
  [Algebra K L] [Algebra K M] [Algebra K N]
  (base : DVF K) (targetL : DVF L) (targetM : DVF M) (targetN : DVF N)
  [hL : base.valuation.HasExtension targetL.valuation]
  [hM : base.valuation.HasExtension targetM.valuation]
  [hN : base.valuation.HasExtension targetN.valuation]
  [HenselianRing base.valuationSubring base.maximalIdeal]

Lean source · statement

instance : Algebra base.valuation.Completion targetL.valuation.Completion

theorem

extendCompletionAlgHom_id

L35 ↗

ValuationTheory.DiscreteValuationField.DVF.extendCompletionAlgHom_id

Documentation

Extending the identity on a finite separable extension gives the identity on its actual valuation completion.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L M N : Type*} [Field K] [Field L] [Field M] [Field N]
  [Algebra K L] [Algebra K M] [Algebra K N]
  (base : DVF K) (targetL : DVF L) (targetM : DVF M) (targetN : DVF N)
  [hL : base.valuation.HasExtension targetL.valuation]
  [hM : base.valuation.HasExtension targetM.valuation]
  [hN : base.valuation.HasExtension targetN.valuation]
  [HenselianRing base.valuationSubring base.maximalIdeal]
local instance : Algebra base.valuation.Completion targetL.valuation.Completion :=
  completionAlgebra base targetL

Lean source · statement

theorem extendCompletionAlgHom_id [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    extendCompletionAlgHom base targetL targetL (AlgHom.id K L) =
      AlgHom.id base.valuation.Completion targetL.valuation.Completion

theorem

extendCompletionAlgHom_comp

L44 ↗

ValuationTheory.DiscreteValuationField.DVF.extendCompletionAlgHom_comp

Documentation

Extending a composite is composition of the extended homomorphisms. Only the two source extensions must be finite and separable.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.DVF
variable {K L M N : Type*} [Field K] [Field L] [Field M] [Field N]
  [Algebra K L] [Algebra K M] [Algebra K N]
  (base : DVF K) (targetL : DVF L) (targetM : DVF M) (targetN : DVF N)
  [hL : base.valuation.HasExtension targetL.valuation]
  [hM : base.valuation.HasExtension targetM.valuation]
  [hN : base.valuation.HasExtension targetN.valuation]
  [HenselianRing base.valuationSubring base.maximalIdeal]
local instance : Algebra base.valuation.Completion targetL.valuation.Completion :=
  completionAlgebra base targetL

Lean source · statement

theorem extendCompletionAlgHom_comp
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [FiniteDimensional K M] [Algebra.IsSeparable K M]
    (f : L →ₐ[K] M) (g : M →ₐ[K] N) :
    extendCompletionAlgHom base targetL targetN (g.comp f) =
      (extendCompletionAlgHom base targetM targetN g).comp
        (extendCompletionAlgHom base targetL targetM f)

Module documentation

Functoriality of homomorphisms on valuation completions

Declarations

(anonymous instance)

extendCompletionAlgHom_id

extendCompletionAlgHom_comp