Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

Regular Paper

代数幾何の形式化について
On the Formalizations of Algebraic Geometry
渡瀬 泰成 1,*
Yasushige Watase1,*
1 東京都杉並区松ノ木 3-21-6* yasushige.watase@gmail.com
Proof checked by Mizar Version: 8.1.11 and MML Version: 5.65.1394
Received: December 16, 2021. Accepted: May 16, 2022.

Abstract
In the article we formalized introductory basic deﬁnitions and propositions of Algebraic Geometry. The formalization in the article is covered the ﬁrst half of chapter 1
of [1]. Namely “Algebraic Set”, “Ideal of an Algebraic Set” and related propositions.
Throughout the article we denote k n a set theoretical n-ple product of a ﬁeld or ringk. In actual coding Funcs(n, k) is regarded as k n . We introduced modiﬁed evaluation
function (E eval) for multivariate Polynomial and its ﬁrst argument requires Element of
Polynom-Ring(n,k) to avoid using transformation of Polynomial attribute to Elementof Polynomial Ring.

はじめに

1

代数幾何の初歩的な定義と関連の命題群とその証明の形式化を行った．対象として扱う空間は可換環，体 k の直積集合 k n をとる．k n の点は k の要素の n 個の対 (n-tuple) に対応する．具体的には代数的集合と k n の部分集合を零点に持つ多項式から生成されるイ
デアルの定義と関連の命題群とその証明の形式化を行った．形式化の過程で多変数多項式環に関連する定理で証明の困難な点も考察する．

2

アフィン代数幾何の形式化概略

2.1

形式化の動機

代数幾何の形式化は以下の点で重要と考える．

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

1/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)i) Mizar ライブラリに未だ形式化されていない．
ii) 可換代数の具体的応用例を与え，また可換代数論，多項式環の命題群の形式化iii) 楕円曲線論も代数曲線の例であり，代数幾何の形式化が符号理論，学習理論など工学的分野で応用される事が期待される．

iv) 他の証明検証システムでは ISABEL によるスキーム論が形式化されている [2]．本
稿ではより具体性のある古典的代数幾何を題材に形式化を行い応用し易いライブラ
リ構築を目指す．

2.2

形式化の範囲2.2.1

対象となる空間

幾何として対象となるのはアフィン空間であり, 体 k に対し，アフィン空間として k nをとり理論を展開する．k n をベクトル空間とみて GL(n, k) の作用と k n とベクトルの平行移動の合成を変換群とする幾何である．本形式化ではアフィン幾何に関連する内容には触れず, 単なる k の要素の n 個の対 (n-tuple) の集合として形式化を進める．従ってベクトル空間を要求しないので k は体である必要はなく, 可換環で成り立つ定理は k は可換環としている．n 個の対 n-tuple は n → k として形式化する．これは n 変数多項式への代入との親和性を優先した．全空間 k n はすべての n → k となり Funcs(n, k) により形式化した．一方既存 M M L で数ベクトル空間 n-VectSp overk は [3] に於いて定義，形式化されている．しかしながら n-VectSp overk の点は Seg n → k で形式化され k n の n-tuple と0 を基点とする, しないの食い違いがあり効率よく既存線形空間論のライブラリからの結果が利用できない．

2.2.2

形式化の項目i) 代数的集合ii) 既約な代数的集合iii) i),ii) に付随した命題群の形式化
形式化の過程で認識された困難な点は後述し考察を加える．

2.2.3

形式化の底本選定

本形式化で参考，底本とした教科書は

i) Fulton の教科書「代数曲線」[1]ii) 秋月康夫，中井喜和，永田雅宜の教科書「代数幾何学」[4]
Fulton の教科書 i) は世界的に定評があり ii) は i) の構成と重なり，証明の細部の省略も少なく i) の参考書として利用できる．

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

2/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

2.3

形式化の実際

2.3.1

多項式の零点集合, 多項式の集合の共通零点の形式化

一変数の多項式の零点集合は Roots として POLYNOM5:def 10 で形式化されているが，n 変数の多項式に対応するように拡張し新規に定義した．

