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 polynomial
Main statements #
Polynomial.IsSplittingField.algEquiv: Every splitting field of a polynomial
fis isomorphic to
SplittingField fand 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
SplittingField will be a quotient of a
MvPolynomial, it has nice instances on it.
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.
The algebra equivalence with
which we will use to construct the field structure.