mathlib documentation

field_theory.polynomial_galois_group

Galois Groups of Polynomials #

In this file we introduce the Galois group of a polynomial, defined as the automorphism group of the splitting field.

Main definitions #

Main 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) :
σ = τ
@[instance]
def polynomial.gal.unique {F : Type u_1} [field F] (p : polynomial F) [h : fact (polynomial.splits (ring_hom.id F) p)] :
Equations

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

The restriction homomorphism

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 from roots p p.splitting_field to roots p E

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

gal_action as a permutation representation

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

The restriction homomorphism between Galois groups

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 embeds 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₂)
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

The restriction homomorphism from the Galois group of a homomorphism

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