<abstract xmlns="http://www.w3.org/1999/xhtml">
A classical algebraic geometry is study of zero points of system of multivariate polynomials [3], [7] and those zero points would be corresponding to points, lines, curves, surfaces in an affine space. In this article we give some basic definition of the area of affine algebraic geometry such as algebraic set, ideal of set of points, and those properties according to [4] in the Mizar system[5], [2].
We treat an affine space as the <italic>n</italic>-fold Cartesian product <italic>k</italic><italic>n </italic>as the same manner appeared in [4]. Points in this space are identified as <italic>n</italic>-tuples of elements from the set <italic>k</italic>. The formalization of points, which are <italic>n</italic>-tuples of numbers, is described in terms of a mapping from <italic>n </italic>to <italic>k</italic>, where the domain <italic>n </italic>corresponds to the set <italic>n </italic>= <italic>{</italic>0, 1, . . ., <italic>n</italic> − 1<italic>}</italic>, and the target domain <italic>k </italic>is the same as the scalar ring or field of polynomials. The same approach has been applied when evaluating multivariate polynomials using <italic>n</italic>-tuples of numbers [10].
This formalization aims at providing basic notions of the field which enable to formalize geometric objects such as algebraic curves which is used e.g. in coding theory [11] as well as further formalization of the fields [8] in the Mizar system, including the theory of polynomials [6].
</abstract>

A classical algebraic geometry is study of zero points of system of multivariate polynomials [3], [7] and those zero points would be corresponding to points, lines, curves, surfaces in an affine space. In this article we give some basic definition of the area of affine algebraic geometry such as algebraic set, ideal of set of points, and those properties according to [4] in the Mizar system[5], [2].
We treat an affine space as the n-fold Cartesian product kn as the same manner appeared in [4]. Points in this space are identified as n-tuples of elements from the set k. The formalization of points, which are n-tuples of numbers, is described in terms of a mapping from n to k, where the domain n corresponds to the set n = {0, 1, . . ., n − 1}, and the target domain k is the same as the scalar ring or field of polynomials. The same approach has been applied when evaluating multivariate polynomials using n-tuples of numbers [10].
This formalization aims at providing basic notions of the field which enable to formalize geometric objects such as algebraic curves which is used e.g. in coding theory [11] as well as further formalization of the fields [8] in the Mizar system, including the theory of polynomials [6].

Introduction to Algebraic Geometry

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

{"article-title":"Introduction to Algebraic Geometry"}

A classical algebraic geometry is study of zero points of system of multivariate polynomials [3], [7] and those zero points would be corresponding to points,...

Introduction to Algebraic Geometry

Published Online: Oct 04, 2023

Page range: 67 - 73

Accepted: Jun 30, 2023

DOI: https://doi.org/10.2478/forma-2023-0007

Keywords
affine algebraic set, multivariate polynomial

© 2023 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Introduction to Algebraic Geometry

Published Online: Oct 04, 2023

Page range: 67 - 73

Accepted: Jun 30, 2023

DOI: https://doi.org/10.2478/forma-2023-0007

Keywordsaffine algebraic set, multivariate polynomial

© 2023 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Keywords
affine algebraic set, multivariate polynomial