Splitting fields #
This file introduces the notion of a splitting field of a polynomial and provides an embedding from
a splitting field to any field that splits the polynomial. A polynomial f : polynomial K
splits
over a field extension L
of K
if it is zero or all of its irreducible factors over L
have
degree 1
. A field extension of K
of a polynomial f : polynomial K
is called a splitting field
if it is the smallest field extension of K
such that f
splits.
Main definitions #
polynomial.splits i f
: A predicate on a field homomorphismi : K → L
and a polynomialf
saying thatf
is zero or all of its irreducible factors overL
have degree1
.polynomial.splitting_field f
: A fixed splitting field of the polynomialf
.polynomial.is_splitting_field
: A predicate on a field to be a splitting field of a polynomialf
.
Main statements #
polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C
: If a polynomial has as many roots as its degree, it can be written as the product of its leading coefficient with∏ (X - a)
wherea
ranges through its roots.lift_of_splits
: IfK
andL
are field extensions of a fieldF
and for some finite subsetS
ofK
, the minimal polynomial of everyx ∈ K
splits as a polynomial with coefficients inL
, thenalgebra.adjoin F S
embeds intoL
.polynomial.is_splitting_field.lift
: An embedding of a splitting field of the polynomialf
into another field such thatf
splits.polynomial.is_splitting_field.alg_equiv
: Every splitting field of a polynomialf
is isomorphic tosplitting_field f
and thus, being a splitting field is unique up to isomorphism.
A polynomial splits
iff it is zero or all of its irreducible factors have degree
1.
Equations
- polynomial.splits i f = (f = 0 ∨ ∀ {g : polynomial L}, irreducible g → g ∣ polynomial.map i f → g.degree = 1)
Pick a root of a polynomial that splits.
Equations
- polynomial.root_of_splits i hf hfd = classical.some _
A polynomial splits if and only if it has as many roots as its degree.
If P
is a monic polynomial that splits, then coeff P 0
equals the product of the roots.
If P
is a monic polynomial that splits, then P.next_coeff
equals the sum of the roots.
If p
is the minimal polynomial of a
over F
then F[a] ≃ₐ[F] F[x]/(p)
Equations
- alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly F x = (alg_equiv.of_bijective ((adjoin_root.lift_hom (minpoly F x) x _).cod_restrict (algebra.adjoin F {x}) _) _).symm
If a subalgebra
is finite_dimensional as a submodule then it is finite_dimensional
.
If K
and L
are field extensions of F
and we have s : finset K
such that
the minimal polynomial of each x ∈ s
splits in L
then algebra.adjoin F s
embeds in L
.
Non-computably choose an irreducible factor from a polynomial.
Equations
- f.factor = dite (∃ (g : polynomial K), irreducible g ∧ g ∣ f) (λ (H : ∃ (g : polynomial K), irreducible g ∧ g ∣ f), classical.some H) (λ (H : ¬∃ (g : polynomial K), irreducible g ∧ g ∣ f), polynomial.X)
Divide a polynomial f by X - C r where r is a root of f in a bigger field extension.
Equations
Auxiliary construction to a splitting field of a polynomial, which removes
n
(arbitrarily-chosen) factors.
Uses recursion on the degree. For better definitional behaviour, structures
including splitting_field_aux
(such as instances) should be defined using
this recursion in each field, rather than defining the whole tuple through
recursion.
Equations
- polynomial.splitting_field_aux n = n.rec_on (λ (K : Type u) (_x : field K) (_x : polynomial K), K) (λ (n : ℕ) (ih : Π {K : Type u} [_inst_4 : field K], polynomial K → Type u) (K : Type u) (_x : field K) (f : polynomial K), ih f.remove_factor)
Instances for polynomial.splitting_field_aux
- polynomial.splitting_field_aux.field
- polynomial.splitting_field_aux.inhabited
- polynomial.splitting_field_aux.algebra
- polynomial.splitting_field_aux.is_scalar_tower
- polynomial.splitting_field_aux.algebra'''
- polynomial.splitting_field_aux.algebra'
- polynomial.splitting_field_aux.algebra''
- polynomial.splitting_field_aux.scalar_tower'
- polynomial.splitting_field_aux.scalar_tower
Equations
- polynomial.splitting_field_aux.field n = n.rec_on (λ (K : Type u) (_x : field K) (_x_1 : polynomial K), _x) (λ (n : ℕ) (ih : Π {K : Type u} [_inst_4 : field K] {f : polynomial K}, field (polynomial.splitting_field_aux n f)) (K : Type u) (_x : field K) (f : polynomial K), ih)
Equations
Equations
- polynomial.splitting_field_aux.algebra n = n.rec_on (λ (R : Type u_1) (K : Type u) (_x : comm_semiring R) (_x_1 : field K) (_x : algebra R K) (_x_1 : polynomial K), _x) (λ (n : ℕ) (ih : Π (R : Type u_1) {K : Type u} [_inst_4 : comm_semiring R] [_inst_5 : field K] [_inst_6 : algebra R K] {f : polynomial K}, algebra R (polynomial.splitting_field_aux n f)) (R : Type u_1) (K : Type u) (_x : comm_semiring R) (_x_1 : field K) (_x_2 : algebra R K) (f : polynomial K), ih R)
A splitting field of a polynomial.
Equations
Instances for polynomial.splitting_field
- polynomial.splitting_field.field
- polynomial.splitting_field.inhabited
- polynomial.splitting_field.algebra'
- polynomial.splitting_field.algebra
- polynomial.is_splitting_field.splitting_field
- polynomial.is_splitting_field.polynomial.splitting_field.finite_dimensional
- polynomial.splitting_field.normal
- polynomial.gal.apply_mul_semiring_action
- polynomial.gal.algebra
- polynomial.gal.is_scalar_tower
Equations
This should be an instance globally, but it creates diamonds with the ℕ
, ℤ
, and ℚ
algebras
(via their smul
and to_fun
fields):
example :
(algebra_nat : algebra ℕ (splitting_field f)) = splitting_field.algebra' f :=
rfl -- fails
example :
(algebra_int _ : algebra ℤ (splitting_field f)) = splitting_field.algebra' f :=
rfl -- fails
example [char_zero K] [char_zero (splitting_field f)] :
(algebra_rat : algebra ℚ (splitting_field f)) = splitting_field.algebra' f :=
rfl -- fails
Until we resolve these diamonds, it's more convenient to only turn this instance on with
local attribute [instance]
in places where the benefit of having the instance outweighs the cost.
In the meantime, the splitting_field.algebra
instance below is immune to these particular diamonds
since K = ℕ
and K = ℤ
are not possible due to the field K
assumption. Diamonds in
algebra ℚ (splitting_field f)
instances are still possible via this instance unfortunately, but
these are less common as they require suitable char_zero
instances to be present.
Embeds the splitting field into any other field that splits the polynomial.
- splits : polynomial.splits (algebra_map K L) f
- adjoin_roots : algebra.adjoin K ↑((polynomial.map (algebra_map K L) f).roots.to_finset) = ⊤
Typeclass characterising splitting fields.
Splitting field of f
embeds into any field that splits f
.
Equations
- polynomial.is_splitting_field.lift L f hf = dite (f = 0) (λ (hf0 : f = 0), (algebra.of_id K F).comp (↑(algebra.bot_equiv K L).comp (_.mpr algebra.to_top))) (λ (hf0 : ¬f = 0), (_.mpr (classical.choice _)).comp algebra.to_top)
Any splitting field is isomorphic to splitting_field f
.