mathlibdocumentation

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.

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) :
def polynomial.gal {F : Type u_1} [field F] (p : polynomial F) :
Type u_1

The Galois group of a polynomial.

Equations
@[protected, instance]
noncomputable def polynomial.gal.has_coe_to_fun {F : Type u_1} [field F] (p : polynomial F) :
(λ (_x : p.gal),
Equations
@[ext]
theorem polynomial.gal.ext {F : Type u_1} [field F] (p : polynomial F) {σ τ : p.gal} (h : ∀ (x : p.splitting_field), x σ x = τ x) :
σ = τ
noncomputable def polynomial.gal.unique_gal_of_splits {F : Type u_1} [field F] (p : polynomial F) (h : 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 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_sub_C {F : Type u_1} [field F] (x : F) :
Equations
@[protected, instance]
noncomputable def polynomial.gal.unique_gal_X_pow {F : Type u_1} [field F] (n : ) :
Equations
@[protected, instance]
noncomputable def polynomial.gal.algebra {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [ E] [h : fact (polynomial.splits E) p)] :
Equations
@[protected, instance]
def polynomial.gal.is_scalar_tower {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [ E] [h : fact (polynomial.splits E) p)] :
noncomputable def polynomial.gal.restrict {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [ E] [fact (polynomial.splits 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] [ E] [fact (polynomial.splits E) p)] [ E] :
noncomputable def polynomial.gal.map_roots {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [ E] [fact (polynomial.splits 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] [ E] [h : fact (polynomial.splits E) p)] :
noncomputable def polynomial.gal.roots_equiv_roots {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [ E] [fact (polynomial.splits 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] [ E] [fact (polynomial.splits 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] [ E] [fact (polynomial.splits E) p)] (ϕ : E ≃ₐ[F] E) (x : (p.root_set E)) :
( ϕ x) = ϕ x

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] [ E] [fact (polynomial.splits 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] [ E] [fact (polynomial.splits E) p)] (ϕ : E ≃ₐ[F] E) (x : (p.root_set E)) :
( ( ϕ)) x) = ϕ x
theorem polynomial.gal.gal_action_hom_injective {F : Type u_1} [field F] (p : polynomial F) (E : Type u_2) [field E] [ E] [fact (polynomial.splits E) p)] :

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
• = dite (q = 0) (λ (hq : q = 0), 1) (λ (hq : ¬q = 0),
theorem polynomial.gal.restrict_dvd_surjective {F : Type u_1} [field F] {p q : polynomial F} (hpq : p q) (hq : q 0) :
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.restrict_prod_injective {F : Type u_1} [field F] (p q : polynomial F) :

polynomial.gal.restrict_prod is actually a subgroup embedding.

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₁ : p₁) (h₂ : p₂) :
polynomial.splits (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
theorem polynomial.gal.restrict_comp_surjective {F : Type u_1} [field F] (p q : polynomial F) (hq : q.nat_degree 0) :
theorem polynomial.gal.card_of_separable {F : Type u_1} [field F] {p : polynomial F} (hp : p.separable) :

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.

theorem polynomial.gal.gal_action_hom_bijective_of_prime_degree' {p : polynomial } (p_irr : irreducible p) (p_deg : nat.prime p.nat_degree) (p_roots1 : + 1 ) (p_roots2 : + 3) :

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