Mechanized Mathematics and Its Applications, Works in Progress

Identiﬁcation of Rings (Y.Watase)letter

埋め込みの原理 (環の場合)
On Identiﬁcation of Rings
渡瀬 泰成 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 10, 2022. Revised: May 14, 2023. Accepted: June 13, 2023.

要約
We formalized a standard procedure of ring identiﬁcation appeared as a lemma in§13 of chapter 1 of [2], namely:
LEMMA. If R and S ′ are rings and if T0 is a given isomorphism of R onto a subring
R′ of S ′ , then there exists a ring S which contains R as a subring and which is suchthat T0 can be extended to an isomorphism T of R onto S ′ .
We discussed the relation between the above lemma and polynomial rings in termsof formalization as well, and concluded that polynomial rings would be regarded as apart of a formal series.

1

序論
本稿では環といえば単位元をもつ可換環とする. 与えられた 2 つの環 R と S ′ について, 次の 2 条件 1), 2) をみたすとき R が S ′ の中に埋め込まれると定義する.

1) S ′ と同型な環 S が存在.
2) S は R を部分環として含む.
この定義からは次の命題 1 が S ′ から S への同型写像 T を考え R の T −1 による像をとれば示される.
命題 1. 「R が S ′ の中に埋め込まれる」ならば「S ′ は R と同型な部分環をもつ」

MMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

1/8

Mechanized Mathematics and Its Applications, Works in Progress

Identiﬁcation of Rings (Y.Watase)

この「S ′ は R と同型な部分環をもつ」が十分条件となる次の命題も示される．
命題 2. 「S ′ が R と同型な部分環をもつ」ならば「R が S ′ の中に埋め込まれる」
命題 2 の証明の形式化が本稿の中心的な内容であり所謂「埋め込み原理」といわれ命題 2 を精密にした以下の補題が文献 [2]1 章 §13 の内容であり上述要旨の Lemma である.

LEMMA. R が S ′ が環で T0 が R から S ′ の部分環 R′ への環同型写像ならば, 環 S が存
在し S は R を部分環に持ち, T0 を延長して S から S ′ への同型写像となるように S がとれる.
有理数体の代数拡大を考える場合有理数体が埋め込まれているほうが計算がしやすい.
これは拡大体の四則演算で有理数も拡大体の元として扱え計算が実行できるからだ. 単射が存在しているだけでは単射の像として有理数を扱う煩雑さが伴い演算の記述や計算に複雑さが増す. 単射像でなく埋め込まれている状況で計算できる方が実用的である. 上記の Lemma では標準的に与えられた環 R が埋め込まれているように拡大環を構成し、且S ′ と同型となる手順を与えている. MML ライブラリには体の拡大においての埋め込みを論じたアーティクル [1] が存在し有理数体 Q が多項式環 Q[X] に埋め込まれていることを論じている. 形式的には多項式環では係数環は埋め込まれているのであって部分環ではない. 非形式的には部分環とみなしている. 多項式環についての更なる議論は 3 章に譲る.

埋め込み原理の形式化

2

文献 [2]1 章 §1 の Lemma の記号 R,S ′ ,S を環 A,B,C と読み替え A から B へ単射があるとき B と同型で A を埋め込みとしてもつ C の構成は以下の Step1,2 のプロセスを踏まfえ遂行される. 単射 A ↣ B があたえられ B ∩ C = ∅ ∧ B ∼= C で A が埋め込まれるように C を構成する議論を進める．

Step(I) X ∼= (B\f (A)) ∧ X ∩ B = ∅ なる集合 X を作る．
Step(II) C として X ∪ A に環の構造を導入し B と同型な環 C で B ∩ C = ∅ と出来る.
(f (A) の部分を A で置き換える.)
上記 Step（I）は [3] の 6 章の補題 6.1 に対応し,Step（II）は補題 6.2 に対応するが詳細は次節にて述べる.

2.1

埋め込みの原理の形式化

この節では文献 [3] の 6 章の補題, 定理に従って埋め込みの定理の形式化の内容を要約する.
定理 (補題 6.1. [3] より再掲). 空でない二つの集合 A, B を与えれば，B ∩ C = ∅ である
ような空でない集合 C と全単射 ϕ : A → C の組 (C, ϕ) が少なくとも一つ存在する.
補題 6.1. に対応する形式化は Listing 1 となる.

MMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

2/8

Mechanized Mathematics and Its Applications, Works in Progress

Identiﬁcation of Rings (Y.Watase)

Listing 1. ALGEMBED:2 - Th.2
1
2
3

theorem :: ALGEMBED:2
for a,b be non empty set holds ex c be non empty set st (a /\ c ={})&(ex f be Function st f is one−to−one & dom f = b & rng f = c );定理 (補題 6.2. [3] より再掲). R は環とする. X は空でない集合で，全単射 f : R → Xが与えられていると仮定せよ. X 上に和と積を

