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 = Gal(AlgebraicClosure K/K)

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

absoluteGaloisGroup is a topological space with the Krull topology.

Equations

• Field.instTopologicalSpaceAbsoluteGaloisGroup K = { IsOpen := Field.instTopologicalSpaceAbsoluteGaloisGroup._aux_1 K, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

instance Field.instIsTopologicalGroupAbsoluteGaloisGroup (K : Type u_1) [Field K] : IsTopologicalGroup (absoluteGaloisGroup K)

noncomputable def Field.absoluteGaloisGroup.mapOfAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra (AlgebraicClosure K) (AlgebraicClosure L)] [IsScalarTower K (AlgebraicClosure K) (AlgebraicClosure L)] : absoluteGaloisGroup L →ₜ* absoluteGaloisGroup K

A commuting square of two fields and their algebraic closures induces a continuous homomorphism of their absolute Galois groups.

Equations

• Field.absoluteGaloisGroup.mapOfAlgebra K L = { toMonoidHom := (AlgEquiv.restrictNormalHom (AlgebraicClosure K)).comp (AlgEquiv.restrictScalarsHom K), continuous_toFun := ⋯ }

@[simp]

theorem Field.absoluteGaloisGroup.mapOfAlgebra_toFun_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra (AlgebraicClosure K) (AlgebraicClosure L)] [IsScalarTower K (AlgebraicClosure K) (AlgebraicClosure L)] (x : absoluteGaloisGroup L) (a : AlgebraicClosure K) : ((mapOfAlgebra K L) x) a = ((↑((AlgEquiv.restrictScalarsHom K) x)).restrictNormal (AlgebraicClosure K)) a

@[simp]

theorem Field.absoluteGaloisGroup.mapOfAlgebra_toFun_symm_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Algebra (AlgebraicClosure K) (AlgebraicClosure L)] [IsScalarTower K (AlgebraicClosure K) (AlgebraicClosure L)] (x : absoluteGaloisGroup L) (b : AlgebraicClosure K) : (AlgEquiv.symm ((mapOfAlgebra K L) x)) b = Function.surjInv ⋯ b

noncomputable def Field.absoluteGaloisGroup.map {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) : absoluteGaloisGroup L →ₜ* absoluteGaloisGroup K

An embedding of fields induces a continuous homomorphism of absolute Galois groups. Note that this depends on an arbitrary choice of embedding of the algebraic closures.

Equations

• Field.absoluteGaloisGroup.map f = Field.absoluteGaloisGroup.mapOfAlgebra K L

@[simp]

theorem Field.absoluteGaloisGroup.map_toFun_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) (x : absoluteGaloisGroup L) (a : AlgebraicClosure K) : ((map f) x) a = ((↑((AlgEquiv.restrictScalarsHom K) x)).restrictNormal (AlgebraicClosure K)) a

@[simp]

theorem Field.absoluteGaloisGroup.map_toFun_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (f : K →+* L) (x : absoluteGaloisGroup L) (b : AlgebraicClosure K) : (AlgEquiv.symm ((map f) x)) b = Function.surjInv ⋯ b

The topological abelianization of the absolute Galois group

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

@[reducible, inline]

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)