Documentation

Mathlib.FieldTheory.AbsoluteGaloisGroup

The topological abelianization of the absolute Galois group. #

We define the absolute Galois group of a field K and its topological abelianization.

Main definitions #

Main results #

Tags #

field, algebraic closure, galois group, abelianization

The absolute Galois group #

def Field.absoluteGaloisGroup (K : Type u_1) [Field K] :
Type u_1

The absolute Galois group of K, defined as the Galois group of the field extension K^al/K, where K^al is an algebraic closure of K.

Equations
Instances For

    The topological abelianization of the absolute Galois group #

    Equations
    • =
    @[reducible, inline]

    The topological abelianization of absoluteGaloisGroup, that is, the quotient of absoluteGaloisGroup by the topological closure of its commutator subgroup.

    Equations
    Instances For