Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)

Regular Paper

可換環の局所化
Localization of Commutative Rings
渡瀬 泰成 *
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 article reports current progressing work on formalizing localization of a commutative ring. It consists mainly of a construction of ring of fraction. It is the generalized
formalization of field of fraction of a integral domain [1]. Firstly it was formalized thata process of construction of a ring of fraction with respect to a multiplicative closed
set. Secondly some properties and some interpretation of a ring of fraction in Zariski
topolgical space.

1

はじめに
本稿では環の局所化の形式化について作成中のアーティクルについて報告する．FM 誌

26(4), 2018 にザリスキ位相の形式化を行ったアーティクル TOPZARI1 が掲載され，本稿はその続編となり，ちょうど参考文献 [2] の 1 章が TOPZARI1，3 章が本稿で扱うアーティクルに対応する．

2

環の局所化
環 R と R の部分集合で積閉集合 S が与えられると，分子を R の元，分母を S の元と思って分数の一般化が展開できる．R が整域の場合は，R ∖ 0 = R× は積閉集合となり分数を定義して得られる分数環が商体となる．これは QUOFIELD（文献 [1]）として先行
アーティクルとして形式化されている．

R × R× の元 [a, s], [b, t] が等しい関係を a · t − b · s = 0 とすると，これは同値関係となり，商集合上に和・積が定義される．この商集合上にできた代数的対象は体の公理を満たし商体と呼ぶ．分数の表示は同値類の元を a/s と表記していることになる．
零因子を含む環の場合の分数環の構成を形式化を行う．

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

1/11

Mechanized Mathematics and Its Applications, Works in Progress

2.1

Localization of Commutative Rings (Watase Y.)

分数を定義する関係

環 R とその積閉な部分集合を S として，それらの直積集合 R × S に以下に定義した

Frac Equal という関係を定義する．有理数が等しいときの条件の一般化である．

