<abstract xmlns="http://www.w3.org/1999/xhtml">
<bold>Summary</bold>. 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 <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] as the smallest field extension of <italic>F</italic>, in which <italic>p</italic> splits into linear factors. From this follows, that for a splitting field <italic>E</italic> of <italic>p</italic> we have <italic>E</italic> = <italic>F</italic> (<italic>A</italic>) where <italic>A</italic> is the set of <italic>p</italic>’s roots. Splitting fields are unique, however, only up to isomorphisms; to be more precise up to <italic>F</italic> -isomorphims i.e. isomorphisms <italic>i</italic> with <italic>i|F</italic> = Id<italic>F</italic>. We prove that two splitting fields of <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] are <italic>F</italic> -isomorphic using the well-known technique [4], [3] of extending isomorphisms from <italic>F</italic>1 → <italic>F</italic>2 to <italic>F</italic>1(<italic>a</italic>) → <italic>F</italic>2(<italic>b</italic>) for <italic>a</italic> and <italic>b</italic> being algebraic over <italic>F</italic>1 and <italic>F</italic>2, respectively.
</abstract>

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 = IdF. We prove that two splitting fields of p ∈ F [X] are F -isomorphic using the well-known technique [4], [3] of extending isomorphisms from F1 → F2 to F1(a) → F2(b) for a and b being algebraic over F1 and F2, respectively.

Splitting Fields

Formalized Mathematics

{"article-title":"Splitting Fields"}

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...

Splitting Fields

Article Category: Artikel

Online veröffentlicht: 30. Dez. 2021

Seitenbereich: 129 - 139

Akzeptiert: 30. Juni 2021

DOI: https://doi.org/10.2478/forma-2021-0013

Schlüsselwörter
field extensions, polynomials splitting fields

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Splitting Fields

Article Category: Artikel

Online veröffentlicht: 30. Dez. 2021

Seitenbereich: 129 - 139

Akzeptiert: 30. Juni 2021

DOI: https://doi.org/10.2478/forma-2021-0013

Schlüsselwörterfield extensions, polynomials splitting fields

© 2021 University of Białystok, published by Sciendo

CC-BY-SA License ver. 3.0 or later

Schlüsselwörter
field extensions, polynomials splitting fields