Galois Groups of Polynomials #
In this file, we introduce the Galois group of a polynomial
p over a field
defined as the automorphism group of its splitting field. We also provide
some results about some extension
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 pon the roots of
Main results #
restrict p Eis compatible with
gal_action p E.
gal pacting on the roots of
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
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).
Restrict from a superfield automorphism into a member of
The function taking
roots p p.splitting_field to
roots p E. This is actually a bijection,
The bijection between
root_set p p.splitting_field and
root_set p E.
The action of
gal p on the roots of
polynomial.gal.gal_action as a permutation representation
gal p embeds as a subgroup of permutations of the roots of
polynomial.gal.restrict, when both fields are splitting fields of polynomials.
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.
An irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group.