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 #

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

@[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

p.gal = (p.splitting_field ≃ₐ[F] p.splitting_field)

Instances for polynomial.gal

@[protected, instance]

noncomputable def polynomial.gal.has_coe_to_fun {F : Type u_1} [field F] (p : polynomial F) :

has_coe_to_fun p.gal (λ (_x : p.gal), p.splitting_field → p.splitting_field)

Equations

polynomial.gal.has_coe_to_fun p = alg_equiv.has_coe_to_fun

@[protected, instance]

noncomputable def polynomial.gal.apply_mul_semiring_action {F : Type u_1} [field F] (p : polynomial F) :

mul_semiring_action p.gal p.splitting_field

Equations

polynomial.gal.apply_mul_semiring_action p = alg_equiv.apply_mul_semiring_action

@[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

polynomial.gal.unique_gal_of_splits p h = {to_inhabited := {default := 1}, uniq := _}

@[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

polynomial.gal.unique p = polynomial.gal.unique_gal_of_splits p _

@[protected, instance]

noncomputable def polynomial.gal.unique_gal_zero {F : Type u_1} [field F] :

Equations

polynomial.gal.unique_gal_zero = polynomial.gal.unique_gal_of_splits 0 polynomial.gal.unique_gal_zero._proof_1

@[protected, instance]

noncomputable def polynomial.gal.unique_gal_one {F : Type u_1} [field F] :

Equations

polynomial.gal.unique_gal_one = polynomial.gal.unique_gal_of_splits 1 polynomial.gal.unique_gal_one._proof_1

@[protected, instance]

noncomputable def polynomial.gal.unique_gal_C {F : Type u_1} [field F] (x : F) :

unique (⇑polynomial.C x).gal

Equations

polynomial.gal.unique_gal_C x = polynomial.gal.unique_gal_of_splits (⇑polynomial.C x) _

@[protected, instance]

noncomputable def polynomial.gal.unique_gal_X {F : Type u_1} [field F] :

unique polynomial.X.gal

Equations

polynomial.gal.unique_gal_X = polynomial.gal.unique_gal_of_splits polynomial.X polynomial.gal.unique_gal_X._proof_1

@[protected, instance]

noncomputable def polynomial.gal.unique_gal_X_sub_C {F : Type u_1} [field F] (x : F) :

unique (polynomial.X - ⇑polynomial.C x).gal

Equations

polynomial.gal.unique_gal_X_sub_C x = polynomial.gal.unique_gal_of_splits (polynomial.X - ⇑polynomial.C x) _

@[protected, instance]

noncomputable def polynomial.gal.unique_gal_X_pow {F : Type u_1} [field F] (n : ℕ) :

unique (polynomial.X ^ n).gal

Equations

polynomial.gal.unique_gal_X_pow n = polynomial.gal.unique_gal_of_splits (polynomial.X ^ n) _

@[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)] :

algebra p.splitting_field E

Equations

polynomial.gal.algebra p E = (polynomial.is_splitting_field.lift p.splitting_field p _).to_ring_hom.to_algebra

@[protected, 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)] :

is_scalar_tower F p.splitting_field E

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

polynomial.gal.restrict p E = alg_equiv.restrict_normal_hom p.splitting_field

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] :

function.surjective ⇑(polynomial.gal.restrict p E)

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

↥(p.root_set p.splitting_field) → ↥(p.root_set E)

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

Equations

polynomial.gal.map_roots p E = set.maps_to.restrict ⇑(is_scalar_tower.to_alg_hom F p.splitting_field E) (p.root_set p.splitting_field) (p.root_set E) _

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

function.bijective (polynomial.gal.map_roots p E)

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

↥(p.root_set p.splitting_field) ≃ ↥(p.root_set E)

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

Equations

polynomial.gal.roots_equiv_roots p E = equiv.of_bijective (polynomial.gal.map_roots p E) _

@[protected, instance]

noncomputable def polynomial.gal.gal_action_aux {F : Type u_1} [field F] (p : polynomial F) :

