Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

Regular Paper

ザリスキ位相Zariski Topology
渡瀬 泰成 *
Yasushige Watase** ywatase@ss.iij4u.or.jp
Proof checked by Mizar Version: 8.1.08 and MML Version: 5.53.1335
Received: November 28, 2018. Accepted: April 11, 2019.

Abstract
This paper introduces a new MML article recently posted and appeared in [1]. The
article provides some definitions and theorems about prime ideals of rings that have notbeen formalized and Zariski Topology is formalized. The article is based on the firstchapter of [2].

1

TOPZARI1 の概要
本稿は，FM 誌 26(4),2018 に投稿したザリスキ位相の形式化を行ったアーティクル(TOPZARI1) の内容についての報告である．形式化した内容は，可換環の素イデアルの諸定義と定理，そして素イデアルからなる集合に位相構造を与えるザリスキ位相である．
形式化にあたり文献 [2] の 1 章を参考にした．以下断わらないに限り環と言えば可換環とし，A, B は単位的可換環を表す．また特に零環を含めた可換環の場合は R を用いた．

2

新たに形式化し追加した定義類
素イデアルのスぺクトル，べき零元，零根基，ジャコブソン根基，局所環を定義した．

また形式証明を簡潔に見やすくする工夫として幾らかの関数（Mizar では Functor と称す）を定義した．まず関数の定義の説明から始める．

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

1/12

Mechanized Mathematics and Its Applications, Works in Progress

2.1

Zariski Topology (Watase Y.)

相対的イデアルの集合や素イデアルの集合

RING 2 : def3 で定義された関数 Ideals A は A のイデアル全体の為す集合を表している．相対的の意味は，ここでは例えば A の部分集合 S を含むイデアルや，S と交わらないイデアルといったような条件を伴うイデアルを考える場合を指す．

• Ideals(A, S) は A の部分集合 S を含むイデアル全体の集合を表す．(TOPZARI1 : def1)• Ideals(A, J, f) は A の部分集合 J を含むイデアルのうち multClSet(f) と交わらないもの全体の集合を表す．ここで multClSet(f) は A の元 ｆ で生成する積閉集合を表す．(TOPZARI1 : def4)• Spectrum R は R の素イデアル全体の集合を表す．(TOPZARI1:def 5)• m-Spectrum R は R の極大イデアル全体の集合を表す．(TOPZARI1:def 7)• PrimeIdeals(R, E) は R の部分集合 E を含む素イデアル全体の集合を表す．
(TOPZARI1:def 11)
次に環論に関する定義を形式化した．

2.2

局所環，半局所環• 局所環とは，唯一の極大イデアルを持つ環と定義される．書籍の記述のようなインフォーマルな記述では短く表現されるが，形式化するには長くなる．例えば任意の2 つの極大イデアルは一致すると表現して形式化することになる．ここでは極大ス
ペクトルを用い簡潔な表現とした．

ex m be Ideal of A st m-Spectrum A = {m}; (TOPZARI1:def 9)• 半局所環は，有限個の極大イデアルを持つ環と定義される．これも極大スペクトルを用い簡潔になる．

m-Spectrum A is finite; (TOPZARI1:def 10)• 冪零元 A の元 a が冪零とは非負整数 k が取れて元 a の k 乗が零となること．
ex k being non zero Nat st ak = 0.A; (TOPZARI1:def 2)• ジャコブソン根基とは，すべての極大イデアルの共通部分．
J-Rad A = meet m-Spectrum A; (TOPZARI1:def 14)

3

イデアル関連の定理群
ここでは 2 つの定理の形式化証明の概略をしめす．

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

2/12

Mechanized Mathematics and Its Applications, Works in Progress

3.1

Zariski Topology (Watase Y.)

定理 8 (TOPZARI1:8) の説明『環 A には A の真のイデアル J を含む極大イデアルが存在すること』の形式証明の素描を以下の様に示す．

• Ideals(A, J, f) は包含関係に関して半順序集合となり上昇列は極大元を持つ．ここで√f は f ̸∈ J となる元とする．
Ideals(A,J,f) has upper Zorn property wrt RelIncl(Ideals(A,J,f) ); (TOPZARI1:6)• Ideals(A, J, f) の極大元は極大イデアルとなる．
ex m be prime Ideal of A st not f in m & J c= m; (TOPZARI1:7)
ここで，f = 1.A として以下を得る．

