Module

SeparableGaloisMap.lean

Nyll.GaloisCohomology.Topology.SeparableGaloisMap

4 declarations indexed from sourceView source ↗

Module documentation

Restriction maps on the separable parts of algebraic closures

The algebraic-closure embedding used for absolute Galois restriction preserves the separable closure. Its restriction intertwines the actual Galois maps.

Imports2

Imported by3

def

separableClosureLift

L22 ↗

Field.absoluteGaloisGroup.separableClosureLift

Documentation

The chosen algebraic-closure embedding restricts to the separable closures.

Source context 2 commands

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

namespace Field.absoluteGaloisGroup
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

def separableClosureLift (f : K →+* L) :
    SeparableClosure K →+* SeparableClosure L

theorem

separableClosureLift_coe

L34 ↗

Field.absoluteGaloisGroup.separableClosureLift_coe

Documentation

Inclusion into the algebraic closure recovers the chosen closure embedding.

Source context 2 commands

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

namespace Field.absoluteGaloisGroup
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

theorem separableClosureLift_coe (f : K →+* L) (s : SeparableClosure K) :
    (separableClosureLift f s : AlgebraicClosure L) = closureLift f (s : AlgebraicClosure K)

theorem

separableClosureLift_algebraMap

L38 ↗

Field.absoluteGaloisGroup.separableClosureLift_algebraMap

Documentation

The separable-closure embedding extends the original field embedding.

Source context 2 commands

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

namespace Field.absoluteGaloisGroup
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

theorem separableClosureLift_algebraMap (f : K →+* L) (x : K) :
    separableClosureLift f (algebraMap K (SeparableClosure K) x) =
      algebraMap L (SeparableClosure L) (f x)

theorem

map_separableClosureLift

L45 ↗

Field.absoluteGaloisGroup.map_separableClosureLift

Documentation

Galois restriction intertwines the induced embedding of separable closures.

Source context 2 commands

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

namespace Field.absoluteGaloisGroup
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

theorem map_separableClosureLift (f : K →+* L)
    (σ : Gal(AlgebraicClosure L/L)) (s : SeparableClosure K) :
    separableClosureLift f
        (ValuationTheory.Completion.separableClosureAutEquiv K (map f σ) s) =
      ValuationTheory.Completion.separableClosureAutEquiv L σ (separableClosureLift f s)

Module documentation

Restriction maps on the separable parts of algebraic closures

Declarations

separableClosureLift

separableClosureLift_coe

separableClosureLift_algebraMap

map_separableClosureLift