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 #

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

Main results #

restrict_smul: restrict p E is compatible with gal_action p E.
gal_action_hom_injective: the action of gal p on the roots of p in E is faithful.
restrict_prod_inj: gal (p * q) embeds as a subgroup of gal p × gal q.

source

@[instance]

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

has_coe_to_fun p.gal

source

@[instance]

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

fintype p.gal

source

@[instance]

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

group p.gal

source

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)

source

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

σ = τ

source

@[instance]

def polynomial.gal.unique {F : Type u_1} [field F] (p : polynomial F) [h : fact (polynomial.splits (ring_hom.id F) p)] :

unique p.gal

Equations

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

source

def polynomial.gal.unique_gal_of_splits {F : Type u_1} [field F] (p : polynomial F) (h : polynomial.splits (ring_hom.id F) p) :

unique p.gal

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 := _}

source

@[instance]

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

unique 0.gal

Equations

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

source

@[instance]

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

unique 1.gal

Equations

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

source

@[instance]

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

source

@[instance]

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

source

@[instance]

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

source

@[instance]

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

source

@[instance]

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

source

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

source

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

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

source

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)

source

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

Equations

polynomial.gal.map_roots p E = λ (x : ↥(p.root_set p.splitting_field)), ⟨⇑(is_scalar_tower.to_alg_hom F p.splitting_field E) ↑x, _⟩

source

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)

source

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

source

@[instance]

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_scalar := {smul := λ (ϕ : p.gal) (x : ↥(p.root_set p.splitting_field)), ⟨⇑ϕ ↑x, _⟩}, one_smul := _, mul_smul := _}

source

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

mul_action p.gal ↥(p.root_set E)

Equations

polynomial.gal.gal_action p E = {to_has_scalar := {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 := _}

source

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

source

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)

gal_action as a permutation representation

Equations

polynomial.gal.gal_action_hom p E = {to_fun := λ (ϕ : p.gal), {to_fun := λ (x : ↥(p.root_set E)), ϕ • x, inv_fun := λ (x : ↥(p.root_set E)), ϕ⁻¹ • x, left_inv := _, right_inv := _}, map_one' := _, map_mul' := _}

source

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)

source

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

q.gal →* p.gal

The restriction homomorphism between Galois groups

Equations

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

source

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)

source

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

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

source

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

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

source

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

source

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

source

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

polynomial.gal.restrict_comp p q hq = polynomial.gal.restrict p (p.comp q).splitting_field

source

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)

source

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

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

source

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