NYLL
Module

MathlibAbsoluteAbelianization.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.MathlibAbsoluteAbelianization
2 declarations indexed from sourceView source ↗

Module documentation

Comparison with Mathlib's absolute Galois abelianization

Restriction from the algebraic closure to the separable closure identifies Mathlib's absolute Galois group with the separable-closure model. The induced map on topological abelianizations is a homeomorphism of groups, not merely an abstract group isomorphism.

Imports3
Imported by2

Declarations

def

absoluteGaloisGroupAbelianizationEquivSeparable

L26 ↗
Documentation

Mathlib's absolute Galois abelianization and the separable-closure topological abelianization are canonically isomorphic as topological groups.

Source context 2 commands

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

noncomputable section
universe u
Lean source · statement
def absoluteGaloisGroupAbelianizationEquivSeparable
    (K : Type u) [Field K] :
    Field.absoluteGaloisGroupAbelianization K ≃ₜ*
      TopologicalAbelianization Gal(SeparableClosure K / K)
theorem

absoluteGaloisGroupAbelianizationEquivSeparable_mk

L36 ↗
Documentation

The comparison sends an absolute Galois automorphism to its restriction to the separable closure, also after passing to the abelianization.

Source context 2 commands

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

noncomputable section
universe u
Lean source · statement
theorem absoluteGaloisGroupAbelianizationEquivSeparable_mk
    (K : Type u) [Field K] (σ : Field.absoluteGaloisGroup K) :
    absoluteGaloisGroupAbelianizationEquivSeparable K
        (QuotientGroup.mk σ) =
      QuotientGroup.mk (AlgEquiv.separableClosure σ)

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