mathlib documentation

field_theory.polynomial_galois_group

Galois Groups of Polynomials #

In this file, we introduce the Galois group of a polynomial p over a field F, defined as the automorphism group of its splitting field. We also provide some results about some extension E above p.splitting_field, and some specific results about the Galois groups of ℚ-polynomials with specific numbers of non-real roots.

Main definitions #

Main results #

Other results #

@[instance]
def polynomial.gal.has_coe_to_fun {F : Type u_1} [field F] (p : polynomial F) :
@[instance]
def polynomial.gal.fintype {F : Type u_1} [field F] (p : polynomial F) :
@[instance]
def polynomial.gal.group {F : Type u_1} [field F] (p : polynomial F) :
def polynomial.gal {F : Type u_1} [field F] (p : polynomial F) :
Type u_1

The Galois group of a polynomial.

Equations
@[ext]
theorem polynomial.gal.ext {F : Type u_1} [field F] (p : polynomial F) {σ τ : p.gal} (h : ∀ (x : p.splitting_field), x p.root_set p.splitting_fieldσ x = τ x) :
σ = τ

If p splits in F then the p.gal is trivial.

Equations
@[instance]
def polynomial.gal.unique_gal_zero {F : Type u_1} [field F] :
Equations
@[instance]
def polynomial.gal.unique_gal_one {F : Type u_1} [field F] :
Equations
@[instance]
Equations
@[instance]
def polynomial.gal.is_scalar_tower {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [h : fact (polynomial.splits (algebra_map F E) p)] :
def polynomial.gal.restrict {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] :
(E ≃ₐ[F] E) →* p.gal

Restrict from a superfield automorphism into a member of gal p.

Equations
theorem polynomial.gal.restrict_surjective {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] [normal F E] :
def polynomial.gal.map_roots {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] :

The function taking roots p p.splitting_field to roots p E. This is actually a bijection, see polynomial.gal.map_roots_bijective.

Equations
theorem polynomial.gal.map_roots_bijective {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [h : fact (polynomial.splits (algebra_map F E) p)] :
def polynomial.gal.roots_equiv_roots {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] :

The bijection between root_set p p.splitting_field and root_set p E.

Equations
@[instance]
Equations
@[instance]
def polynomial.gal.gal_action {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] :

The action of gal p on the roots of p in E.

Equations
@[simp]
theorem polynomial.gal.restrict_smul {F : Type u_1} [field F] {p : polynomial F} {E : Type u_2} [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] (ϕ : E ≃ₐ[F] E) (x : (p.root_set E)) :

polynomial.gal.restrict p E is compatible with polynomial.gal.gal_action p E.

def polynomial.gal.gal_action_hom {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] :

polynomial.gal.gal_action as a permutation representation

Equations
theorem polynomial.gal.gal_action_hom_restrict {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] (ϕ : E ≃ₐ[F] E) (x : (p.root_set E)) :

gal p embeds as a subgroup of permutations of the roots of p in E.

def polynomial.gal.restrict_dvd {F : Type u_1} [field F] {p q : polynomial F} (hpq : p q) :

polynomial.gal.restrict, when both fields are splitting fields of polynomials.

Equations
theorem polynomial.gal.restrict_dvd_surjective {F : Type u_1} [field F] {p q : polynomial F} (hpq : p q) (hq : q 0) :
def polynomial.gal.restrict_prod {F : Type u_1} [field F] (p q : polynomial F) :
(p * q).gal →* p.gal × q.gal

The Galois group of a product maps into the product of the Galois groups.

Equations
theorem polynomial.gal.mul_splits_in_splitting_field_of_mul {F : Type u_1} [field F] {p₁ q₁ p₂ q₂ : polynomial F} (hq₁ : q₁ 0) (hq₂ : q₂ 0) (h₁ : polynomial.splits (algebra_map F q₁.splitting_field) p₁) (h₂ : polynomial.splits (algebra_map F q₂.splitting_field) p₂) :
polynomial.splits (algebra_map F (q₁ * q₂).splitting_field) (p₁ * p₂)

p splits in the splitting field of p ∘ q, for q non-constant.

def polynomial.gal.restrict_comp {F : Type u_1} [field F] (p q : polynomial F) (hq : q.nat_degree 0) :
(p.comp q).gal →* p.gal

polynomial.gal.restrict for the composition of polynomials.

Equations

For a separable polynomial, its Galois group has cardinality equal to the dimension of its splitting field over F.

theorem polynomial.gal.prime_degree_dvd_card {F : Type u_1} [field F] {p : polynomial F} [char_zero F] (p_irr : irreducible p) (p_deg : nat.prime p.nat_degree) :

The number of complex roots equals the number of real roots plus the number of roots not fixed by complex conjugation (i.e. with some imaginary component).

An irreducible polynomial of prime degree with two non-real roots has full Galois group.

An irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group.