• 任意の環 A に真のイデアル J を含む極大イデアルが存在する．
ex m be maximal Ideal of A st J c= m; (TOPZARI1:8)
極大イデアルは素イデアルので，書き換えて以下を得る．

• 任意の環 A に真のイデアル J を含む素イデアルが存在する．
ex m be prime Ideal of A st J c= m;

3.2(TOPZARI1:9)

定理 18 (TOPZARI1:18) の説明

イデアル J の根基は，すべての J を含む素イデアルの共通部分に等しい．インフォー
マルには以下の様に記述される．

√

J=

∩

p (インフォーマル)J⊆p,p∈spec A

記号を整備してあるので，Mizar での表記も TOPZARI1:18 として以下の簡潔さを保ち形式化される．

sqrt J = meet PrimeIdeals(A, J); (フォーマル)√∩
次に証明の流れを見る．まず J ⊂ p (J ⊆ p) を示す．
左辺から任意の元 x を取ると，ある自然数 k が取れて，xk ∈ J となる．実は任意の素イデアル p に対して，xk ∈ p ならば x ∈ p が TOPZARI1 : 16 により成り立つ．よって

x は右辺に入る．
√∩
次に J ⊃ p (J ⊆ p) を示す．
『x が右辺の元ならば x は左辺に入る』の対偶は，√『x ̸∈ J ならば ∃p st x ̸∈ p & J ⊆ p』となり，これは前出定理 9 で示されている．よって証明が完成する．

4

ザリスキ位相ザリスキ位相では，環の素イデアルを点と思って閉集合を定めて位相を入れる．[2] や教科書にあるインフォーマルな表現での定義とフォーマルな形式記述を対比しなが形式化の過程を振り返って見る．

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

3/12

Mechanized Mathematics and Its Applications, Works in Progress

4.1

Zariski Topology (Watase Y.)

インフォーマルなザリスキ位相の定義

A を環とし，X を A のすべての素イデアルからなる集合とする．A の部分集合 E に対して E を含む素イデアルが為す集合を V (E) と表記する．このとき以下が成り立つ．

√(i) E が生成 A のイデアルを a とすると，V (E) = V (a) = V ( a).
(ii) V (0) = X, V (1) = ∅.
(iii) (Ei )i∈I が任意の A の部分集合の族とするとき，∪∩V ( Ei ) =V (Ei ).
i∈Ii∈I(iv) V (a ∩ b) = V (ab) = V (a) ∪ V (b).
以上からすべての V (E) からなる集合は位相空間の閉集合の公理を満たす. この結果得られる位相をザリスキ位相という．

4.2

フォーマルなザリスキ位相の定義

フォーマルな定義の表現，すなわち形式化での位相の入れ方は，閉集合であるための必要十分条件を与え論理スキーム TOPGEN 3 : sch1 を適用して得られる．

Listing 1. TOPGEN 3 - sch 1
scheme :: TOPGEN 3:sch 1
TopDefByClosedPred{X() −> set, C[set]}: ex T being strict TopSpace st thecarrier of T = X() & for A being Subset of T holds A is closed iﬀ C[A]providedC[{}] & C[X()] andfor A,B being set st C[A] & C[B] holds C[A \/ B] andfor G being Subset−Family of X() st for A being set st A in G holds
C[A] holds C[Intersect G];

実際，5.1 の条件 (ii)〜(iv) は TOPGEN 3 : sch1 で与える provides 以下の条件に呼応していることは容易に見て取れる．閉集合を定義する条件 C は spectrumA の任意の部分集合を F とすると，F が閉集合 ⇔ ∃E ⊂ A st F = PrimeIdeals(A, E)
により与えられる．以上をまとめるとザリスキ位相の形式化は以下の様になる．

Listing 2. TOPZARI1 - def 15
definition
let A;
func ZariskiTS(A) −> strict TopSpace means:: TOPZARI1:def 15
the carrier of it = Spectrum A &for F being Subset of it holds F is closed iﬀ(ex E be non empty Subset of A st F = PrimeIdeals(A,E));
end;

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

4/12

Mechanized Mathematics and Its Applications, Works in Progress

4.3

Zariski Topology (Watase Y.)

ザリスキ位相に関連した性質の形式化

ザリスキ位相から導かれる幾らかの性質を証明し，位相の定義がうまく形式化されているか検証してみる．

