NYLL
Module

HenselianAbsoluteGalois.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianAbsoluteGalois
2 declarations indexed from sourceView source ↗

Module documentation

The absolute Galois group of a Henselian DVF and its completion

The tensor comparison gives the isomorphism on separable closures. The purely inseparable comparison with algebraic closures connects it to the actual Field.absoluteGaloisGroup, with its Krull topology, in every characteristic. The chosen separable-closure embedding records the choice.

Imports3
Imported by3

Declarations

def

completionAbsoluteGaloisEquiv

L29 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.completionAbsoluteGaloisEquiv
Documentation

Completion identifies the actual absolute Galois groups as topological groups. The only choice is an embedding of the two separable closures, which can always be supplied by IsSepClosed.lift.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K : Type*} [Field K] (base : HenselianDVF K)
Lean source · statement
def completionAbsoluteGaloisEquiv
    (i : SeparableClosure K →ₐ[K] SeparableClosure base.valuation.Completion) :
    Field.absoluteGaloisGroup K ≃ₜ* Field.absoluteGaloisGroup base.valuation.Completion
theorem

completionAbsoluteGaloisEquiv_apply

L50 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.completionAbsoluteGaloisEquiv_apply
Documentation

The completed absolute Galois action agrees through the chosen embedding with restriction of the original action to the separable closure.

Source context 3 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField.HenselianDVF
variable {K : Type*} [Field K] (base : HenselianDVF K)
Lean source · statement
theorem completionAbsoluteGaloisEquiv_apply
    (i : SeparableClosure K →ₐ[K] SeparableClosure base.valuation.Completion)
    (σ : Field.absoluteGaloisGroup K) (s : SeparableClosure K) :
    AlgEquiv.toAlgHom (base.completionAbsoluteGaloisEquiv i σ)
      (i s : AlgebraicClosure base.valuation.Completion) =
      (i (Completion.separableClosureAutEquiv K σ s) :
        AlgebraicClosure base.valuation.Completion)

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