The topological abelianization of the absolute Galois group.

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

Main definitions

• Field.absoluteGaloisGroup : The Galois group of the field extension K^al/K, where K^al is an algebraic closure of K.
• Field.absoluteGaloisGroupAbelianization : The topological abelianization of Field.absoluteGaloisGroup K, that is, the quotient of Field.absoluteGaloisGroup K by the topological closure of its commutator subgroup.

Main results

• Field.absoluteGaloisGroup.commutator_closure_isNormal : the topological closure of the commutator of absoluteGaloisGroup is a normal subgroup.

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

• Field.absoluteGaloisGroup K = (AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K)

noncomputable instance Field.instGroupAbsoluteGaloisGroup (K : Type u_1) [Field K] : Group (Field.absoluteGaloisGroup K)

Equations

• Field.instGroupAbsoluteGaloisGroup K = AlgEquiv.aut

noncomputable instance Field.instTopologicalSpaceAbsoluteGaloisGroup (K : Type u_1) [Field K] : TopologicalSpace (Field.absoluteGaloisGroup K)

absoluteGaloisGroup is a topological space with the Krull topology.

Equations

• Field.instTopologicalSpaceAbsoluteGaloisGroup K = krullTopology K (AlgebraicClosure K)

The topological abelianization of the absolute Galois group

instance Field.absoluteGaloisGroup.commutator_closure_isNormal (K : Type u_1) [Field K] : Subgroup.Normal (Subgroup.topologicalClosure (commutator (Field.absoluteGaloisGroup K)))

Equations

• (_ : Subgroup.Normal (Subgroup.topologicalClosure (commutator (Field.absoluteGaloisGroup K)))) = (_ : Subgroup.Normal (Subgroup.topologicalClosure (commutator (Field.absoluteGaloisGroup K))))

@[inline, reducible]

abbrev Field.absoluteGaloisGroupAbelianization (K : Type u_1) [Field K] : Type u_1

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

Equations

• Field.absoluteGaloisGroupAbelianization K = TopologicalAbelianization (Field.absoluteGaloisGroup K)