a + b = f (f −1 (a) + f −1 (b)), ab = f (f −1 (a)f −1 (b))
で定めると, 集合 X はこの和と積によって環となる.
補題 6.2. における集合 X の和と積の定義を形式化したものがそれぞれ Listing 1 とListing 2 である．
Listing 2. ALGEMBED:def 1 - Def.1
12
3
4
5
6
7
8
910deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
let a,b be Element of X;
assume thatf is bijective;
func addemb(f,a,b) −> Element of X equals:: ALGEMBED:def 1f.((the addF of A).(f”.a,f”.b));
end;

123
4
5678910

deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
let a,b be Element of X;
assume thatf is bijective;
func multemb(f,a,b) −> Element of X equals:: ALGEMBED:def 3f.((the multF of A).(f”.a,f”.b));
end;

Listing 3. ALGEMBED:def 3 - Def.3

補題 6.2 の結論である X が環を為す部分は上記で定義した加法 addemb(f ,a,b) と乗法multemb(f ,a,b) 及び補題の仮定の写像 f を用いて集合 X を基礎集合にもつ環 emb Ring(f )を定義した. この形式化が以下の Listing 4 となる.

Listing 4. ALGEMBED:def 5 - Def.5
123456789deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
assume thatf is bijective;
func emb Ring(f) −> strict non empty doubleLoopStr equals:: ALGEMBED:def 5
doubleLoopStr(# X, addemb f, multemb f, f.1.A, f.0.A #);end;

MMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

3/8Mechanized Mathematics and Its Applications, Works in Progress

Identiﬁcation of Rings (Y.Watase)

定理 (定理 6.4 (埋め込みの原理) [3] より再掲). 写像 f : A → B は環の準同型写像であって，単射と仮定する. このとき，次の条件 1), 2) を満たすような環 C と環の同型写像の組(C, g) が少なくとも一つ存在する.
1) A は環 C の部分環である.
2) 写像 i : A ,→ C によって自然な埋め込み i(a) = a を表すと，等式 i = gf が成り立つ.
以下の定理の内容の理解のため可換図式1 を示す：

/C?

gB_f⟳

ι

A
確かに C が A の拡大系になっていることが 2 番目の条件から i が恒等写像であることから理解される. この定理は文献 [2]Chapter 1.13: Idetiﬁcation of Rings と同一内容となる. 定理 6.4 の形式化は以下の通りである．

Listing 5. ALGEMBED:7 - Th.5
12345678

theorem :: ALGEMBED:7for A being Ring, B be A−homomorphic Ring,f being Homomorphism of A,B st f is monomorphism & ([#]B \ rng f) <> {}holds
ex C be A−homomorphic Ring,i be (Homomorphism of A,C),
G be Function of B,C st i is RingMonomorphism &G is RingIsomorphism & i = G∗f & i = id A & Image i is Subring of C &[#](Image i) = [#]A;

Proof (定理 6.4). B = f (A) であれば C = A としてよいので B 6= f (A) の場合を示す.
ϕ : B \ f (A) → X, X ∩ A = ∅ となる (X, ϕ) は補題 6.1 により構成する.
C = X ∪ A と定め, g : B → C を以下の様に定義する.
{a if b ∈ f (A)∀b ∈ B, g(b) =ϕ(a) if b ∈/ f (A).
g は全単射であることが確認でき補題 6.2 を適用し C に環構造が入る.
∀a ∈ A, g(f (a)) = a = ι(a) よって A は C の部分環であることがルーチン的な計算により検証できるので細部は ALGEMBED:7 の証明本体を参照.

3

考察
代数構造の拡大系について「埋め込みの原理」を環を題材に形式化が完了した. 「埋め込みの原理」はどの数学的な構造にも本来適用されるべき原理だが構造をパラメータにはとれないので個別に同様の議論をしなければならないことも分かる. 環で成り立つことはそのまま体でも成り立つので今回の形式化は汎用性があることも言える.

1 図式から同型を除き (C, g) がー意に取れれば普遍写像と考えてもよいが, domf = A となる単射が決まれば (C, g) が決まることは了解されても圏論での解釈は今後の課題である.

MMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

4/8

Mechanized Mathematics and Its Applications, Works in Progress

3.1

Identiﬁcation of Rings (Y.Watase)多項式の特徴づけについて

多項式環の特徴付けには「埋め込みの原理」と「多項式の不定元の線型結合表示」が入用であるがこれらは未だにライブラリにはない.
定理 (定理 1.33. [4] より再掲). 環 Ａ を与えれば, 次の 3 条件 1) − 3) を満たす組 (S, X)が存在する.

1). S は環, A は S の部分環である.
2). X ∈ S であって, X は A 上超越的である.
3). 環 S の元 f はすべて, 環 A の元の族 ai0≤i≤n を選んで,f=n∑ai X ii=0という形に表すことができる.
以上が定理 1.33 であって定理に現れる S が A 上 X を不定元に持つ多項式環と呼びA[X] と表す.
非形式の不定元のべきの線型結合表示で多項式を扱うことが多く現状の形式表現は使いづらい面があるので形式表現の環と同型な係数環が埋め込こまれた環を具体的に形式化できないか考察する. 即ち「埋め込みの原理」を Mizar での 1 変数多項式に適用してみる.

