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