Splitting Fields
Christoph Schwarzweller · Formalized Mathematics · 2021
Summary . In this article we further develop field theory in Mizar [1], [2]: we prove existence and uniqueness of splitting fields. We define the splitting field of a polynomial p ∈ F [ X ] as the smallest field extension of F , in which p splits into linear factors. From this follows, that for a splitting field E of p we have E = F ( A ) where A is the set of p ’s roots. Splitting fields are unique, however, only up to isomorphisms; to be more precise up to F -isomorphims i.e. isomorphisms i with i| F = Id F . We prove that two splitting fields of p ∈ F [ X ] are F -isomorphic using the well-known technique [4], [3] of extending isomorphisms from F 1 → F 2 to F 1 ( a ) → F 2 ( b ) for a and b being algebraic over F 1 and F 2 , respectively.