• ザリスキ位相は T0 空間である．空間の 2 点の分離性が T0 でとは，どちらか一方の点に他を含まない近傍が取れる性質である．また零環に対するザリスキ位相は密着位相となる（ADTS と Mizar では称する）．この条件を満たすことを定理 35 で示す．

Listing 3. TOPZARI1 - Th.35
theorem :: TOPZARI1:35
for P,Q being Point of ZariskiTS A st P <> Q holds
ex V being Subset of ZariskiTS A
st V is open & ( P in V & not Q in V or Q in V & not P in V );この定理と T0 の定義 T 0 を与えている TOPSP:def 7 により証明される．

• 環準同形が誘導する連続写像：環準同形 h : A −→ B は次の連続写像を誘導する．
ah : Spec B −→ Spec A（ここで a h は a h(p) = h−1 (p) で定義され， p は B の素イデアルとする）

Listing 4. TOPZARI1 - def 16
definition ::: similar to ”f from FUNCT 3
let A, B, h;assumeh is RingHomomorphism;func Spec h −> Function of ZariskiTS B, ZariskiTS A means:: TOPZARI1:def 16
for x be Point of ZariskiTS B holds it.x = h”x;end;

この写像が連続であることは，h−1 の閉集合の逆像がまた閉集合となることを示せばよい．これは次の定理により示した．

h is RingHomomorphism implies(Spec h)”PrimeIdeals(A,E) = PrimeIdeals(B,h.:E);

5(TOPZARI1:38)

考察と展望
ここまでの考察と今後の展望に言及する．今回の形式化は簡潔なスタイルで定評のある可換代数の教科書 [2] を底本とした．Mizar は設計の思想から定理の記述をインフォー
マルな自然な表現との両立めざしたものであるため，あらかじめ特定の集合は関数として定義しておき，定理では論理記号や集合の記号が多く並ぶ記述を避ける形式化が実現できた．Mizar での形式化の技法として重要に思われる．
今後はネター空間の諸定理の整備，空間の被約，既約の概念の導入によりネター環のザリスキ位相の性質の形式化が期待される．また純粋に可換環の題材からイデアルの準素分解など今後の形式化の題材となる．

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

5/12

Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

参考文献[1] Watase Y. Zariski Topology. Formalized Mathematics. 2018;26(4). To be appeared.
[2] Atiyah MF, MacDonald IG. Introduction to Commutative Algebra. Addison Wesley
Publishing Company; 1969.
[3] Bancerek G, Byliński C, Grabowski A, Kornilowicz A, Matuszewski R, Naumowicz
A, et al. Mizar: State-of-the-art and Beyond. In: Kerber M, Carette J, Kaliszyk C,
Rabe F, Sorge V, editors. Intelligent Computer Mathematics. vol. 9150 of Lecture
Notes in Computer Science. Springer International Publishing; 2015. p. 261–279.
Available from: http://dx.doi.org/10.1007/978-3-319-20615-8_17.

Mizar article information
Works in Progress
TOPZARI1 Zariski Topology
by Yasushige Watase
Summary: We formalize, in Mizar [3], basic definitions of commutative ring theory
such as Prime Spectrum, Nilradical, Jacobson Radical and Local Ring, and Sem-Local
Ring, then formalize proofs of some relating theorems along with the first chapter of [2].
We denote Spectrum A for the set of all prime ideal of a commutative ring A and introduce the so-called Zariski topology in order to make Spectrum A a topological space.
In the article the topological speace was denoted ZariskiTS. We formalize a topologicalspace defined by the topology and provide a formal proof of the fact that Spectrum A is
T0 space. Finally we formalize a continuous map assciated with a ring homomorphism
h : A −→ B. Namely h induces a continious map Spec h : ZariskiTS B −→ ZariskiTS A( Spec h is defined by (Spec h)(p) = h−1 (p) where p is a prime ideal of B.)
Listing 5. TOPZARI1 - abstract:: {Z}ariski {T}opology:: by Yasushige Watase:::: Received October 16, 2018:: Copyright (c) 2018 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 file 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 ARYTM 3, FUNCT 1, RELAT 1, WELLORD1, CARD 3, XBOOLE 0, TARSKI,XCMPLX 0, STRUCT 0, SUBSET 1, SUPINF 2, NAT 1, CARD 1, MESFUNC1, GROUP 1,
ARYTM 1, FINSEQ 1, SETFAM 1, INT 2, QUOFIELD, MSSUBFAM, BINOP 1, GROUP 4,
NUMBERS, IDEAL 1, C0SP1, ZFMISC 1, FUNCSDOM, CARD FIL, RING 1, SQUARE 1,
BCIALG 2, NEWTON, RING 2, ORDERS 1, XXREAL 0, FINSET 1, WELLORD2,

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