A 係数の 1 変数多項式環の形式化では A 値の無限列の為す環の部分環として構成した.
これを T としよう. ϕ : A → T (a 7→ (a, 0, 0, · · · )) とすれば ϕ は単射である. また T の不定元は t = (0, 1, 0, · · · ) である. 以上の状況で「埋め込みの原理」を適用すると以下の可換図式を得る.

/S?

ξT_φ

⟳

ι

A
「埋め込みの原理」により (S, ξ) が構成される (ξ は同型射). ξ(t) = X と置くと T での多項式の準同形像は定理 1.33. 3) と準同型の線型性により X j の A− 線型結合となって S(= A[X]) で非形式での議論が出来るようになる. Mizar で形式化された多項式環

Polynom-Ring A は S(= A[X]) と同一視しているのである. t = (0, 1, 0, · · · ) を T の不定元として成り立つことは同型射 ξ で送った先でも成り立っていることを示している. 先に述べた補題 6.1 のなかで現れる集合 X は存在しか示して居らず具体的に構成する術がないので上記の t = (0, 1, 0, · · · ) を不定元として形式化を継続するほかないと判断する. 無論 S や ξ を具体的に構成する方法を追求する途も残る. 当面前者を採用して不定元 t による係数環との線型結合表示を使い易い形に形式化することが優先課題と考える.

3.2

形式化での記号の注意点

前節で多項式環と係数環の関係をみた. 係数環 A と A[X] の交わりは定理 1.33 の記号で考えると A[X] ∩ A 6= ∅ であり, Polynom-Ring A = A[X] という意味で使用するとMMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

5/8

Mechanized Mathematics and Its Applications, Works in Progress

Identiﬁcation of Rings (Y.Watase)

A[X] ∩ A = ∅ となる. A[X] の記号の使い方を明確に定義していないと正反対の結果を招く. 非形式な論文を書く場合, 非形式な表現で利用されている記号を形式化で定義された対象に用いると同一視の介在をわすれてしまうリスクがあることが理解される.

3.3多項式環の係数環の埋め込みの問題「互いに同型な２つの対象で一方の対象で成り立つ事が他方でもこの同型射 Φ により翻訳され成り立つ.] という命題を考え P としよう. すると多項式環の係数環の「埋め込み」の議論で見た様に Polynom-Ring A と A[X] は同型である (Polynom-Ring A = ΦA[X]).
他方 Polynom-Ring A ∩ A = ∅ と A[X] ∩ A 6= ∅ とが成り立ち命題 P は成り立っていない様に見え大いに疑問に思う. この議論は係数環とは何か, 記号の定義, 多項環の構成法も含め正確さ欠いているが丹念に調べ形式化していけば議論の不備や多項式環の形式化の改良点が浮き彫りにされこの分野の形式化に寄与出来ると期待している.

参考文献[1] Schwarzweller C. On Monomorphisms and Subﬁelds. Formalized Mathematics.
2019;27(2):133–137.
[2] Zariski O. and Samuel P. Commutative Algebra I, Springer, 1975
[3] 後藤四郎. 2007 年度 明治大学代数学 3 講義用テキスト. http://www.commalg.jp/~goto/pdf/daisuu3.pdf[4] 後藤四郎, 渡辺敬一. 可換環論. 日本評論社, 2011
[5] 島内剛一. 数学の基礎. 日本評論社, 1971Mizar article information
Mizar Mathematical Library (MML)
Works in Progress
ALGEMBED

Embeding Principal（Idetiﬁcation of Rings)

by Y.Watase
In the article standard embeding a ring into its over-ring is formalized in Mizar
along with the text book of Zariski & Samuel Commutative Algebra I.

