mathlib documentation

ideles / galois

The topological abelianization of the absolute Galois group. #

We define the topological abelianization of the absolute Galois group of a field K. In order to fo this, we needed to formalize the definition subgroup.connected_component_of_one and the lemmas topological_group.continuous_conj and subgroup.is_normal_topological_closure, which have already been integrated into mathlib.

Main definitions #

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

Tags #

number field, galois group, abelianization

def G_K (K : Type u_1) [field K] :

Type u_1

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

Equations

G_K K = (algebraic_closure K ≃ₐ[K] algebraic_closure K)

@[protected, instance]

noncomputable def G_K.group (K : Type u_1) [field K] :

Equations

G_K.group K = alg_equiv.aut

@[protected, instance]

noncomputable def G_K.inhabited (K : Type u_1) [field K] :

inhabited (G_K K)

Equations

G_K.inhabited K = {default := 1}

@[protected, instance]

noncomputable def G_K.topological_space (K : Type u_1) [field K] :

topological_space (G_K K)

G_K is a topological space with the Krull topology.

Equations

G_K.topological_space K = krull_topology K (algebraic_closure K)

@[protected, instance]

def G_K.topological_group (K : Type u_1) [field K] :

topological_group (G_K K)

G_K is a topological group with the Krull topology.

Topological abelianization

@[protected, instance]

def G_K.is_normal_commutator_closure (K : Type u_1) [field K] :

(commutator (G_K K)).topological_closure.normal

def G_K_ab (K : Type u_1) [field K] :

Type u_1

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

Equations

G_K_ab K = (G_K K ⧸ (commutator (G_K K)).topological_closure)

@[protected, instance]

noncomputable def G_K_ab.group (K : Type u_1) [field K] :

group (G_K_ab K)

Equations

G_K_ab.group K = quotient_group.quotient.group (commutator (G_K K)).topological_closure

@[protected, instance]

noncomputable def G_K_ab.inhabited (K : Type u_1) [field K] :

inhabited (G_K_ab K)

Equations

G_K_ab.inhabited K = {default := 1}

@[protected, instance]

noncomputable def G_K_ab.topological_space (K : Type u_1) [field K] :

topological_space (G_K_ab K)

G_K_ab is a topological space with the quotient topology.

Equations

G_K_ab.topological_space K = quotient_group.quotient.topological_space (commutator (G_K K)).topological_closure

@[protected, instance]

def G_K_ab.topological_group (K : Type u_1) [field K] :

topological_group (G_K_ab K)

G_K_ab is a topological group with the quotient topology.