Open AccessRenamings and a Condition-free Formalization of Kronecker’s Construction
Author(s) -
Christoph Schwarzweller
Publication year - 2020
Publication title -
formalized mathematics
Language(s) - English
Resource type - Journals
eISSN - 1898-9934
pISSN - 1426-2630
DOI - 10.2478/forma-2020-0012
Subject(s) - disjoint sets , mathematics , kronecker delta , field (mathematics) , extension (predicate logic) , polynomial , field extension , discrete mathematics , degree (music) , combinatorics , algebraic extension , tutte polynomial , injective function , minimal polynomial (linear algebra) , algebra over a field , homogeneous polynomial , pure mathematics , matrix polynomial , computer science , graph , mathematical analysis , line graph , voltage graph , acoustics , ordinary differential equation , quantum mechanics , programming language , differential equation , differential algebraic equation , physics
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.