Listing 1. ALGGEO 1 - def 6
deﬁnition ::Zero set of f
let R,n;let f be Polynomial of n,R;
func Roots(f) −> Subset of Funcs(n,[#]R) equals{x where x is Function of n,R : eval(f,x) = 0.R};
end;

この関数によって以下の多項式の集合 S に対する共通零点集合，即ち S の要素すべてに零点となる点を共通零点すべてを定義する．この定義の形式化には関数 Zero を導入して S の要素の共通零点定義することから始める．

Listing 2. ALGGEO 1 - def 7
deﬁnition ::Zero set of S ={F1,F2,...Fn}
let R,n,S;func Zero (S) −> Subset of Funcs(n,[#]R) equals:: ALGGEO 1:def 7
meet {Roots(f) where f is Polynomial of n,R : f in S};
end;

関数 Zero では，任意の S の要素 x : n → k で多項式の集合 F の要素を評価しているが，Polynomial of n, k が S に属するという条件で言い換えている．多項式環 k[X1 , X2 . . . Xn ]の要素は Mizar での属性は Polynomial of n, k ではなく Element of Polynom-Ring(n, k)となる．Element of Polynom-Ring(n, k) 属性のままで計算する場合 Polynomial 属性を引数にとる既存評価関数 eval は利用できず不便なので，Element of Polynom-Ring 属性
を引数にとる評価関数 E eval を導入しておく．

Listing 3. ALGGEO 1 - def 4
deﬁnition
let n be Ordinal, L be right zeroed add−associative right complementablewell−unital distributive non trivial doubleLoopStr;
let f be Element of Polynom−Ring (n,L),x be Function of n,L;
func E eval(f,x) −> Element of L means:: ALGGEO 1:def 4
ex p be Polynomial of n,L st p = f & it = eval(p,x);end;

このように Element of Polynom-Ring(n, k) 属性に対応した定義だと有限の多項式の列 F に対する評価も以下のように定義可能となる．

Listing 4. ALGGEO 1 - def 5
deﬁnition
let R,n,F,x;
func E eval(F,x) −> FinSequence of the carrier of R means:: ALGGEO 1:def 5
dom it = dom F & for i be Nat st i in dom F holds it.i = E eval(F/.i,x);
end;

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

3/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)多項式環の要素の属性で共通零点集合の定義を言い換えると以下の通りである．
定理 1

Zero (S) = {x ∈ k n |∀f (element of Polynomial Ring) ∧ f ∈ S, E eval(f, x) = 0.R}

2.3.2

代数的集合

定義 1 k を体とし，k n の部分集合 V が n 変数多項式環 k [x1 , x2 . . . xn ] の有限個の部分
集合 S = {F1 (x1 , x2 . . . xn ), · · · Fr (x1 , x2 . . . xn )} の要素 Fi 達の共通零点となるとき V を
代数的集合という．

k n の部分集合が代数的集合であるという述語は以下の attr と mode を用いて形式化した．attr zero points derived は点集合が零点から由来した集合であるという性質を記述
し，代数的集合は零点由来の集合を表すものとして mode で定義した．

Listing 5. ALGGEO 1 - Th.16
deﬁnition
let R,n;let IT be Subset of Funcs(n,[#]R);
attr IT is zero points derived means:: ALGGEO 1:def 8
ex S be non empty Subset of Polynom−Ring(n,R) st IT = Zero (S);end;registration
let R,n;cluster zero points derived for non empty Subset of Funcs(n,[#]R);end;
deﬁnition
let n,R;
mode Algebraic Set of n,R iszero points derived non empty Subset of Funcs(n,[#]R);
end;

2.3.3

零点集合の性質

零点集合の性質として命題群が証明される．以下はその例である．
命題 1∀f, g ∈ R[x1 , x2 , . . . xn ], Zero (f g) = Zero (f ) ∪ Zero (g) holds.
Mizar での形式化は，Listing 6. ALGGEO 1 - Th.21
theorem :: ALGGEO 1:21
for R be non degenerated domRing, f,g be Polynomial of n,R holds
Zero ({f∗’g}) = Zero ({f}) \/ Zero ({g});

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

4/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

命題 2∀a = (a1 , a2 , . . . , an ) ∈ Rn , Zero ({x1 − a1 , x2 − a2 , . . . , xn − an }) = a holds.
Mizar での形式化は，Listing 7. ALGGEO 1 - Th.24
theorem :: ALGGEO 1:24
for a be Function of n,R holds Zero (polyset(a)) = {a};ここでは {x1 − a1 , x2 − a2 , . . . , xn − an } を polyset(a) と関数化してしまっているが，要素 xi − ai は以下の HILBASIS : def3 で定義されている単項式 1 1 [5] を利用して形式化を行った．

Listing 8. ALGGEO 1 - def.10
deﬁnition
let n,R;
let a be Function of n,R, i be Element of n;
func wpoly(a,i) −> Element of Polynom−Ring(n,R) equals:: ALGGEO 1:def 10
1 1(i,R) − (a.i)∗1 (n,R);
end;

2.3.4

k n の部分集合のイデアルの形式化

定義 2 k n の部分集合 X をとり，X のすべて点でゼロとなる多項式全体を I(X) と定義
し X のイデアルと称す．
この形式化は以下の様にの通り X のすべて点でゼロとなる多項式全体に対応付ける関
数 Ideal を定義することによる．

Listing 9. ALGGEO 1 - def.11
deﬁnition ::Ideal of X c= Funcs(n,R);
let R, n, X;
func Ideal X −> non empty Subset of Polynom−Ring(n,R) equals:Def11:{f where f is Polynomial of n,R : X c= Roots(f)};

I(X) は多項式環のイデアルになることが示され「X のイデアル」と呼ばれる所以で
ある．

2.3.5

既約/可約な代数的集合

代数的集合に既約・可約の概念を以下のように定義する．はじめに可約を定義し，その否定により既約を定義する．
定義 3 k n の代数的集合 V が可約であるとは代数的集合 V1 , V2 が存在し V1

neqV2 ∧ V = V1 ∪ V2 をみたすときをいう．V が可約でないとき既約という．

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

5/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

関数 Zero と関数 Ideal の相互作用

2.3.6

関数 Zero と関数 Ideal を用いた命題群が証明される．
命題 3 X, Y ⊂ k n , S ⊂ k[x1 , x2 . . . xn ], V を k n の代数的集合とする．この時以下が成立
する．

1. X ⊂ Y ⇒ Ideal Y ⊂ Ideal X,
2. Ideal (∅) = k[x1 , x2 . . . xn ],3. (0) ⊂ Ideal (k n ),4. Ideal (Zero (S)) ⊃ S,
5. Zero (Ideal (X)) ⊃ X,
6. Zero (Ideal (Zero (S))) = Zero S,
7. Ideal (Zero (Ideal (X))) = Ideal X,
8. V = Ideal (Zero V ).
上記命題の項番 3. は k が無限体であれば等号が成立する．証明には以下の命題が必要
である．
命題 4

∀f ∈ k[x1 , x2 . . . xn ] ∧ f is non-zero ⇒ ∃a ∈ k n st f (a) ̸= 0.k
命題 4. の証明は MML ライブラリーの既存定理から導出は今のところ成功していな
い．既存の多項式の評価関数では証明が出来ない．次節でこの問題を考察する．

多変数多項式の評価関数について

3

前節で取り上げた命題 4. の証明を難しくしている点を解説する．まずは問題を単純化し問題を考察する．

3.1

問題

命題 5 k を無限個の元を含む体，f (x, y) を恒等 0 でない k 係数 2 変数の多項式とする．
このとき f (a, b) ̸= 0 となる (a, b) は無限個存在する．
この証明のスケッチは，「f (a, y) が恒等 0 とならない様に x = a を選ぶ，そうしてできた k[y] の多項式 f (a, y) の零点の個数は次数を超えないので有限個よって f (a, b) ̸= 0 となる (a, b) は無限個存在する．
」
この証明で形式化できない点は f (a, y) のように不定元を選択して評価することにある．f (x, y) を k[x][y] の多項式と見做すことは可能である．fˆx (y) ∈ k[x][y] と表記する．
しかしこれを一変数の多項式と考えて eval 関数では k[x] の要素を代入しての評価となる．

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

6/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

係数部分を先 k の要素 a で eval 関数で評価したものを fˆa (y) と表記すれば，これは k[y]の要素として k の要素で評価される．fˆa (y) を可能にする部分評価関数と言うべきものが必要である．この部分評価関数と既存関数が両立すること，即ち f (a, b) = eval(f, (a, b))と fˆa (y) が等しいことを確かめれば，命題 5. の証明の形式化も現実的となる．

4

今後の形式化
前章で考察した問題の解決が最優先の課題であり，提示した部分評価関数も Bag 演算を整備して応用のし易い関数として開発することである．Mizar の 40 年の長きにわたる
歴史においてこの多項式の分野は取り扱いづらい分野の一つと思われる．形式化実績の積
み重ね，汎用性のある有用なライブラリ構築が期待される．代数的集合の既約分解の導入にはイデアルの分解も関連するので準素イデアル [6] の続編も必要となる．代数幾何の形
式化は可換環, 多項式環， ネター空間論にまたがる分野であり MML ライブラリを総動員し活用しないと形式化でいないので Mizar システムのみならずプログラミング技術も試される場である.
多項式環自体は具体的な題材であるが扱うには十分複雑な代数構造であることが形式化を通して工数がかさむことで理解される．より単純な代数構造上の幾何から形式化を進めるアプローチもある．半群上の幾何， 所謂トロピカル幾何や工程計画問題 [7] に応用される Max-Plus 代数の形式化を進めるアプローチも今後の考慮したい．

参考文献[1] Fulton W. Algebraic Curves. The Benjamin/Cummings Publishing Company; 1969.
[2] Bordg A, Paulson L, Li W.
etry.

Grothendieck’s Schemes in Algebraic Geom-

Archive of Formal Proofs. 2021 Mar;https://isa-afp.org/entries/

Grothendieck_Schemes.html, Formal proof development.
[3] Lango A, Bancerek G. Product of Families of Groups and Vector Spaces. Formalized
Mathematics. 1992;3(2):235–240. Available from: http://fm.mizar.org/1992-3/
pdf3-2/prvect_1.pdf.
[4] Akizuki Y, Nakai Y, Nagata M. Algebraic Geometry. Iwanami Shoten (in Japanese);
1987.
[5] Backer J, Rudnicki P.
2001;9(3):583–589.

Hilbert Basis Theorem.

Available from:

Formalized Mathematics.

http://fm.mizar.org/2001-9/pdf9-3/

hilbasis.pdf.
[6] Watase Y. On Primary Ideals (in press). Formalized Mathematics. 2021;29(2).
[7] 小林 正典. Tropical geometry and its application to scheduling problem. 代数幾何学
シンポジウム記録. 2021 jan;(2020):106–114. Available from: https://ci.nii.ac.

jp/naid/120006952786/.

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

7/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

Mizar article information
Works in Progress
ALGGEO 1 Intrduction to Algebraic Geometryby Yasushige Watase
Summary: In the article we formalized introductory basic deﬁnitions and propositionsof Algebraic Geometry. The formalization in the article is covered the ﬁrst half of chapter
1 of [1]. Namely ”Algebraic Set”, ”Ideal of an Algebraic Set” and related propositions.
Throughout the article we denote k n a set theoretical n-ple product of a ﬁeld or ringk. In actual coding Funcs(n, k) is regarded as k n . We introduced modiﬁed evaluation
function (E eval) for multivariate Polynomial and its ﬁrst argument requires Element of
Polynom-Ring(n,k) to avoid using transformation of Polynomial attribute to Elementof Polynomial Ring.
Listing 10. ALGGEO 1 - abstract:: Introduction to Algebraic Geometory I:: by Yasushige Watase:::: Received May 27, 2019:: Copyright (c) 2019−2021 Association of Mizar Users:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence:: version 3.0 or later, or the Creative Commons Attribution−ShareAlike:: License version 3.0 or later, subject to the binding interpretation:: detailed in ﬁle COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC−BY−SA for the full text of these:: licenses, or see http://www.gnu.org/licenses/gpl.html and:: http://creativecommons.org/licenses/by−sa/3.0/.
environvocabularies NUMBERS, SUBSET 1, RELAT 1, ORDINAL4, FINSEQ 1, XBOOLE 0,
FUNCT 1, XXREAL 0, TARSKI, NAT 1, ARYTM 3, ZFMISC 1, CARD 1, YELLOW 8,
ORDINAL1, ARYTM 1, PRE POLY, QC LANG1, GROUP 1, ALGSTR 0, RLVECT 1,
VECTSP 1, POLYNOM1, POLYNOM2, AFINSQ 1, FINSEQ 2, CARD 3, SQUARE 1,
STRUCT 0, PARTFUN1, FINSET 1, SUPINF 2, FUNCOP 1, ALGSEQ 1, RATFUNC1,FUNCT 2, HILBASIS, VECTSP 2, CARD FIL, RSSPACE, IDEAL 1, MESFUNC1, INT 2,
SETFAM 1, XCMPLX 0, PRE TOPC, POLYNOM5, LATTICES, BSPACE, NEWTON, RING 1,
ALGGEO 1;
notationsTARSKI,XBOOLE 0, XTUPLE 0, ZFMISC 1, SUBSET 1, SETFAM 1, RELAT 1, FUNCT 1,
ORDINAL1, RELSET 1, PARTFUN1, MCART 1, FUNCT 2, BINOP 1, DOMAIN 1,
FUNCOP 1, FUNCT 4, FINSET 1, CARD 1, PBOOLE, ORDERS 1, NUMBERS, XCMPLX 0,
XXREAL 0, XREAL 0, NAT 1, INT 1, MEMBERED, VALUED 0, INT 2, NAT D,
CLASSES2, FINSEQ 1, FINSEQ 2, VALUED 1, RVSUM 1, AFINSQ 1, FINSEQ 7,
PRE POLY, STRUCT 0, ALGSTR 0, ORDERS 2,PRE TOPC, RLVECT 1, GROUP 1,
VECTSP 1, ALGSTR 1, VECTSP 2, GROUP 2, GROUP 3, POLYNOM1, ALGSEQ 1,
PRVECT 1, BINOM, POLYNOM2, POLYNOM3, POLYNOM4, POLYNOM5, UPROOTS, GROUP 9,
HURWITZ, IDEAL 1, RING 1, RING 2, POLYALG1, HILBASIS, POLYNOM7, GROEB 1,
RATFUNC1, GROUP 1A, RING 4, HILB10 2, FIELD 1;
constructors
TARSKI, XTUPLE 0, ZFMISC 1, SUBSET 1, SETFAM 1, RELAT 1, RELAT 2, RELSET 1,
RECDEF 1, DOMAIN 1, ORDINAL2, FUNCT 4, PBOOLE, NAT D, BINOP 2, FINSEQ 7,
ORDERS 2, GROUP 1, GROUP 4, FVSUM 1, POLYNOM1, ALGSEQ 1, WAYBEL 4,
PRVECT 1, QUOFIELD, BINOM, POLYNOM2, POLYNOM3, BAGORDER, POLYNOM4,POLYNOM5, UPROOTS, GROUP 9, HURWITZ, HILBASIS, POLYALG1, POLYNOM6,POLYNOM7, GROEB 1, RATFUNC1, GROUP 1A, RING 4, HILB10 2, FIELD 1;

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

8/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

registrations XBOOLE 0, RELAT 1, FUNCT 1, ORDINAL1, XREAL 0, NAT 1, CARD 1,
VALUED 0, VALUED 1, RELSET 1, INT 1, STRUCT 0, VECTSP 1, PRE POLY,
MEMBERED, POLYNOM2, AFINSQ 1, ORDINAL2, POLYNOM6, HILB10 2, XXREAL 0,
SUBSET 1, FUNCT 2, FINSEQ 1, FINSEQ 2, MATRIX11,FVSUM 1, AFINSQ 2,
FUNCOP 1, ALGSTR 1, ALGSTR 0, HILBASIS, PRVECT 1, POLYNOM7, GCD 1,
POLYNOM1, VECTSP 2, POLYALG1, RLVECT 1, GROUP 1A, PRE CIRC, WAYBEL 2,
IDEAL 1, RING 1, RING 2, POLYNOM3, XXREAL 2, UPROOTS,POLYNOM5, PBOOLE,BAGORDER, RELAT 2, ORDERS 2, GROEB 1, TERMORD, BINOM, GROUP 1, MOD 4,
RINGCAT1, ALGSEQ 1;
requirements NUMERALS, SUBSET, ARITHM, REAL;
deﬁnitions TARSKI, XBOOLE 0, MEMBERED, RLVECT 1, ALGSTR 0, STRUCT 0, GROUP 1,
VECTSP 1, SUBSET 1, FUNCT 2;
equalities FINSEQ 1, STRUCT 0, ALGSTR 0, POLYNOM1, VECTSP 1, FINSEQ 2,
ORDINAL1, SUBSET 1, AFINSQ 1, XBOOLE 0, FUNCT 2, BINOP 1, FUNCOP 1;
expansions POLYNOM1, FUNCT 2, ORDINAL1,IDEAL 1, SUBSET 1,FUNCT 1, BINOP 1,
VECTSP 2, RLVECT 1, ALGSTR 0, GROUP 2, TARSKI, STRUCT 0, VECTSP 1,
GROUP 1, XBOOLE 0, ZFMISC 1, GROUP 6, INT 1;
theorems TARSKI, FUNCT 1, CARD 1, NAT 1, ZFMISC 1, XREAL 1, FINSEQ 3,
FINSEQ 1, FINSEQ 5, FINSEQ 2, ORDINAL1, HILB10 3, XBOOLE 0, RELAT 1,
PRE POLY, FUNCT 2, POLYNOM1, POLYNOM2, FUNCOP 1, PARTFUN1,XBOOLE 1, RLVECT 1, POLYNOM7, SUBSET 1, IDEAL 1, ALGSTR 1, RING 1,
SETFAM 1, BINOM, GROUP 1, XCMPLX 1, FVSUM 1, VECTSP 2, TARSKI 0,
HILBASIS, XXREAL 0, TOPZARI1;
schemes FINSEQ 2, NAT 1;
begin :: Preliminaries
reserve K for Field;
reserve R for non degenerated comRing;
reserve o,o1,x,x1,y,y1 for object;reserve q,I for Ideal of R;
reserve n for non zero Nat;
reserve m,d,i,j for Nat;
reserve S,T for non empty Subset of Polynom−Ring(n,R);
reserve F,G for FinSequence of the carrier of Polynom−Ring(n,R);
reserve X for non empty set;
reserve A for non empty set;
reserve x1,x2,z for set;
reserve A,B for non empty set;:: Aﬃne Space (X,V)
deﬁnition ::numerical spacelet R, n;func NumSp(R,n) −> non empty set equals:: ALGGEO 1:def 1
Funcs(n,[#]R);
end;
reserve t for Element of n−tuples on [#]R;reserve t1 for FinSequence of [#]R;
deﬁnition
let n be Nat;
let K be Field;
let p be n−element [#]K−valued XFinSequence;func @p −> Function of n,K equals:: ALGGEO 1:def 2
p;end;
deﬁnition
let n be Nat;
let K be Field;

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

9/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

let p be n−element [#]K−valued XFinSequence;func @p −> Function of n,K equals:: ALGGEO 1:def 3
p;end;
deﬁnition
let n be Ordinal, L be right zeroed add−associative right complementablewell−unital distributive non trivial doubleLoopStr,
p be Polynomial of n,L;
redeﬁne func {p} −> Subset of Polynom−Ring(n,L);
end;
deﬁnition
let n be Ordinal, L be right zeroed add−associative right complementablewell−unital distributive non trivial doubleLoopStr;
let f be Element of Polynom−Ring (n,L),x be Function of n,L;
func E eval(f,x) −> Element of L means:: ALGGEO 1:def 4
ex p be Polynomial of n,L st p = f & it = eval(p,x);
end;::new Function for FinSeq of Polynomial is introduced
reserve x for Function of n,R;deﬁnition
let R,n,F,x;
func E eval(F,x) −> FinSequence of the carrier of R means:: ALGGEO 1:def 5
dom it = dom F & for i be Nat st i in dom F holds it.i = E eval(F/.i,x);
end;
theorem :: ALGGEO 1:1
for N0 be Nat for x,F st len F = N0+1 holds
E eval(F,x) = (E eval(F|N0,x))ˆ<∗E eval(F/.(len F),x)∗>;theorem :: ALGGEO 1:2
for x,F st len F = 0 holds E eval(Sum F,x) = Sum E eval(F,x);theorem :: ALGGEO 1:3
for x,F st len F <> 0 holds E eval(Sum F,x) = Sum E eval(F,x);theorem :: ALGGEO 1:4
for F be FinSequence of the carrier of Polynom−Ring(n,R),x be Function of n,R holds E eval(Sum F,x) = Sum E eval(F,x);theorem :: ALGGEO 1:5
for G be FinSequence of the carrier of R holds
G = (len G)|−> 0.R iﬀ (for i be Nat st i in dom G holds G.i = 0.R);
theorem :: ALGGEO 1:6
for n be Nat holds
Sum (n|−>0.R) = 0.R;
deﬁnition ::Zero set of f
let R,n;let f be Polynomial of n,R;
func Roots(f) −> Subset of Funcs(n,[#]R) equals:: ALGGEO 1:def 6{x where x is Function of n,R : eval(f,x) = 0.R};
end;
theorem :: ALGGEO 1:7
Roots(0 (n,R)) = Funcs(n,[#]R);
theorem :: ALGGEO 1:8
Roots(1 (n,R)) = {};MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

10/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)::1.2 Aﬃne Space and Algebraic Sets::reserve S,T for non empty Subset of Polynom−Ring(n,R);deﬁnition ::Zero set of S ={F1,F2,...Fn}
let R,n,S;func Zero (S) −> Subset of Funcs(n,[#]R) equals:: ALGGEO 1:def 7
meet {Roots(f) where f is Polynomial of n,R : f in S};
end;
theorem :: ALGGEO 1:9
for n,R,S holds{Roots(f) where f is Polynomial of n,R : f in S} <> {};theorem :: ALGGEO 1:10
Zero (S) = {} implies{x where x is Function of n,R : for f be Element of Polynom−Ring(n,R)
st f in S holds E eval(f,x) = 0.R} ={};
theorem :: ALGGEO 1:11
Zero (S) <> {} implies
Zero (S) ={x where x is Function of n,R : for f be Element of Polynom−Ring(n,R)
st f in S holds E eval(f,x) = 0.R};
theorem :: ALGGEO 1:12
Zero (S) ={x where x is Function of n,R : for f be Element of Polynom−Ring(n,R)
st f in S holds E eval(f,x) = 0.R};
theorem :: ALGGEO 1:13
for p be Polynomial of n,R holds Zero ({p}) = Roots(p);theorem :: ALGGEO 1:14
for o be Function of n,R holds (not o in Zero (S)) implies(ex f be Polynomial of n,R st f in S & not o in Roots(f));
theorem :: ALGGEO 1:15
Zero ({0 (n,R)}) = Funcs(n,[#]R);
theorem :: ALGGEO 1:16
S c= T implies Zero (T) c= Zero (S);theorem :: ALGGEO 1:17
Zero (S\/T) = Zero (S)/\Zero (T);::::::::::::::::::::::::::::::::::::::::::::::::::::::::2.10.2021
theorem :: ALGGEO 1:18
Zero (S) = Zero (S−Ideal);deﬁnition
let R,n;let IT be Subset of Funcs(n,[#]R);
attr IT is zero points derived means:: ALGGEO 1:def 8
ex S be non empty Subset of Polynom−Ring(n,R) st IT = Zero (S);end;theorem :: ALGGEO 1:19[#]Funcs(n,[#]R) is zero points derived;
registration
let R,n;cluster zero points derived for non empty Subset of Funcs(n,[#]R);end;
deﬁnition

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

11/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

let n,R;
mode Algebraic Set of n,R iszero points derived non empty Subset of Funcs(n,[#]R);end;
deﬁnition
let R,n;let IT be Subset of Funcs(n,[#]R);
attr IT is Alg Set means:: ALGGEO 1:def 9
ex S be non empty Subset of Polynom−Ring(n,R) st IT = Zero (S);end;theorem :: ALGGEO 1:20
for Z be Algebraic Set of n,R holds
ex I be Ideal of Polynom−Ring(n,R) st Z = Zero (I);theorem :: ALGGEO 1:21
for R be non degenerated domRing, f,g be Polynomial of n,R holds
Zero ({f∗’g}) = Zero ({f}) \/ Zero ({g});theorem :: ALGGEO 1:22 :::Integral Domain requires
for R be non degenerated domRing, I,J be Ideal of Polynom−Ring(n,R),
M be non empty Subset of Polynom−Ring(n,R) st
M = rng ((the multF of Polynom−Ring(n,R))|[:I,J:]) holds
Zero (I) \/ Zero (J) = Zero (M);theorem :: ALGGEO 1:23
for a be Element of R,x,i be Element of n holds
1 1(i,R) is Polynomial of n,R & a|(n,R) is Polynomial of n,R;deﬁnition
let n,R;
let a be Function of n,R, i be Element of n;
func wpoly(a,i) −> Element of Polynom−Ring(n,R) equals:: ALGGEO 1:def 10
1 1(i,R) − (a.i)∗1 (n,R);
end;
deﬁnition
let n,R;
let a be Function of n,R;
func polyset(a) −> non empty Subset of Polynom−Ring(n,R) equals:: ALGGEO 1:def 11{ f where f is Element of Polynom−Ring(n,R):
ex i be Element of n st f = wpoly(a,i)};end;
theorem :: ALGGEO 1:24
for a be Function of n,R holds Zero (polyset(a)) = {a};deﬁnition let X be non empty set;mode Point of X is 1−element Subset of X;
end;::1.3 The Ideal of a Set of Points
reserve X,Y for Subset of Funcs(n,[#]R);
reserve a for Function of n,R;deﬁnition ::Ideal of X c= Funcs(n,R);
let R, n, X;
func Ideal X −> non empty Subset of Polynom−Ring(n,R) equals:: ALGGEO 1:def 12{f where f is Polynomial of n,R : X c= Roots(f)};end;theorem :: ALGGEO 1:25

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

12/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

for p, q being Element of Polynom−Ring(n,R) st p in Ideal X & q in Ideal X
holds p + q in Ideal X;
theorem :: ALGGEO 1:26
for a, p being Element of Polynom−Ring(n,R) st p in Ideal X holdsa∗p in Ideal X;
theorem :: ALGGEO 1:27
for a, p being Element of Polynom−Ring(n,R) st p in Ideal X holdsp∗a in Ideal X;
theorem :: ALGGEO 1:28
for X holds Ideal X is Ideal of Polynom−Ring(n,R);
registration
let R, n, X;
cluster Ideal X −> add−closed for Subset of Polynom−Ring(n,R);
cluster Ideal X −> right−ideal for Subset of Polynom−Ring(n,R);
end;::(6) If X c= Y , then I(Y) c= I(X).
::(7) I({}) = k[X1,...,Xn]; I(An) = (0) if k is an inﬁnite ﬁeld;::I({(a1,...,an)}) = (X1 − a1,...,Xn − an) for a1,...,an \in k.
::(8) S c= I(V(S))for any set S of polynomials; X c= V (I(X))for any set X of::points.
::(9) V (I(V (S))) = V (S) for any set S of polynomials, and I(V (I(X))) = I(X) ::for any set X of points. So if V isan algebraic set, V = V (I(V )), and::if I is the ideal of an algebraic set, I = I(V (I)).
theorem :: ALGGEO 1:29 ::(6)X c= Y implies Ideal Y c= Ideal X;
theorem :: ALGGEO 1:30 ::(7)X = {} implies Ideal X = [#]Polynom−Ring(n,R);
theorem :: ALGGEO 1:31 ::(7)X = Funcs(n,[#]R) implies {0.Polynom−Ring(n,R)} c= Ideal (X);theorem :: ALGGEO 1:32
for S be non empty Subset of Polynom−Ring(n,R) holds S c= Ideal (Zero (S));
theorem :: ALGGEO 1:33
S c= Ideal (Zero (S));
theorem :: ALGGEO 1:34 ::(8)X c= Zero (Ideal X);
theorem :: ALGGEO 1:35 ::(9)Zero (Ideal (Zero S)) = Zero S;
theorem :: ALGGEO 1:36 ::(9)Ideal (Zero (Ideal X)) = Ideal X;
theorem :: ALGGEO 1:37 ::(9)for X be Algebraic Set of n,R holds X = Zero (Ideal X);
deﬁnition
let R,n;let IT be Algebraic Set of n,R;
attr IT is reduciblemeans:: ALGGEO 1:def 13
ex V1,V2 be Algebraic Set of n,R st IT = V1 \/ V2 & V1 <> V2;
end;notation

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

13/14

Mechanized Mathematics and Its Applications, Works in Progress

Formalizations of Algebraic Geometry (Watase Y.)

let R,n;let V be Algebraic Set of n,R;antonym V is irreducible for V is reducible;
end;

MMA-WiP (2022), vol.4, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2022.4.3 - ISSN 2434-5458 (Online)

14/14