Module

HenselianCompletionAutEquiv.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianCompletionAutEquiv

5 declarations indexed from sourceView source ↗

Module documentation

Automorphisms and Henselian completion

The correspondence of homomorphisms respects composition. Passing to units therefore gives a group isomorphism of automorphisms, whose action extends the original action on the finite separable extension.

Imports4

Nyll.ValuedFieldTheory.Valuation.Completion.DVFHomFunctor
Nyll.ValuedFieldTheory.Valuation.Completion.HenselianCompletionHomEquiv
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Group.Units.Equiv

Imported by1

Nyll.ValuedFieldTheory.Valuation.Completion.All

instance

(anonymous instance)

L30 ↗

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : HenselianDVF K) (target : DVF L)
  [base.toDVF.valuation.HasExtension target.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]

Lean source · statement

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

def

completionEndEquiv

L35 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionEndEquiv

Documentation

Completion identifies the endomorphism monoids of a finite separable extension of a Henselian DVF and its actual valuation completion.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : HenselianDVF K) (target : DVF L)
  [base.toDVF.valuation.HasExtension target.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  DVF.completionAlgebra base.toDVF target

Lean source · full declaration

def completionEndEquiv :
    (L →ₐ[K] L) ≃*
      @AlgHom base.valuation.Completion target.valuation.Completion
        target.valuation.Completion _ _ _
        (DVF.completionAlgebra base.toDVF target)
        (DVF.completionAlgebra base.toDVF target) where
  toEquiv := completionAlgHomEquiv base target target
  map_mul' f g :=
    DVF.extendCompletionAlgHom_comp base.toDVF target target target g f

theorem

completionEndEquiv_coe

L46 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionEndEquiv_coe

Documentation

The endomorphism correspondence extends the original map on field elements.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : HenselianDVF K) (target : DVF L)
  [base.toDVF.valuation.HasExtension target.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  DVF.completionAlgebra base.toDVF target

Lean source · statement

theorem completionEndEquiv_coe (f : L →ₐ[K] L) (x : L) :
    completionEndEquiv base target f (x : target.valuation.Completion) =
      (f x : target.valuation.Completion)

def

completionAutEquiv

L53 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionAutEquiv

Documentation

Completion identifies the automorphism groups by transporting units of the actual endomorphism monoids.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : HenselianDVF K) (target : DVF L)
  [base.toDVF.valuation.HasExtension target.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  DVF.completionAlgebra base.toDVF target

Lean source · statement

def completionAutEquiv :
    (L ≃ₐ[K] L) ≃*
      @AlgEquiv base.valuation.Completion target.valuation.Completion
        target.valuation.Completion _ _ _
        (DVF.completionAlgebra base.toDVF target)
        (DVF.completionAlgebra base.toDVF target)

theorem

completionAutEquiv_coe

L65 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.completionAutEquiv_coe

Documentation

The completed automorphism agrees with the original automorphism on the embedded finite extension.

Source context 4 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
  (base : HenselianDVF K) (target : DVF L)
  [base.toDVF.valuation.HasExtension target.valuation]
  [FiniteDimensional K L] [Algebra.IsSeparable K L]
local instance : Algebra base.valuation.Completion target.valuation.Completion :=
  DVF.completionAlgebra base.toDVF target

Lean source · statement

theorem completionAutEquiv_coe (e : L ≃ₐ[K] L) (x : L) :
    completionAutEquiv base target e (x : target.valuation.Completion) =
      (e x : target.valuation.Completion)

Module documentation

Automorphisms and Henselian completion

Declarations

(anonymous instance)

completionEndEquiv

completionEndEquiv_coe

completionAutEquiv

completionAutEquiv_coe