6/12

Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

PRE TOPC, RCOMP 1, TEX 1, ORDINAL2, TOPZARI1, ALGSTR 0, LATTICEA;
notations TARSKI, XBOOLE 0, ZFMISC 1, SUBSET 1, SETFAM 1, DOMAIN 1, RELAT 1,
ORDINAL1, WELLORD1, FUNCT 1, FUNCT 2, FINSET 1, STRUCT 0, PRE TOPC,ALGSTR 0, RLVECT 1, ORDERS 1, GROUP 1, VECTSP 1, IDEAL 1, RING 1, RING 2,
TEX 1, RELSET 1, XCMPLX 0, XXREAL 0, NUMBERS, BINOM, GROUP 6, QUOFIELD,
C0SP1, FINSEQ 1;
constructors ARYTM 3, TDLAT 3, ORDERS 1, RINGCAT1, RING 2, BINOM, RELSET 1,
GCD 1, ALGSTR 0, TEX 1;
registrations XBOOLE 0, ORDINAL1, RELSET 1, XREAL 0, NAT 1, STRUCT 0, CARD 1,
VECTSP 1, ALGSTR 1, SUBSET 1, FUNCT 2, ALGSTR 0, RLVECT 1, IDEAL 1,
RINGCAT1, RING 1, RING 2, PRE TOPC, TDLAT 3, TEX 1, SCMRINGI;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin :: Preliminaries: Some Properties of Ideals
reserve R for commutative Ring;
reserve A,B for non degenerated commutative Ring;
reserve h for Function of A,B;
reserve I0,I,I1,I2 for Ideal of A;
reserve J,J1,J2 for proper Ideal of A;
reserve p for prime Ideal of A;
reserve S,S1 for non empty Subset of A;
reserve E,E1,E2 for Subset of A;
reserve a,b,f for Element of A;
reserve n for Nat;
reserve x,o,o1 for object;definition let A,S;
func Ideals(A,S) −> Subset of Ideals A equals:: TOPZARI1:def 1{ I where I is Ideal of A: S c= I };end;registration let A,S;
cluster Ideals(A,S) −> non empty;
end;
theorem :: TOPZARI1:1
Ideals(A,S) = Ideals(A,S−Ideal);:: Some Properties of power of an element of a ring:: Definition of Nilpotency
definition
let A be unital non empty multLoopStr 0, a be Element of A;
attr a is nilpotent means:: TOPZARI1:def 2
ex k being non zero Nat st a|ˆk = 0.A;
end;
registration
let A be unital non empty multLoopStr 0;
cluster 0.A −> nilpotent;
end;registration
let A be unital non empty multLoopStr 0;
cluster nilpotent for Element of A;
end;registration let A;
cluster 1.A −> non nilpotent;
end;:: Definition of a multiplicatively closed set generated by an element:: which does not meet a proper Ideal J
definition

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

7/12

Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

