# Volume 27 (2019): Issue 3 (October 2019)

Journal Details
Format
Journal
eISSN
1898-9934
ISSN
1426-2630
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

0 Articles
Open Access

#### On the Intersection of Fields F with F [X]

Published Online: 17 Feb 2020
Page range: 223 - 228

#### Abstract

This is the third part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial pF [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [6], [4], [5].

In the first part we show that an irreducible polynomial pF [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have FF [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ: F → F [X]/<p> and show that the translated polynomial ϕ (p) has a root over F [X]/<p>.

Because F is not a subfield of F [X]/<p> we construct in the second part the field (E \ ϕF)∪F for a given monomorphism ϕ: F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that FE = ∅, in particular Kronecker’s construction can be formalized for fields F with FF [X] = ∅.

Surprisingly, as we show in this third part, this condition is not automatically true for arbitrary fields F : With the exception of ℤ2 we construct for every field F an isomorphic copy F′ of F with F′F′ [X] ≠ ∅. We also prove that for Mizar’s representations of ℤn, ℚ and ℝ we have ℤn ∩ ℤn[X] = ∅, ℚ ∩ ℚ[X] = ∅ and ℝ ∩ ℝ[X] = ∅, respectively.

In the fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have FE as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ: F → F [X]/<p>. Together with the first part this gives – for fields F with FF [X] = ∅ – a field extension E of F in which pF [X]\F has a root.

#### Keywords

• roots of polynomials
• field extensions
• Kronecker’s construction

• 12E05
• 12F05
• 68T99
• 03B35
Open Access

#### Field Extensions and Kronecker’s Construction

Published Online: 17 Feb 2020
Page range: 229 - 235

#### Abstract

This is the fourth part of a four-article series containing a Mizar [3], [2], [1] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial pF [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [6], [4], [5].

In the first part we show that an irreducible polynomial pF [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have FF [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ: F → F [X]/<p> and show that the translated polynomial ϕ (p) has a root over F [X]/<p>.

Because F is not a subfield of F [X]/<p> we construct in the second part the field (E \ ϕF)∪F for a given monomorphism ϕ: F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that FE = ∅, in particular Kronecker’s construction can be formalized for fields F with F ∩ F [X] = ∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitrary fields F : With the exception of ℤ2 we construct for every field F an isomorphic copy F′ of F with F′ ∩ F′ [X] ≠ ∅. We also prove that for Mizar’s representations of ℤn, ℚ and ℝ we have ℤnn[X] = ∅, ℚ ℚ[X] = ∅ and ℝ ℝ[X] = ∅, respectively.

In this fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have FE as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ: F → F [X]/<p>. Together with the first part this gives – for fields F with F ∩ F [X] = ∅ – a field extension E of F in which pF [X]\F has a root.

#### Keywords

• roots of polynomials
• field extensions
• Kronecker’s construction

• 12E05
• 12F05
• 68T99
• 03B35
Open Access

#### Underlying Simple Graphs

Published Online: 17 Feb 2020
Page range: 237 - 259

#### Abstract

In this article the notion of the underlying simple graph of a graph (as defined in [8]) is formalized in the Mizar system [5], along with some convenient variants. The property of a graph to be without decorators (as introduced in [7]) is formalized as well to serve as the base of graph enumerations in the future.

#### Keywords

• graph operations
• underlying simple graph

#### MSC 2010

• 68T99
• 03B35
• 05C76
Open Access

Published Online: 17 Feb 2020
Page range: 261 - 301

#### Abstract

In this articles adjacency-preserving mappings from a graph to another are formalized in the Mizar system [7], [2]. The generality of the approach seems to be largely unpreceeded in the literature to the best of the author’s knowledge. However, the most important property defined in the article is that of two graphs being isomorphic, which has been extensively studied. Another graph decorator is introduced as well.

#### Keywords

• graph homomorphism
• graph isomorphism

#### MSC 2010

• 05C60
• 68T99
• 03B35
Open Access

Published Online: 17 Feb 2020
Page range: 303 - 313

#### Abstract

In [6] partial graph mappings were formalized in the Mizar system [3]. Such mappings map some vertices and edges of a graph to another while preserving adjacency. While this general approach is appropriate for the general form of (multidi)graphs as introduced in [7], a more specialized version for graphs without parallel edges seems convenient. As such, partial vertex mappings preserving adjacency between the mapped verticed are formalized here.

#### Keywords

• graph homomorphism
• graph isomorphism

• 05C60
• 68T99
• 03B35
Open Access

#### Operations of Points on Elliptic Curve in Affine Coordinates

Published Online: 17 Feb 2020
Page range: 315 - 320

#### Abstract

In this article, we formalize in Mizar [1], [2] a binary operation of points on an elliptic curve over GF(p) in affine coordinates. We show that the operation is unital, complementable and commutative. Elliptic curve cryptography [3], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security.

#### Keywords

• elliptic curve
• commutative operation

• 14H52
• 14K05
• 68T99
• 03B35