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 ofgal p
on the roots ofp
inE
.
Main results #
restrict_smul
:restrict p E
is compatible withgal_action p E
.gal_action_hom_injective
: the action ofgal p
on the roots ofp
inE
is faithful.restrict_prod_inj
:gal (p * q)
embeds as a subgroup ofgal p × gal q
.
@[instance]
@[instance]
@[instance]
The Galois group of a polynomial
Equations
- p.gal = (p.splitting_field ≃ₐ[F] p.splitting_field)
@[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
- polynomial.gal.unique p = {to_inhabited := {default := 1}, uniq := _}
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 := _}
@[instance]
Equations
- polynomial.gal.unique_gal_zero = polynomial.gal.unique_gal_of_splits 0 polynomial.gal.unique_gal_zero._proof_1
@[instance]
Equations
- polynomial.gal.unique_gal_one = polynomial.gal.unique_gal_of_splits 1 polynomial.gal.unique_gal_one._proof_1
@[instance]
Equations
@[instance]
Equations
- polynomial.gal.unique_gal_X = polynomial.gal.unique_gal_of_splits polynomial.X polynomial.gal.unique_gal_X._proof_1
@[instance]
@[instance]
def
polynomial.gal.unique_gal_X_pow
{F : Type u_1}
[field F]
(n : ℕ) :
unique (polynomial.X ^ n).gal
Equations
@[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)] :
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)] :
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)] :
↥(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, _⟩
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]
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 := _}
@[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 := _}
@[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)] :
p.gal →* equiv.perm ↥(p.root_set E)
gal_action
as a permutation representation
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)] :
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)
theorem
polynomial.gal.restrict_dvd_surjective
{F : Type u_1}
[field F]
{p q : polynomial F}
(hpq : p ∣ q)
(hq : q ≠ 0) :
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₂)
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
def
polynomial.gal.restrict_comp
{F : Type u_1}
[field F]
(p q : polynomial F)
(hq : q.nat_degree ≠ 0) :
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
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) :
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