Listing 1. TOPZARI2 - def 1
definition
let R,S;
let x,y be Element of [:[#]R,S:];pred x,y Frac Equal R,S means:: TOPZARI2:def 1
ex x1,y1 be Element of [#]R,x2,y2,s1 be Element of S
st x = [x1,x2] & y = [y1,y2] & (x1 ∗ y2 − y1 ∗ x2) ∗ s1 = 0.R;
end;

関係 Frac Equal は同値関係となることが証明される．

2.2

直積集合上の 2 項演算

つぎに [R, S] × [R, S] に和と積の 2 項演算を定義する．

R × S の算法 R × S に加法と乗法を定義する．加法は padd と表記して以下の対応を与
える．
padd

→

[R, S]

7−→[x1 · y2 + y1 · x2, x2 · y2]∈∈[R, S] × [R, S][x1, y1] × [x2, y2]

Listing 2. TOPZARI2 - def3
definition
let R,S;
let x,y be Element of [:[#]R,S:];func padd(x,y) −> Element of [:[#]R,S:] means:: TOPZARI2:def 3
ex x1,y1 be Element of [#]R,x2,y2 be Element of S
st x = [x1,x2] & y = [y1,y2] & it = [x1∗y2 + y1∗x2, x2∗y2];end;

乗法は pmult と表記して以下の対応を与える．
pmult[R, S][x1, y1] × [x2, y2]7−→[x1 · x1, y1 · y2]

∈

−→

∈

[R, S] × [R, S]

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

2/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)

Listing 3. TOPZARI2 - def4
definition
let R,S;
let x,y be Element of [:[#]R,S:];func pmult(x,y) −> Element of [:[#]R,S:] means:: TOPZARI2:def 4
ex x1,y1 be Element of [#]R,x2,y2 be Element of S
st x = [x1,x2] & y = [y1,y2] & it = [x1∗y1, x2∗y2];
end;

2.3

R × S の同値関係による商集合 ClassEqRel(R, S) の演算

加法 padd と乗法 pmult は ClassEqRel(R, S) 上に拡張され，それぞれ代表元によらず定義されことが証明される．算法の結合則を検証に於いて TOPZARI2:def 3, TOPZARI2:def

4 の定義では，関数の入れ子で演算の定義域に不整合が生じ，以下の様にそれぞれ fr addと fr mult と再定義にて解消した．

Listing 4. TOPZARI2 - def5
definition
let R,S;func fr add(R,S) −> BinOp of [:[#]R,S:] means:: TOPZARI2:def 5
for x,y holds it.(x,y) = padd(x,y);end;

Listing 5. TOPZARI2 - def6
definition
let R,S;func fr mult(R,S) −> BinOp of [:[#]R,S:] means:: TOPZARI2:def 6
for v,w being Element of [:[#]R,S:] holds it.(v,w) = pmult(v,w);
end;

次に以下の 2 元を定義し，ClassEqRel(R, S) の演算として加法と乗法の単位元となることの証明を形式化した．

Listing 6. TOPZARI2 - def 9
definition
let R,S;func 0.(R,S) −> Element of [:[#]R,S:] equals:: TOPZARI2:def 9[0.R ,1.R ];end;definition
let R,S;func 1.(R,S) −> Element of [:[#]R,S:] equals

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

3/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.):: TOPZARI2:def 10[1.R ,1.R ];end;

以上の準備の下，ClassEqRel(R, S) に環構造が構成できこれを Fr Ring(R, S) と定義した．短い表記としては S˜R とした．この環は積閉集合 S に関する分数環という．特にp を素イデアルとすると，R ∖ p は積閉集合となる．この積閉集合で定義される分数環をRp と表記する. Rp は局所環となり，正確な言い方ではないが，R の点 p における局所化といい，本稿タイトルの所以となる．

Listing 7. TOPZARI2 - def 11
definition
let R, S;
func Fr Ring(R,S) −> strict doubleLoopStr means:: TOPZARI2:def 11
the carrier of it = Class EqRel(R,S) & 1.it = Class(EqRel(R,S),1.(R,S)) &0.it = Class(EqRel(R,S),0.(R,S)) &(for x, y being Element of it ex a, b being Element of [:[#]R,S:] stx = Class(EqRel(R,S),a) & y = Class(EqRel(R,S),b) &(the addF of it).(x,y) = Class(EqRel(R,S),a+b) ) &for x, y being Element of it ex a, b being Element of [:[#]R,S:] stx = Class(EqRel(R,S),a) & y = Class(EqRel(R,S),b) &(the multF of it).(x,y) = Class(EqRel(R,S),a∗b );end;

Fr Ring(R, S) が環の公理を満たすことをチェックして以下を得る．

Listing 8. TOPZARI2 - Th.27
theorem :: TOPZARI2:27
S˜R is Ring;

2.4

分数環の標準射

次の図式 R から S˜R への標準的な環準同形を形式化した．
canHom

Fr Ring(R, S)x

7−→[x, 1Fr Ring(R,S) ]

∈

−→

∈

R

この射は単射となり，分数環の普遍性に現れる標準的な射となる．

Listing 9. TOPZARI2 - def 12
definition
let R,S;func canHom(R,S) −> Function of R, S˜R means:: TOPZARI2:def 12
for x being Element of R holds it.x = Class(EqRel(R,S),[x,1.R]);
end;

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

4/11

Mechanized Mathematics and Its Applications, Works in Progress

2.5

Localization of Commutative Rings (Watase Y.)

作成予定の形式化すべき定理

以上の『環の局所化』の形式化の定理，定義を実装したが，既に 2,000 行のコード化となっている．あまり多くを形式化するとアーティクル自体が長いものになり重要な事項を優先して全体をまとめる予定である．以下をコード化することとなろう．

• 分数環の普遍写像性（Universal Mapping Property）．
• A ∖ p が積閉集合であること．
• Ap は局所環．
• ザリスキ空間の開集合と局所化の関連．

3

考察と展望
参考とした可換代数の教科書 [2] では積閉集合の定義では零元の条件はない．他の多くの邦書では積閉集合の定義では零元含まないという条件を科す．形式化を展開する場合は後々のため定義の条件は最小限にすべきと考える．余計な条件は将来，繰り返して場合
分けや条件チェックを証明に要求することになるからである．
局所化は，A-加群に対しても定義されるので，形式化の順番として，加群の局所化を定義して A 自身も A-加群なので特別なケースとして扱うこともできた．環上の加群はす
でに 90 年代初頭より形式化されてきた．今後は [2] の 2 章の内容の様に完全列を利用した機能的な取り扱いも形式化が必要となると考える．

参考文献[1] Schwarzweller C. The Field of Quotients Over an Integral Domain. Formalized
Mathematics. 1998;7(1):69–79. Available from: http://fm.mizar.org/1998-7/
pdf7-1/quofield.pdf.
[2] Atiyah MF, MacDonald IG. Introduction to Commutative Algebra. Addison Wesley
Publishing Company; 1969.
[3] Watase Y. Zariski Topology. Formalized Mathematics. 2018;26(4). To be appeared.

Mizar article information
Works in Progress
TOPZARI2 Localization of Commutative Rings
by Yasushige Watase
Summary: This work is a continuation of the previous formalization of Zariski Topology [3]. The aim at this work is for futher formalization of the area of commutative
algebra and algebraic geometry. The article consists mainly of a construction of ring of

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

5/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)

fraction. It is the generalized formalization of field of fraction of a integral domain [1].
Firstly it was formalized that a process of construction of a ring of fraction with respect
to a multiplicative closed set. Secondly some properties and some interpretation of aring of fraction in Zariski topolgical space.
Listing 10. TOPZARI2 - abstract
environvocabularies ARYTM 3, FUNCT 1, RELAT 1, RLVECT 1, VECTSP 1, CARD 3, ALGSTR 0,
XBOOLE 0, TARSKI, FUNCT 2, STRUCT 0, SUBSET 1, SUPINF 2, NAT 1, MESFUNC1,
GROUP 1, ARYTM 1, INT 2, QUOFIELD, MSSUBFAM, BINOP 1, LATTICES, NUMBERS,IDEAL 1, C0SP1, EQREL 1, ZFMISC 1, FUNCSDOM, WAYBEL20, CARD FIL, RING 2,
YELLOW 1, PARTFUN1, RELAT 2, MCART 1, CAT 1, TOPZARI2;
notationsTARSKI, XBOOLE 0, ZFMISC 1, BINOP 1, SUBSET 1, XTUPLE 0, SETFAM 1,
DOMAIN 1, RELAT 1, RELAT 2, ORDINAL1, MEMBERED, WELLORD2, FUNCT 1,
FUNCT 2, PARTFUN1, CARD 3, ARYTM 3, FUNCOP 1, PRALG 1,
PBOOLE, STRUCT 0, ALGSTR 0, PRE TOPC, TSEP 1, RLVECT 1,ORDERS 1,RINGCAT1,
ORDERS 2, YELLOW 1, GROUP 1, VECTSP 1, IDEAL 1, RING 1,RING 2, RELSET 1,
BINOM, GROUP 6, GCD 1, TEX 1, VECTSP 2, COMPLFLD, VECTSP10, QUOFIELD,
C0SP1, FINSEQ 1, EQREL 1, POLYNOM3;
constructors
ARYTM 3, FUNCOP 1, PRALG 1, STRUCT 0, ALGSTR 0,
PRE TOPC, TSEP 1, TDLAT 3, TEX 4, RLVECT 1,ORDERS 1, ORDERS 2, RINGCAT1,
YELLOW 1, GROUP 1, VECTSP 1, IDEAL 1, REALALG1, RING 1,RING 2, C0SP1,
BINOM, RELSET 1, GCD 1, QUOFIELD;
registrations XBOOLE 0, ORDINAL1, RELSET 1, XREAL 0, NAT 1, INT 1, MEMBERED,FINSEQ 1, STRUCT 0, VECTSP 1, ALGSTR 1, SUBSET 1, RELAT 1, FUNCT 2,
ALGSTR 0, RLVECT 1, QUOFIELD, RINGCAT1, RING 1, C0SP1, FUNCT 1, PARTFUN1,
RING 2, NAT 2, ENDALG, PBOOLE, MSSUBFAM, EQREL 1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions RELAT 1, FUNCT 2, VECTSP 1, GROUP 1, GROUP 6, IDEAL 1, INT 3,
CARD 3, RING 2, ORDERS 1, XBOOLE 0, FUNCT 1, PBOOLE, FINSET 1, TARSKI,
RING 1, PRE TOPC, TDLAT 3, T 0TOPSP, RINGCAT1, REALALG1;
equalities BINOP 1, XCMPLX 0, STRUCT 0, ALGSTR 0, FINSEQ 1,
VECTSP10, WELLORD1, SUBSET 1, XBOOLE 0, FUNCOP 1;
expansions STRUCT 0, GROUP 1, ALGSTR 0, RLVECT 1, VECTSP 1, IDEAL 1, XBOOLE 0,
FUNCT 1, QUOFIELD, GROUP 6, TARSKI, GCD 1, ORDERS 1, RING 1, REALALG1,
SUBSET 1, EQREL 1, BINOP 1, PBOOLE;
theorems ALGSTR 0, GROUP 1, VECTSP 1, RLVECT 1, IDEAL 1, SUBSET 1, FUNCT 2,TARSKI, C0SP1, ZFMISC 1, RING 2, RELAT 1, XTUPLE 0, EQREL 1, BINOP 1,
MCART 1;schemes FUNCT 2, EQREL 1, BINOP 1;
begin :: Preliminaries
reserve R,R1 for commutative Ring;
reserve A,B for non degenerated commutative Ring;registration
let R;
cluster multiplicatively−closed for non empty Subset of R;
end;
reserve S for non empty multiplicatively−closed Subset of R;
reserve T for non empty multiplicatively−closed Subset of A;
reserve x,y,z,u,v,w,p,p1,q,q1 for Element of [:[#]R,S:];
reserve s,s1 for Element of S;

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

6/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)

definition
let R,S;
let x,y be Element of [:[#]R,S:];pred x,y Frac Equal R,S means:: TOPZARI2:def 1
ex x1,y1 be Element of [#]R,x2,y2,s1 be Element of S
st x = [x1,x2] & y = [y1,y2] & (x1 ∗ y2 − y1 ∗ x2) ∗ s1 = 0.R;
end;
theorem :: TOPZARI2:1
0.R in S implies x,y Frac Equal R,S;
definition let R,S;
func EqRel(R,S) −> Equivalence Relation of [:[#]R,S:] means:: TOPZARI2:def 2[p,q] in it iﬀ p,q Frac Equal R,S;
end;
registration
let R,S;cluster EqRel(R,S) −> non empty total symmetric transitive;end;
registration
let R;
cluster [#]R −> non empty multiplicatively−closed;
end;
registration
let R,S;cluster [:[#]R,S:] −> non empty;
end;
theorem :: TOPZARI2:2
Class(EqRel(R,S),x) = Class(EqRel(R,S),y) iﬀ x,y Frac Equal R,S;
reserve x1,y1 for Element of [#]R;reserve x2,y2 for Element of S;
definition
let R,S;
let x,y be Element of [:[#]R,S:];func padd(x,y) −> Element of [:[#]R,S:] means:: TOPZARI2:def 3
ex x1,y1 be Element of [#]R,x2,y2 be Element of S
st x = [x1,x2] & y = [y1,y2] & it = [x1∗y2 + y1∗x2, x2∗y2];end;
definition
let R,S;
let x,y be Element of [:[#]R,S:];func pmult(x,y) −> Element of [:[#]R,S:] means:: TOPZARI2:def 4
ex x1,y1 be Element of [#]R,x2,y2 be Element of S
st x = [x1,x2] & y = [y1,y2] & it = [x1∗y1, x2∗y2];end;
definition
let R,S;
let x, y be Element of [:[#]R,S:];
redefine func padd(x,y);
commutativity;
end;
theorem :: TOPZARI2:3

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

7/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)

pmult(x,y) = pmult(y,x);
definition
let R,S;
let x, y be Element of [:[#]R,S:];
redefine func pmult(x,y);
commutativity;
end;
theorem :: TOPZARI2:4
pmult(padd(x,y),z), padd(pmult(x,z),pmult(y,z)) Frac Equal R,S;
theorem :: TOPZARI2:5
x,u Frac Equal R,S & y,v Frac Equal R,S implies
pmult(x,y),pmult(u,v) Frac Equal R,S;
theorem :: TOPZARI2:6
x,u Frac Equal R,S & y,v Frac Equal R,S implies
padd(x,y),padd(u,v) Frac Equal R,S;
theorem :: TOPZARI2:7
x,u Frac Equal R,S & y,v Frac Equal R,S & z,w Frac Equal R,S implies
padd(x,padd(y,z)),padd(u,padd(v,w)) Frac Equal R,S;
definition
let R,S;func fr add(R,S) −> BinOp of [:[#]R,S:] means:: TOPZARI2:def 5
for x,y holds it.(x,y) = padd(x,y);
end;
definition
let R,S;func fr mult(R,S) −> BinOp of [:[#]R,S:] means:: TOPZARI2:def 6
for v,w being Element of [:[#]R,S:] holds it.(v,w) = pmult(v,w);
end;
definition
let R,S,x,y;
func x+y −> Element of [:[#]R,S:] equals:: TOPZARI2:def 7(fr add(R,S)).(x,y);
end;
definition
let R,S,x,y;
func x∗y −> Element of [:[#]R,S:] equals:: TOPZARI2:def 8(fr mult(R,S)).(x,y);
end;
definition
let R,S;func 0.(R,S) −> Element of [:[#]R,S:] equals:: TOPZARI2:def 9[0.R ,1.R ];end;definition
let R,S;func 1.(R,S) −> Element of [:[#]R,S:] equals:: TOPZARI2:def 10[1.R ,1.R ];MMA-WiP (2019), vol.1, no.4 - http://mizar-jp.org/journal/MMA-WiP/j2019.1.4 - ISSN 2434-5458 (Online)

8/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)

end;theorem :: TOPZARI2:8
x + 0.(R,S) = x;theorem :: TOPZARI2:9
x ∗ 1.(R,S) = x;theorem :: TOPZARI2:10
x ∗ y = y ∗ x;
theorem :: TOPZARI2:11
x + y = y + x;
theorem :: TOPZARI2:12
x+(y+z) = (x+y)+z;
theorem :: TOPZARI2:13x∗(y∗z) = (x∗y)∗z;
theorem :: TOPZARI2:14
x,u Frac Equal R,S & y,v Frac Equal R,S implies
x∗y,u∗v Frac Equal R,S;
theorem :: TOPZARI2:15
x,u Frac Equal R,S & y,v Frac Equal R,S implies
x+y,u+v Frac Equal R,S;
theorem :: TOPZARI2:16(x+y)∗z, x∗z + y∗z Frac Equal R,S;
begin :: Localization of Ring by S
definition
let R, S;::$N Locarization
func Fr Ring(R,S) −> strict doubleLoopStr means:: TOPZARI2:def 11
the carrier of it = Class EqRel(R,S) & 1.it = Class(EqRel(R,S),1.(R,S)) &0.it = Class(EqRel(R,S),0.(R,S)) &(for x, y being Element of it ex a, b being Element of [:[#]R,S:] stx = Class(EqRel(R,S),a) & y = Class(EqRel(R,S),b) &(the addF of it).(x,y) = Class(EqRel(R,S),a+b) ) &for x, y being Element of it ex a, b being Element of [:[#]R,S:] stx = Class(EqRel(R,S),a) & y = Class(EqRel(R,S),b) &(the multF of it).(x,y) = Class(EqRel(R,S),a∗b );end;notation
let R ,S;
synonym S˜R for Fr Ring(R,S);
end;
reserve a, b, c for Element of [:[#]R,S:];
reserve r1, r2 for Element of [#]R;reserve s1, s2 for Element of S;
registration
let R ,S;cluster S˜R −> non empty;
end;
theorem :: TOPZARI2:17
0.R in S iﬀ S˜R is degenerated;
reserve x, y, z for Element of S˜R;
theorem :: TOPZARI2:18

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

9/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)

ex a being Element of [:[#]R,S:] st x = Class(EqRel(R,S),a);theorem :: TOPZARI2:19
Class(EqRel(R,S),a) is Element of S˜R;
theorem :: TOPZARI2:20
Class(EqRel(R,S),[r1,s1]) is Element of S˜R;
theorem :: TOPZARI2:21
Class(EqRel(R,S),a) = Class(EqRel(R,S),[a‘1,a‘2]);
theorem :: TOPZARI2:22
a‘1 = a‘2 implies Class(EqRel(R,S),a) = 1.(S˜R);
theorem :: TOPZARI2:23
x = Class(EqRel(R,S),a) & y = Class(EqRel(R,S),b) implies x+y =Class(EqRel(R,S),a+b);
theorem :: TOPZARI2:24
x = Class(EqRel(R,S),a) & y = Class(EqRel(R,S),b) implies x∗y =Class(EqRel(R,S),a∗b);
theorem :: TOPZARI2:25
Class(EqRel(R,S),a∗b) = Class(EqRel(R,S),b∗a);theorem :: TOPZARI2:26
x∗y = y∗x;
theorem :: TOPZARI2:27
S˜R is Ring;registration
let R,S;cluster S˜R −> Abelian add−associative right zeroed
right complementable associative well−unital distributive;end;
registration
let R,S;cluster S˜R −> commutative;end;
definition
let R,S;func canHom(R,S) −> Function of R, S˜R means:: TOPZARI2:def 12
for x being Element of R holds it.x = Class(EqRel(R,S),[x,1.R]);
end;
theorem :: TOPZARI2:28
canHom(R,S) is RingHomomorphism;
reserve s for Element of S;
reserve g for Function of R, R1;
definition
let R ;
func Unit Set(R) −> Subset of [#]R equals:: TOPZARI2:def 13{a where a is Element of R: a is Unit of R };end;registration
let R;
cluster Unit Set(R) −> non empty;
end;
theorem :: TOPZARI2:29

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

10/11

Mechanized Mathematics and Its Applications, Works in Progress

Localization of Commutative Rings (Watase Y.)a‘1 in S implies Class(EqRel(R,S),a) is Unit of S˜R;

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

11/11