Splitting fields #
In this file we prove the existence and uniqueness of splitting fields.
Main definitions #
Polynomial.SplittingField f
: A fixed splitting field of the polynomialf
.
Main statements #
Polynomial.IsSplittingField.algEquiv
: Every splitting field of a polynomialf
is isomorphic toSplittingField f
and thus, being a splitting field is unique up to isomorphism.
Implementation details #
We construct a SplittingFieldAux
without worrying about whether the instances satisfy nice
definitional equalities. Then the actual SplittingField
is defined to be a quotient of a
MvPolynomial
ring by the kernel of the obvious map into SplittingFieldAux
. Because the
actual SplittingField
will be a quotient of a MvPolynomial
, it has nice instances on it.
Non-computably choose an irreducible factor from a polynomial.
Instances For
See note [fact non-instances].
Divide a polynomial f by X - C r
where r
is a root of f
in a bigger field extension.
Instances For
Auxiliary construction to a splitting field of a polynomial, which removes
n
(arbitrarily-chosen) factors.
It constructs the type, proves that is a field and algebra over the base field.
Uses recursion on the degree.
Instances For
Auxiliary construction to a splitting field of a polynomial, which removes
n
(arbitrarily-chosen) factors. It is the type constructed in SplittingFieldAuxAux
.
Instances For
A splitting field of a polynomial.
Instances For
The algebra equivalence with SplittingFieldAux
,
which we will use to construct the field structure.
Instances For
Embeds the splitting field into any other field that splits the polynomial.
Instances For
Any splitting field is isomorphic to SplittingFieldAux f
.