Listing 6. ALGEMBED - abstract
environvocabularies NUMBERS, SUBSET 1, RELAT 1, XBOOLE 0, BINOP 1, FUNCT 1, TARSKI,
ARYTM 3, ZFMISC 1, ARYTM 1, FUNCT 2, GROUP 1, ALGSTR 0, RLVECT 1, VECTSP 1,LATTICES, SUPINF 2, MESFUNC1, QUOFIELD, MSSUBFAM, FUNCSDOM, RING 2, GROUP 6,
FDIFF 1, MOD 4, C0SP1, FIELD 2, STRUCT 0, PEVAL 1;
notations TARSKI, XBOOLE 0, ZFMISC 1, SUBSET 1, RELAT 1, FUNCT 1, RELSET 1,PARTFUN1, FUNCT 2, BINOP 1, STRUCT 0, ALGSTR 0, RLVECT 1, GROUP 1, VECTSP 1,GROUP 6, RINGCAT1, MOD 4, QUOFIELD, RING 1, C0SP1, RING 2;

MMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

6/8Mechanized Mathematics and Its Applications, Works in Progress

Identiﬁcation of Rings (Y.Watase)constructors RELSET 1, REALSET1, ORDERS 1, RINGCAT1, MOD 4, C0SP1, RING 1,RING 2;
registrations XBOOLE 0, RELAT 1, FUNCT 1, RELSET 1, FUNCT 2, STRUCT 0,VECTSP 1, SUBSET 1, RINGCAT1, MOD 4, RING 2;
requirements SUBSET, BOOLE;
equalities STRUCT 0, ALGSTR 0;
expansions VECTSP 1, FUNCT 1;
theorems TARSKI, ZFMISC 1, RLVECT 1, FUNCT 1, FUNCT 2, RELAT 1, CARD 1,GROUP 1, XBOOLE 0, XBOOLE 1, WELLORD2, SUBSET 1, XTUPLE 0, VECTSP 1, RING 2,BINOP 1, ALGSTR 0, MOD 4, RINGCAT1, GROUP 6, QUOFIELD;
schemes FUNCT 2, BINOP 1;
begin
theorem :: ALGEMBED:1
for a be non empty set holds
ex b be object st (for x be set holds not [x,b] in a);theorem :: ALGEMBED:2
for a,b be non empty set holds ex c be non empty set st (a /\ c ={})&(ex f be Function st f is one−to−one & dom f = b & rng f = c );theorem :: ALGEMBED:3
for A be Ring, X be non empty set, f be Function of A,X,a,b be Element of X st f is bijective holdsf.((the addF of A).(f”.a,f”.b)) is Element of X;
deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
let a,b be Element of X;
assume thatf is bijective;
func addemb(f,a,b) −> Element of X equals:: ALGEMBED:def 1f.((the addF of A).(f”.a,f”.b));end;
theorem :: ALGEMBED:4
for A be Ring, X be non empty set, f be Function of A,X,a,b,c be Element of X st f is bijective holds
addemb(f,a,addemb(f,b,c)) = addemb(f,addemb(f,a,b),c);deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
assume thatf is bijective;
func addemb f −> BinOp of X means:: ALGEMBED:def 2
for a,b being Element of X holds it.(a,b) = addemb(f,a,b);
end;
theorem :: ALGEMBED:5
for A be Ring, X be non empty set, f be Function of A,X,a,b be Element of X st f is bijective holdsf.((the multF of A).(f”.a,f”.b)) is Element of X;
deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
let a,b be Element of X;
assume that

MMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

7/8

Mechanized Mathematics and Its Applications, Works in Progress

Identiﬁcation of Rings (Y.Watase)f is bijective;
func multemb(f,a,b) −> Element of X equals:: ALGEMBED:def 3f.((the multF of A).(f”.a,f”.b));end;
deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
assume thatf is bijective;
func multemb f −> BinOp of X means:: ALGEMBED:def 4
for a,b being Element of X holds it.(a,b) = multemb(f,a,b);
end;
deﬁnition
let A be Ring, X be non empty set;let f be Function of A,X;
assume thatf is bijective;
func emb Ring(f) −> strict non empty doubleLoopStr equals:: ALGEMBED:def 5
doubleLoopStr(# X, addemb f, multemb f, f.1.A, f.0.A #);end;theorem :: ALGEMBED:6
for A be Ring, X be non empty set, f be Function of A,Xst f is bijective holds emb Ring(f) is Ring;::Z−S:ComAlg.Isection 13: Idetiﬁcation of Rings (Imbeding Theorem)
theorem :: ALGEMBED:7
for A being Ring, B be A−homomorphic Ring,f being Homomorphism of A,B st f is monomorphism & ([#]B \ rng f) <> {}holds
ex C be A−homomorphic Ring,i be (Homomorphism of A,C),
G be Function of B,C st i is RingMonomorphism &G is RingIsomorphism & i = G∗f & i = id A & Image i is Subring of C &[#](Image i) = [#]A;

MMA-WiP (2023), vol.5, no.3 - https://mizar-jp.org/journal/MMA-WiP/j2023.5.3 - ISSN 2434-5458 (Online)

8/8