mathlib3 documentation

field_theory.polynomial_galois_group

Galois Groups of Polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[protected, instance]
noncomputable def polynomial.gal.fintype {F : Type u_1} [field F] (p : polynomial F) :
@[protected, instance]
noncomputable def polynomial.gal.group {F : Type u_1} [field F] (p : polynomial F) :
@[protected, instance]
noncomputable def polynomial.gal.has_coe_to_fun {F : Type u_1} [field F] (p : polynomial F) :
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) :
σ = τ
noncomputable def polynomial.gal.unique_gal_of_splits {F : Type u_1} [field F] (p : polynomial F) (h : polynomial.splits (ring_hom.id F) p) :

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

Equations
@[protected, instance]
noncomputable def polynomial.gal.unique {F : Type u_1} [field F] (p : polynomial F) [h : fact (polynomial.splits (ring_hom.id F) p)] :
Equations
@[protected, instance]
noncomputable def polynomial.gal.unique_gal_zero {F : Type u_1} [field F] :
Equations
@[protected, instance]
noncomputable def polynomial.gal.unique_gal_one {F : Type u_1} [field F] :
Equations
@[protected, instance]
noncomputable def polynomial.gal.unique_gal_C {F : Type u_1} [field F] (x : F) :
Equations
@[protected, instance]
noncomputable def polynomial.gal.unique_gal_X {F : Type u_1} [field F] :
Equations
@[protected, instance]
noncomputable def polynomial.gal.unique_gal_X_pow {F : Type u_1} [field F] (n : ) :
Equations
@[protected, instance, irreducible]
noncomputable def polynomial.gal.algebra {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)] :
Equations
@[protected, instance]
noncomputable 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
noncomputable 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
noncomputable 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
@[protected, instance]
noncomputable def polynomial.gal.gal_action_aux {F : Type u_1} [field F] (p : polynomial F) :
Equations
@[protected, instance]
noncomputable 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.

noncomputable 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.

noncomputable 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_def {F : Type u_1} [field F] {p q : polynomial F} [decidable (q = 0)] (hpq : p q) :
polynomial.gal.restrict_dvd hpq = dite (q = 0) (λ (hq : q = 0), 1) (λ (hq : ¬q = 0), polynomial.gal.restrict p q.splitting_field)
noncomputable 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.

noncomputable 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.

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.