mul_action p.gal ↥(p.root_set p.splitting_field)

Equations

polynomial.gal.gal_action_aux p = {to_has_smul := {smul := λ (ϕ : p.gal), set.maps_to.restrict ⇑ϕ (p.root_set p.splitting_field) (p.root_set p.splitting_field) _}, one_smul := _, mul_smul := _}

@[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)] :

mul_action p.gal ↥(p.root_set E)

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

Equations

polynomial.gal.gal_action p E = {to_has_smul := {smul := λ (ϕ : p.gal) (x : ↥(p.root_set E)), ⇑(polynomial.gal.roots_equiv_roots p E) (ϕ • ⇑((polynomial.gal.roots_equiv_roots p E).symm) x)}, one_smul := _, mul_smul := _}

@[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) ϕ • 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] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] :

p.gal →* equiv.perm ↥(p.root_set E)

polynomial.gal.gal_action as a permutation representation

Equations

polynomial.gal.gal_action_hom p E = mul_action.to_perm_hom p.gal ↥(p.root_set E)

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

↑(⇑(⇑(polynomial.gal.gal_action_hom p E) (⇑(polynomial.gal.restrict p 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] [algebra F E] [fact (polynomial.splits (algebra_map F E) p)] :

function.injective ⇑(polynomial.gal.gal_action_hom p 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) :

q.gal →* p.gal

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

Equations

polynomial.gal.restrict_dvd hpq = dite (q = 0) (λ (hq : q = 0), 1) (λ (hq : ¬q = 0), polynomial.gal.restrict p q.splitting_field)

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)

theorem polynomial.gal.restrict_dvd_surjective {F : Type u_1} [field F] {p q : polynomial F} (hpq : p ∣ q) (hq : q ≠ 0) :

function.surjective ⇑(polynomial.gal.restrict_dvd hpq)

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

polynomial.gal.restrict_prod p q = (polynomial.gal.restrict_dvd _).prod (polynomial.gal.restrict_dvd _)

theorem polynomial.gal.restrict_prod_injective {F : Type u_1} [field F] (p q : polynomial F) :

function.injective ⇑(polynomial.gal.restrict_prod p q)

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₁ : 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₂)

theorem polynomial.gal.splits_in_splitting_field_of_comp {F : Type u_1} [field F] (p q : polynomial F) (hq : q.nat_degree ≠ 0) :

polynomial.splits (algebra_map F (p.comp q).splitting_field) 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

polynomial.gal.restrict_comp p q hq = let h : fact (polynomial.splits (algebra_map F (p.comp q).splitting_field) p) := _ in polynomial.gal.restrict p (p.comp q).splitting_field

theorem polynomial.gal.restrict_comp_surjective {F : Type u_1} [field F] (p q : polynomial F) (hq : q.nat_degree ≠ 0) :

function.surjective ⇑(polynomial.gal.restrict_comp p q hq)

theorem polynomial.gal.card_of_separable {F : Type u_1} [field F] {p : polynomial F} (hp : p.separable) :

fintype.card p.gal = finite_dimensional.finrank F p.splitting_field

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

p.nat_degree ∣ fintype.card p.gal

theorem polynomial.gal.splits_ℚ_ℂ {p : polynomial ℚ} :

fact (polynomial.splits (algebra_map ℚ ℂ) p)

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

theorem polynomial.gal.gal_action_hom_bijective_of_prime_degree {p : polynomial ℚ} (p_irr : irreducible p) (p_deg : nat.prime p.nat_degree) (p_roots : fintype.card ↥(p.root_set ℂ) = fintype.card ↥(p.root_set ℝ) + 2) :

function.bijective ⇑(polynomial.gal.gal_action_hom p ℂ)

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 : fintype.card ↥(p.root_set ℝ) + 1 ≤ fintype.card ↥(p.root_set ℂ)) (p_roots2 : fintype.card ↥(p.root_set ℂ) ≤ fintype.card ↥(p.root_set ℝ) + 3) :

function.bijective ⇑(polynomial.gal.gal_action_hom p ℂ)

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