Renamings and a Condition-free Formalization of Kronecker’s Construction
Christoph Schwarzweller · Formalized Mathematics · 2020
Summary 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 ] / 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.