Renamings and a Condition-free Formalization of Kronecker’s Construction

In [7], [9], [10] we presented a formalization of Kronecker’s construction of a field extension E for a field F in which a given polynomial p ∈ F [X]\F has a root [5], [6], [3]. A drawback of our formalization was that it works only for polynomial-disjoint fields, that is for fields F with F ∩ F [X] = ∅. The main purpose of Kronecker’s construction is that by induction one gets a field extension of F in which p splits into linear factors. For our formalization this means that the constructed field extension E again has to be polynomial-disjoint.

In this article, by means of Mizar system [2], [1], we first analyze whether our formalization can be extended that way. Using the field of polynomials over F with degree smaller than the degree of p to construct the field extension E does not work: In this case E is polynomial-disjoint if and only if p is linear. Using F [X]/<p> one can show that for F = ℚ and F = ℤ_n the constructed field extension E is again polynomial-disjoint, so that in particular algebraic number fields can be handled.

For the general case we then introduce renamings of sets X as injective functions f with dom(f) = X and rng(f) ∩ (X ∪ Z) = ∅ for an arbitrary set Z. This, finally, allows to construct a field extension E of an arbitrary field F in which a given polynomial p ∈ F [X]\F splits into linear factors. Note, however, that to prove the existence of renamings we had to rely on the axiom of choice.