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

## Main definitions #

• polynomial.gal p: the Galois group of a polynomial p.
• polynomial.gal.restrict p E: the restriction homomorphism (E ≃ₐ[F] E) → gal p.
• polynomial.gal.gal_action p E: the action of gal p on the roots of p in E.

## Main results #

• polynomial.gal.restrict_smul: restrict p E is compatible with gal_action p E.
• polynomial.gal.gal_action_hom_injective: gal p acting on the roots of p in E is faithful.
• polynomial.gal.restrict_prod_injective: gal (p * q) embeds as a subgroup of gal p × gal q.
• polynomial.gal.card_of_separable: For a separable polynomial, its Galois group has cardinality equal to the dimension of its splitting field over F.
• polynomial.gal.gal_action_hom_bijective_of_prime_degree: An irreducible polynomial of prime degree with two non-real roots has full Galois group.

## Other results #

• polynomial.gal.card_complex_roots_eq_card_real_add_card_not_gal_inv: 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).
@[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 σ x = τ x) :
σ = τ
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
@[instance]
def polynomial.gal.unique {F : Type u_1} [field F] (p : polynomial F) [h : fact p)] :
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]
def polynomial.gal.unique_gal_C {F : Type u_1} [field F] (x : F) :
Equations
@[instance]
def polynomial.gal.unique_gal_X {F : Type u_1} [field F] :
Equations
@[instance]
def polynomial.gal.unique_gal_X_sub_C {F : Type u_1} [field F] (x : F) :
Equations
@[instance]
def polynomial.gal.unique_gal_X_pow {F : Type u_1} [field F] (n : ) :
Equations
@[instance]
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
@[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)] :
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] :
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)] :
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
@[instance]
Equations
@[instance]
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.

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.

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) :
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.

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.