let A,J,f;func multClSet(J,f) −> Subset of A equals:: TOPZARI1:def 3
the set of all f|ˆi where i is Nat;end;registration let A,J,f;cluster multClSet(J,f) −> multiplicatively−closed;
end;
theorem :: TOPZARI1:2
for n be Nat holds (1.A)|ˆn = 1.A;
theorem :: TOPZARI1:3
not 1.A in sqrt J;
theorem :: TOPZARI1:4
multClSet(J,1.A) = {1.A};
definition let A,J,f;func Ideals(A,J,f) −> Subset of Ideals A equals:: TOPZARI1:def 4{I where I is Subset of A: I is proper Ideal of A &J c= I & I /\ multClSet(J,f) = {} };end;theorem :: TOPZARI1:5
for A, J, f st not f in sqrt J holds J in Ideals(A,J,f);::[AM] Theorem 1.3
theorem :: TOPZARI1:6
for A, J, f st not f in sqrt J holds
Ideals(A,J,f) has upper Zorn property wrt RelIncl(Ideals(A,J,f) );theorem :: TOPZARI1:7
for f,J st not f in sqrt J holds
ex m be prime Ideal of A st not f in m & J c= m;::[AM] Cor 1.4
theorem :: TOPZARI1:8
ex m be maximal Ideal of A st J c= m;theorem :: TOPZARI1:9
ex m be prime Ideal of A st J c= m;::[AM] Cor 1.5
theorem :: TOPZARI1:10
a is NonUnit of A implies ex m be maximal Ideal of A st a in m;
begin :: Spectrum of Prime Ideals and Maximal Ideal
definition
let R be commutative Ring;
func Spectrum R −> Subset−Family of R equals:: TOPZARI1:def 5{I where I is Ideal of R: I is quasi−prime & I <> [#]R}
if R is non degenerated
otherwise {};end;
definition
let A;
redefine func Spectrum A −> Subset−Family of A equals:: TOPZARI1:def 6
the set of all I where I is prime Ideal of A;
end;registration
let A;

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

8/12

Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

cluster Spectrum A −> non empty;
end;definition
let R;
func m−Spectrum R −> Subset−Family of R equals:: TOPZARI1:def 7{I where I is Ideal of R: I is quasi−maximal & I <> [#]R}
if R is non degenerated
otherwise {};end;
definition
let A;
redefine func m−Spectrum A −> Subset−Family of the carrier of A equals:: TOPZARI1:def 8
the set of all I where I is maximal Ideal of A;
end;registration
let A;
cluster m−Spectrum A −> non empty;
end;
begin :: Local & Semi−Local Ring
definition
let A;
attr A is local means:: TOPZARI1:def 9
ex m be Ideal of A st m−Spectrum A = {m};end;definition
let A;
attr A is semi−local means:: TOPZARI1:def 10
m−Spectrum A is finite;end;
theorem :: TOPZARI1:11
x in I & I is proper Ideal of A implies x is NonUnit of A;
theorem :: TOPZARI1:12(for m1,m2 be object st m1 in m−Spectrum A & m2 in m−Spectrum A holds
m1 = m2)
implies A is local;::[AM] prop 1.6 i)theorem :: TOPZARI1:13(for x holds x in [#]A \ J implies x is Unit of A) implies A is local;
reserve m for maximal Ideal of A;
theorem :: TOPZARI1:14
a in [#]A \ m implies {a}−Ideal + m = [#]A;::[AM] prop 1.6 ii)
theorem :: TOPZARI1:15(for a holds a in m implies 1.A + a is Unit of A) implies A is local;
definition
let R;
let E be Subset of R;
func PrimeIdeals(R,E) −> Subset of Spectrum R equals:: TOPZARI1:def 11{p where p is Ideal of R: p is quasi−prime & p <> [#]R & E c= p}
if R is non degenerated
otherwise {};MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

9/12

Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

end;definition
let A;
let E be Subset of A;
redefine func PrimeIdeals(A,E) −> Subset of Spectrum A equals:: TOPZARI1:def 12{p where p is prime Ideal of A: E c=p };end;registration
let A,J;
cluster PrimeIdeals(A,J) −> non empty;
end;reserve p for prime Ideal of A;
reserve k for non zero Nat;theorem :: TOPZARI1:16
not a in p implies not a|ˆk in p;
begin :: Nilradical & Jacobson Radical
definition
let A;
func nilrad A −> Subset of A equals:: TOPZARI1:def 13
the set of all a where a is nilpotent Element of A;
end;
theorem :: TOPZARI1:17
nilrad A = sqrt({0.A});
registration
let A;
cluster nilrad A −> non empty;
end;registration
let A;
cluster nilrad A −> add−closed for Subset of A;
end;registration
let A;
cluster nilrad A −> left−ideal right−ideal for Subset of A;
end;::::: [AM] Prop 1.14
theorem :: TOPZARI1:18
sqrt J = meet PrimeIdeals(A,J);::::: [AM] Prop 1.8
theorem :: TOPZARI1:19
nilrad A = meet Spectrum A;:::[AM] Ex 1.13 i)
theorem :: TOPZARI1:20
I c= sqrt I;
theorem :: TOPZARI1:21
I c= J implies sqrt I c= sqrt J;
definition
let A;
func J−Rad A −> Subset of A equals:: TOPZARI1:def 14
meet m−Spectrum A;
end;

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

10/12

Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

begin :: Construction of Zariski Topology of the Prime Spectrum of A (Spec A)
theorem :: TOPZARI1:22
PrimeIdeals(A,S) c= Ideals(A,S);
theorem :: TOPZARI1:23
PrimeIdeals(A,S) = Ideals(A,S) /\ Spectrum A;:: [AM] p.12 Ex15 i)
theorem :: TOPZARI1:24
PrimeIdeals(A,S) = PrimeIdeals(A,S−Ideal);
theorem :: TOPZARI1:25
I c= p implies sqrt I c= p;theorem :: TOPZARI1:26
sqrt I c= p implies I c= p;:: [AM] p.12 Ex15 i)
theorem :: TOPZARI1:27
PrimeIdeals(A,sqrt(S−Ideal)) = PrimeIdeals(A,S−Ideal);
theorem :: TOPZARI1:28
E2 c= E1 implies PrimeIdeals(A,E1) c= PrimeIdeals(A,E2);::[AM] p.12 Ex.17 iv) not yet introduce X f = PrimeIdeals(A,{f})theorem :: TOPZARI1:29
PrimeIdeals(A,J1) = PrimeIdeals(A,J2) iﬀ sqrt J1 = sqrt J2;::[AM] Prop 1.11 ii) case of n=2
theorem :: TOPZARI1:30
I1 ∗’ I2 c= p implies I1 c= p or I2 c= p;::[AM] p.12 Ex.15 ii)
theorem :: TOPZARI1:31
PrimeIdeals(A,{1.A}) = {};::[AM] p.12 Ex.15 ii)
theorem :: TOPZARI1:32
Spectrum A = PrimeIdeals(A,{0.A});::[AM] p.12 Ex.15 iv)
theorem :: TOPZARI1:33
for E1,E2 be non empty Subset of A holds
ex E3 be non empty Subset of A st
PrimeIdeals(A,E1) \/ PrimeIdeals(A,E2) = PrimeIdeals(A,E3);::[AM] p.12 Ex.15 iii)
theorem :: TOPZARI1:34
for G being Subset−Family of Spectrum A stfor S being set st S in G holds(ex E be non empty Subset of A st S = PrimeIdeals(A,E))
holds ex F be non empty Subset of A st Intersect G = PrimeIdeals(A,F);::[AM] p.12 Ex.15
definition
let A;
func ZariskiTS(A) −> strict TopSpace means:: TOPZARI1:def 15
the carrier of it = Spectrum A &for F being Subset of it holds F is closed iﬀ(ex E be non empty Subset of A st F = PrimeIdeals(A,E));
end;
registration
let A;
cluster ZariskiTS(A) −> non empty;
end;

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

