Module

SeparableGaloisClosureConjugation.lean

Nyll.GaloisCohomology.Kummer.Concrete.SeparableGaloisClosureConjugation

3 declarations indexed from sourceView source ↗

Module documentation

Absolute Galois abelianization using a separable closure

The comparison factors through the canonical separable closure and restriction from the algebraic closure. Independence of the chosen semilinear lift proves compatibility with the actual absolute action, including imperfect fields.

Imports9

Imported by2

def

separableAbsoluteGaloisClosureEquiv

L31 ↗

KummerTheory.separableAbsoluteGaloisClosureEquiv

Documentation

A separable closure gives the same topological absolute Galois group.

Source context 3 commands

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

namespace KummerTheory
open ProCGroups.Abelian
variable (K Ω : Type*) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosure K Ω]

Lean source · statement

def separableAbsoluteGaloisClosureEquiv :
    Gal(Ω/K) ≃ₜ* Gal(AlgebraicClosure K/K)

def

separableAbsoluteGaloisClosureAbelianizationEquiv

L37 ↗

KummerTheory.separableAbsoluteGaloisClosureAbelianizationEquiv

Documentation

The corresponding comparison on actual topological abelianizations.

Source context 3 commands

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

namespace KummerTheory
open ProCGroups.Abelian
variable (K Ω : Type*) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosure K Ω]

Lean source · statement

def separableAbsoluteGaloisClosureAbelianizationEquiv :
    _root_.TopologicalAbelianization Gal(Ω/K) ≃ₜ*
      _root_.TopologicalAbelianization Gal(AlgebraicClosure K/K)

theorem

separableAbsoluteGaloisClosureAbelianizationEquiv_conjugation

L43 ↗

KummerTheory.separableAbsoluteGaloisClosureAbelianizationEquiv_conjugation

Documentation

Comparison through a separable closure respects semilinear conjugation.

Source context 3 commands

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

namespace KummerTheory
open ProCGroups.Abelian
variable (K Ω : Type*) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosure K Ω]

Lean source · statement

theorem separableAbsoluteGaloisClosureAbelianizationEquiv_conjugation
    (τ : K ≃+* K) (a : Ω ≃+* Ω)
    (ha : ∀ k : K, a (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (x : _root_.TopologicalAbelianization Gal(Ω/K)) :
    separableAbsoluteGaloisClosureAbelianizationEquiv K Ω
        (TopologicalAbelianization.congr (semilinearGaloisConjugateContinuousEquiv τ a ha) x) =
      absoluteGaloisAbelianizationAction τ
        (separableAbsoluteGaloisClosureAbelianizationEquiv K Ω x)

Module documentation

Absolute Galois abelianization using a separable closure

Declarations

separableAbsoluteGaloisClosureEquiv

separableAbsoluteGaloisClosureAbelianizationEquiv

separableAbsoluteGaloisClosureAbelianizationEquiv_conjugation