11/12

Mechanized Mathematics and Its Applications, Works in Progress

Zariski Topology (Watase Y.)

theorem :: TOPZARI1:35
for P,Q being Point of ZariskiTS A st P <> Q holds
ex V being Subset of ZariskiTS A
st V is open & ( P in V & not Q in V or Q in V & not P in V );registration
cluster degenerated for commutative Ring;
end;
registration let R be degenerated commutative Ring;cluster ADTS Spectrum R −> T 0;
end;::[AM] p.13 Ex18 iv)
registration let A;
cluster ZariskiTS A −> T 0;
end;
begin :: Continuous Map ZariskiTS B −> ZariskiTS A:: associated with a ring homomorphism.
reserve M0 for Ideal of B;
theorem :: TOPZARI1:36
h is RingHomomorphism implies h”M0 is Ideal of A;
reserve M0 for prime Ideal of B;
theorem :: TOPZARI1:37
h is RingHomomorphism implies h”M0 is prime Ideal of A;:: Spec h is continuous map of ZariskiTS B −> ZariskiTS A:: associated with a ring homomorphism h:A−>B.
::[AM] p.13 Ex22
definition ::: similar to ”f from FUNCT 3
let A, B, h;assumeh is RingHomomorphism;func Spec h −> Function of ZariskiTS B, ZariskiTS A means:: TOPZARI1:def 16
for x be Point of ZariskiTS B holds it.x = h”x;end;::[AM] p.13 Ex22 ii)
theorem :: TOPZARI1:38
h is RingHomomorphism implies(Spec h)”PrimeIdeals(A,E) = PrimeIdeals(B,h.:E);::[AM] p.13 Ex22 i)
theorem :: TOPZARI1:39
h is RingHomomorphism implies Spec h is continuous;

MMA-WiP (2019), vol.1, no.3 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.3 - ISSN 2434-5458 (Online)

12/12