Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

Regular Paper

イデアルの準素分解
On Primary Decomposition
渡瀬 泰成 1,*
Yasushige Watase1,*
1 東京都杉並区松ノ木 3-21-6* yasushige.watase@gmail.com
Proof checked by Mizar Version: 8.1.14 and MML Version: 5.76.1452
Received: December 15, 2023. Accepted: March 15, 2024.

要約
We formalized the so-called Primary Decomposition of Ideal appeared in the chapter 4 of [1]. we call an ideal a of a commutative ring with the unit element, has a
primary decomposition when such a ﬁnite set of primary ideals {qi } that a = ∩{qi }pTnholds. A decomposition is called minimal when qi are all distinct and qi ⊉ j6=i qj
hold. This paper describes process of developing formal proofs for existence of a primary
decomposition and its minimality.

1

序論
イデアルの分解とは数の素因数分解や整数環のイデアル分解 ((6) = (2) ∩ (3)) と類似の概念である. イデアル a の分解は a とは異なるイデアル b, c の共通部分に等しい (a = b ∩ c)
ときに a は b と c に分解されると考える. 整数環では素イデアルが極大イデアルであり,極大イデアルは準素イデアルとなることが知られているので素因数分解は準素分解の例となる．一般の可換環の場合，有限個の準素イデアル {qi } の共通部分によりイデアルの分解されていることを準素分解という．準素分解があれば分解の成分である {qi } 元の数を最小化した最短表現（言い換えれば 1 つでも分解の成分が欠けると分解を成さない.）が存在する．準素分解で重要な内容は, 与えられた準素分解から最短表現を構成する手順が存在すること, 及び最短表現の一意性と言われる準素分解成分の根基をとり出現する素イ
デアル（素因子）達は準素分解によらないという性質である. これらの内容の形式化が本稿の目的となる. 形式化は一般の可換環でのイデアルの準素分解を文献 [1] を参考にして実施した.

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

1/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition準備2

以下本稿では可換環といえば単位元を持つ非自明な環を指し A で表す. イデアルはドイツ文字 (a, b, c, p, q...) を用い I（A）は環 A のすべてのイデアルからなる集合を表す. P
は冪集合をとる場合用いる. イデアルの有限集合 {qi | i ∈ I, I(有限添数集合)} を {qi } と略記する.

半順序集合に関する準備

2.1

I にはイデアルが包含関係に関し反射的かつ推移的かつ反対称的を満たすので半順序の構造が入り (I, <) = (#I, RelIncl(I)#) と Mizar にて形式化される. この事実によって(I, <) に極大イデアルが存在することが Zorn の補題を用いて証明される. イデアルの束
はイデアル論の証明で重要な役割をはたしている. 以下では本論で有用となる一般の半順序集合 (X, R) で成り立つ性質を述べる. (ここで X は集合で R は X 上の関係である.)
性質 2.1. (既に Mizar で形式化されている事項はそのアーティクルと定理の番号を附した. 今回形式化した定理や定義はアーティクル名として IDEAL3 として引用した.)(i) Poset(X, R) の有限集合は極小元を持つ. （cf. BAGORDER:7）.
(ii) 極小元の表現は述語, 「半順序集合 X の部分集合 M における極小元 x0」は次のよ
うに形式化される：x0 is minimal wrt M, RelIncl(X). (cf. WAYBEL 4 : def 25).

(iii) Poset の有限部分集合 M 中の極小元のなす集合は minimals(M) として形式化される．(cf. DILWORTH:def 9).

(iv) Poset X の部分集合 S の任意の元よりも大なる X の元全体を UpperCone S と表記する.

(v) I(A) の部分集合 S に対して (S, ⊂ ) は半順序集合となる.
Poset X の部分集合を S として minimals(S) と UpperCone(S) を利用して以下の定理が成り立つ.
定理 2.1 (補題 6.1). Upper を以下の様に定義する. ( cf. IDEAL 3:def 9)minimals(S) −→7−→ UpperCone{x} ∪ {x}

x
この時

P(S)
∈

∈

Upper :[

Upper(S) = Sが成り立つ. (cf. IDEAL 3:30)

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

2/19

Mechanized Mathematics and Its Applications, Works in Progress

2.2

Primary Decomposition

イデアルに関する定義や性質

性質 2.2. ここではイデアルの既約, 準素イデアルの定義と性質を述べる.
以下 a, b, q, m は任意の A のイデアルとする.

(i) a が既約であるとは
a = b ∩ c となる a を含むイデアル b, c が存在しない．
(ii) q が準素イデアルとは
xy ∈ q =⇒ x ∈ q ∨ ∃n ∈ N st y n ∈ q (cf. IDEAL 2 : def 4).
(iii) a の b の商 (a : b) は以下の集合で定まるイデアルである．Mizar では (a % b) と表記する．

(a : b) = {x ∈ A | xb ⊆ a} (cf. IDEAL 1 : def 23).
(iv) a の根基

p

a は以下の集合で定まるイデアルである．

√

a = {x ∈ A : xk ∈ a for some k ∈ N} (cf. IDEAL 1 : def 24).

(v) q が準素イデアルのとき

ppq は素イデアルとなり, p = q なるとき q を p-準素, ま

たは p-primary という． (cf. IDEAL 2 : def 6).

(vi)pa = ∩{p0 | p0 ∈ SpecA, a ⊂ p0 } が成り立つので (cf. TOPZARI1:18), q が p-準素
ならば p は q を含む最小の素イデアルである.

(vii)

p
a が極大イデアルならば a は準素イデアル． (cf. IDEAL 2 : 23).

(viii) m を極大イデアル, n を正の整数とする. mn は準素イデアル． (cf. IDEAL 2 : 35).
(ix) 有限個の準素イデアルの共通部分はまた準素イデアルとなる. (cf. IDEAL 2 : def 6).
定義 2.1. イデアル b を固定して写像 (%b) : I（A）→ I（A）を以下の様に定義する.

∈

Ideal(A) −→ Ideal(A)∈(%b) :

7−→b(a : b)

この写像は P(I（A）) から P(I（A）) への写像 {ai } −→ {(ai : b)} を誘導する.
定義 2.2. 写像 sqrt(A) を以下の様に定義する.

Ideal(A) −→ Ideal(A)a∈∈sqrt(A) :

7−→

p

a

√
この写像は P(I（A）) から P(I（A）) への写像 {ai } −→ { ai } を誘導する.

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

3/19

Mechanized Mathematics and Its Applications, Works in Progress

3

準素分解

3.1

準素分解の形式化状況

Primary Decomposition

Mizar 以外の定理証明系 (PVS), Mizar, Isabelle HOL, LEAN でのイデアルの分解に関する形式化の状況を簡単に言及する. 一分解整域 UFD の既約元による分解はいずれのPVS で形式化されている. イデアルの分解は LEAN におけるデデキント整域でのイデア
ル分解を モノイドの一意分解の特殊な場合として形式化している [2]. 本稿で扱っている
準素分解は整域を仮定していない可換環での議論であり Mizar 以外の定理証明系での形式化はない. 代数多様体の既約成分もイデアルの分解と同様の内容であり代数幾何の分野
での既存形式化を Isabelle HOL で調べたがスキーム論の形式化に重きを置き具体的な準素分解には言及はない [3]. Mizar ではアフィン代数的集合を扱った [4] に代数的集合の既約成分が素イデアルとなることの形式化がある. 高階論理に基礎を置く Isabelle HOL でのスキーム論の構成では位相空間の圏から環の圏への関手である層の形式化を主に扱いス
キーム論以前の代数曲線や曲面のような多項式環を対象とした形式化は無いのが現状で
ある.

3.2

準素分解の概要

イデアル a が有限個の準素イデアル {qi } の共通部分に等しくなるときイデアルは準素イデアルにより分解されるという．{qi } の根基を取って現れる素イデアル {qi } を通常 aの素因子と呼ぶ．本編では特に a の分解に現れる {qi } を準素因子と呼ぶこととする. 任
意のイデアルが準素分解を持つとは限らない事が知られており準素分解を持つイデアルを準素分解可能という. これらを定義としてまとめる．
定義 3.1. イデアル a が準素分解可能とは準素イデアルからなる有限集合 {qi } が存在しa = ∩{qi } が成り立つことをいう.
準素分解はイデアル a の根基の素因子分解を与えている．この説明には次の定理が必要である．
定理 3.1. 任意のイデアルの有限列 Fi に対して,
pp∩{qi } = ∩ qiが成り立つ.
定理を準素分解可能なイデアル a に適応すると
ppa = ∩ qiが成り立ち準素イデアルの根基が素イデアルとなりpa = ∩pipqi = pi と置くととなる．pi を素因子と呼ぶ. a の根基が pi により素因子分解されたことが分かる. しかしながら素因子の pi には重複があり得るので重複を持たない様に所与の {qi } を変形して重複ない準素イデアルの集合 {q̃k } を構成する. 重複ばかりでなく更に {q̃k } には以下に定義する最短であることを課す.

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

4/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

定義 3.2. 準素分解可能イデアル a の準素分解 qi が最短であるとは,(cf. IDEAL 3:def

17)
(i)

√

√

qi 6=

(ii) qi ⊉qj (i 6= j) これを radical-distinct と呼ぶ.

Tn

j6=i qjを満たすときを云う. これは最短な分解は１つでも準素因子が欠けると共通部分が a と成らないことを意味している.
以上の準素イデアルの分解をつぎの３つの段階に分けて形式化を行う．

1) 素因子の集合を構成
2) 最短条件 i) の実現．
3) 最短条件 ii) の実現．
素因子の重複ない表現の形式化と最短条件を達成するのかが当面の課題となる. 解決の手
順の概略は文献 [1] の 51 頁の最後の段落から 52 頁の最初の段落に示されているのでこれに従うが手順を具体化するには幾らかの関数の準備が必要となる. 即ち第 1 段階の重複のない素因子の表現は準素因子の写像 sqrt(A) による像として重複を取り除く. 最短条件 i)の実現のためには素因子毎に根基を取ってその因子となる準素因子をグループ化しグルー
プ毎に準素因子の共通部分をとり新たな準素因子を構成する. 最短条件 ii) の実現に新たな構成した準素因子を組み合わせ的に余分な因子を除く手順を関数化して形式化する．

3.3

準素分解の形式化

3.3.1

素因子の重複の除去

準素分解可能なイデアル a で {qi } が準素因子のとき,
定義 3.3.

√qi = pi と置き関数 sqrt(A) による集合 {qi } の像は相異なる素イデアルからなる集合となりこれを prime divset(qi ) と表記する.
従って prime divset(qi ) = {p1 , p2 , . . . , pk } が素因子となり形式化は以下の通りである．

Listing 1. IDEAL 3:def 4 - Def.4
1
2
3
4
5
6
7

deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func prime divset(q) −> non empty ﬁnite Subset of Spectrum A equals::IDEAL 3:def 4(sqrt(A)).:q;
end;

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

5/19

Mechanized Mathematics and Its Applications, Works in Progress

3.3.2

Primary Decomposition

最短条件 i) の実現．

イデアル a の準素因子を {qi } とする. {qi } の元の根基をとって等しくなるものを集めてグループ分けを以下で定義する写像 PFactors よって行う. 別々のグループから元を取っ√√て q1 , q2 とすると q1 6= q2 となっている.
定義 3.4. 準素分解可能イデアル a = ∩qi のとき, 単射 PFactors を定義する.

PRIMARY(A)∈prime divset(qi ) −→∈PFactors(qi ) :−1

7−→ (sqrt(A))

pp ∩ {qi }集合で書き下せば以下の様に成っており実質 {qi } を素因子 p の順に並び替えたもに成っている.

{qi } = { q11 · · · q1r , q21 · · · q2s , · · · , qk1 · · · qkt }| {z }| {z }| {z }
p1 −primary=PFactors(p1 )p2 −primary=PFactors(p2 )pk −primary=PFactors(pk )PFactors の形式化は以下の通りである.
Listing 2. IDEAL 3:def 5 - Def.5
1
2
3
4
5
6
7

let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func PFactors(q) −> Function of prime divset(q), bool PRIMARY(A) means:: IDEAL 3:def 5
for x be Element of prime divset(q) holds ex p1 be prime Ideal of A st
x = p1 & it.x = (sqrt(A))”{p1} /\ q;end;

次に性質 2.2. vii) を利用すると PFactors で分けられた pj -primary グループの共通部
分を取ると ∩{qi1 · · · qij } は再び pj -primary イデアルとなる．これを q̃j と表す. 各グルー
プの共通部分をとると新たに準素イデアルの集合 {q̃j } が出来上がる. これがもとの a のpp
準素分解になることも証明され k 6= j ならば q̃j 6= q̃k が成り立ち最短条件 i) が実現
する. 素因子から対応するグループの共通部分を取る写像 Red を以下の様に定義する.
定義 3.5. 更に単射 PFactors を利用して単射 Red 定義する.

p

PRIMARY(A)∈prime divset(qi ) −→∈Red(qi ) :7−→ ∩(PFactors)(p)Listing 3. IDEAL 3:def 6 - Def 6
1
2
3
4
5
6
7

deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func Red(q) −> Function of prime divset(q), PRIMARY(A) means:: IDEAL 3:def 6
for x be Element of prime divset(q) holds it.x = meet((PFactors(q)).x);
end;

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

6/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

準素因子 {qi } の写像 Red による像は以下の様になる.

=

q˜1

=

=

Red{qi } = { ∩{q11 · · · q1j }, ∩{q21 · · · q2s }, · · · , ∩{qk1 · · · qkt }}
{z
}
|
{z
}
|
{z
} |
q˜2

q˜k

片々根基を取ると q = ∩{q̃j } となり {q̃j } が準素分解となり，且また最短条件 i) を実現している. このことを定理として以下の様に形式化した.
定理 3.2.

∩{qi } = ∩Redpk ∈prime divset(q) (pk )が成り立つ.

Listing 4. IDEAL 3:27 - Th.27
1
2
3

theorem :: IDEAL 3:27
for q be non empty ﬁnite Subset of PRIMARY(A) holds
meet q = meet rng Red(q);{q̃j } の作り方から最短条件 i) を満たしている. ここで更に集合 {q̃j } の極小元から成る集合を定義すると, これもまた準素分解を与え最短条件 i) を満たすので出来るだけ取り回しの良い簡約した準素分解を構成することが出来る.
定義 3.6. {qi } を準素イデアルの集合として写像 Red の像 {q̃j } を包含関係による半順序集合となり {q̃j } の極小元から成る集合を minimalRed(qi ) と定義する.

Listing 5. IDEAL 3:def 18 - Def.18
1
2
3
4
5
6
7

deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func minimalRed(q) −> non empty ﬁnite Subset of Ideals(A) equals:: IDEAL 3:def 18
minimals(RelStr(# rng Red(q),RelIncl(rng Red(q)) #));
end;

minimalRed(qi ) を用いると以下の定理が成り立つ.
定理 3.3. 任意の準素イデアルの有限集合 {qi } に対して,∩{qi } = ∩minimalRed(qi )が成り立ち minimalRed(qi ) が準素分解を与えている事を示している.
定理 3.4. 任意の準素イデアルの有限集合 {qi } に対して,

minimalRed(qi ) は radicaldistinct.
が成り立つ.
定理の形式化例：

Listing 6. IDEAL 3:43 - Th.43
1
2
3

theorem :: IDEAL 3:43
for q be non empty ﬁnite Subset of PRIMARY(A)holds minimalRed(q) is radical−distinct;

定理 3.3, 3.4 により 最短条件 i) を満たす準素分解 minimalRed(qi ) が構成された．

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

7/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

最短条件 ii) の実現．

3.3.3

前節で a = ∩{q̃j } が成り立つこと最短条件 i) を満たすことをみたので， a 6= ∩i6=j {q̃j }の証明が残った. 極小元の共通部分を扱うので極小性から他の理論例えば束論を援用しての証明を模索したが解決出来なかった. 最短条件 ii) の実現のため以下の手順を遂行すればよい.
手順 1. Set N = ♯{q̃j }, i = 1;

while i ≤ N ;if a = ∩i6=j {q̃j } then Swap q̃j to A ∧ i + +else i + +;end;
この手順は有限のイデアルの集合として以下の２つの関数により実現する．

Listing 7. IDEAL 3:def 26 - Def.26
1
2
3
4
5
6
7
8

deﬁnition
let A;
let n be Nat;let S be Element of (Ideals A)∗ ;func Trimming(S,n) −> Function of (Ideals A)∗ , (Ideals A)∗ means:: IDEAL 3:def 26
for x be Element of (Ideals A)∗ holds it.x = Trimming(x);end;

有限集合を計算しやすいように入力を有限列にして手順１．を帰納的に以下の関数で定義
する．

Listing 8. IDEAL 3:def 25 - Def.25
1
2
3
4
5
6
7
8

deﬁnition
let A;
let S be Element of (Ideals A)∗ ;func Trimming(S) −> Element of (Ideals A)∗ equals:: IDEAL 3:def 25(Del(S,1))ˆ<∗(the carrier of A)∗> if meet(rng Del(S,1)) = meet rng S
otherwise (Del(S,1))ˆ<∗S.1∗>;
end;

この手順の正当性を証明するればすくとも最短条件 ii) を満足する分解が得られる.

4

考察
前章の 3.3.3. で言及したが, イデアル a の準素分解で準素因子が極小元で分解が表現された場合は既に最短表現（分解の因子が 1 つでも欠けると分解にならない）になっていると予想していたが証明には至らなかった. この原因は詳細に分析していないが, 極小元を準備して分解を構成した主な理由は分解を保ちながら準素因子の数を減らす為で最短条件 i) の証明では効果的であったが最短条件 ii) では巧く機能しなかった.
いま p1 ⊊ p2 を a の準素分解の素因子とするとき, p1 が素因子の中で極小元であるとき p2は埋没因子という. 準素因子 q1 , q2 がそれぞれ p1 -primary と p2 -primary であったとす√
ると根基を取ると p2 は a の素因子には現れず埋没する. 準素因子で考えると q2 が欠けていてもいいのか，欠くことが出来ないのか代数の計算で判断出来ない（出来なかった）

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

8/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

ので一つ一つ準素因子取り除いて分解が保たれているか判定ルーチンが入用となり前章の手順１を必要とした. 20 世紀初頭の数学証明は手順１の様な構成的なものが見受けられ（クロネッカーの多変数多項式の既約分解のアルゴリズム等）, 20 世紀初頭のイデアル論，
整数論の証明においては Mizar で形式化が出来ることが多いと思われる.
今後は手順１の正当性の証明．本稿では含まなかったが一意性定理, イデアル a に対し異なる最短な分解があってもそれらの素因子は同一であることを示した定理である．これも大事な定理であり形式化を行う．

参考文献[1] Atiyah MF, Macdonald IG. Introduction to Commutative Algebra. vol. 2. AddisonWesley Reading; 1969.
[2] Baanen A, Dahmen SR, Narayanan A, di Capriglio FAENMM.

A Formal-ization of Dedekind Domains and Class Groups of Global Fields.
tom Reason. 2022;66(4):611–637.

J Au-

Available from: https://doi.org/10.1007/

s10817-022-09644-0.
[3] Ballarin C, (Editor), et al. The Isabelle/HOL Algebra Library. 2023;Available from:https://isabelle.in.tum.de/library/HOL/HOL-Algebra/outline.pdf.
[4] Watase Y. Introduction to Algebraic Geometry. Formaliz Math. 2023;31(1):67–73.
Available from: https://doi.org/10.2478/forma-2023-0007.

Mizar article information
Mizar Mathematical Library (MML)
Works in Progress
IDEAL 3 On Primay Ideal Decomposition
by Y.Watase
We formalized the so-called Primary Decomposition of Ideal appeared in the chapter 4 of [1].
we call an ideal a of a commutative ring with the unit element, has a primary decomposition
when such a ﬁnite set of primary ideals {qi } that a = ∩{qi } holds. A decomposition is called
minimal whenpqi are all distinct and qi ⊉

Tn

j6=i

qj hold. This paper describes process ofdeveloping formal proofs for existence of a primary decomposition and its minimality.

Listing 9. IDEAL 3 - abstract:: On Primary Ideals. {P}art {II}:: by Yasushige Watase:::: Received June 30, 2021:: Copyright (c) 2021−2023 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

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

9/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition:: 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 ARYTM 3, FUNCT 1, RELAT 1, CARD 3, XBOOLE 0, TARSKI, XCMPLX 0,
STRUCT 0, SUBSET 1, SUPINF 2, NAT 1, CARD 1, ARYTM 1, FINSEQ 1, SETFAM 1,
INT 2, BINOP 1, GROUP 4, NUMBERS, IDEAL 1, ZFMISC 1, FUNCSDOM, CARD FIL,SQUARE 1, RING 2, XXREAL 0, TOPZARI1, LATTICEA, PARTFUN1, IDEAL 2, INT 3,
ORDINAL4, LATTICE3, CHORD, FINSEQ 3, MOEBIUS1, UPROOTS, FINSET 1, FSM 1,
MATROID0, TERMORD, WAYBEL 4, WELLORD2, DILWORTH, JORDAN4, ORDERS 2,
ORDERS 1,
IDEAL 3;notations TARSKI, XBOOLE 0, SUBSET 1, SETFAM 1, FUNCT 1, RELAT 1, ORDINAL1,
RELSET 1, PARTFUN1, WELLORD2, FUNCT 2, DOMAIN 1, FINSET 1, CARD 1,
ORDERS 1, NUMBERS, XCMPLX 0, XXREAL 0, FINSEQ 1, EQREL 1, FINSEQ 2,
FINSEQOP, FINSEQ 3, RVSUM 1, PRE POLY, STRUCT 0, ALGSTR 0, ORDERS 2,
RLVECT 1, GROUP 1, VECTSP 1, VECTSP 2, WAYBEL 4, YELLOW 1, GCD 1,
VECTSP10, UPROOTS, INT 3, IDEAL 1, RING 1, DILWORTH, RING 2, TOPZARI1,
IDEAL 2;constructors RELSET 1, FINSEQOP, FINSOP 1, WSIERP 1, WAYBEL 4, GCD 1,
DILWORTH, IDEAL 2;
registrations XBOOLE 0, ORDINAL1, RELSET 1, XREAL 0, NAT 1, STRUCT 0, CARD 1,
VECTSP 1, ALGSTR 1, SUBSET 1, ALGSTR 0, IDEAL 1, RING 2, INT 3, RING 1,
TOPZARI1, FINSEQ 1, FINSEQ 5, IDEAL 2, FINSET 1, FUNCT 2, RELAT 1,
FOMODEL0, ORDERS 2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
deﬁnitions TARSKI, IDEAL 1, STRUCT 0, XBOOLE 0,SUBSET 1;
equalities STRUCT 0, FINSEQ 1, ALGSTR 0;
expansions TARSKI, FUNCT 2, IDEAL 1, STRUCT 0, XBOOLE 0, SUBSET 1, TOPZARI1,
FUNCT 1, RING 1;
theorems RLVECT 1, IDEAL 1, FUNCT 2, TARSKI, FUNCT 1, NAT 1, RING 1, XBOOLE 0,
FINSEQ 1, ORDINAL1, XBOOLE 1, RING 2, RELAT 1, SETFAM 1, TOPZARI1,
FINSEQ 5, PARTFUN1, FINSEQ 3, FINSEQ 2, TOPREALA, CARD 1, IDEAL 2,
SUBSET 1, ZFMISC 1, FINSEQOP, TARSKI 0, CARD 2, CARD FIN, SETWISEO,
AOFA L00, DILWORTH, WELLORD2, ORDERS 2,
WAYBEL 4, BAGORDER, ORDINAL6;
schemes NAT 1, RECDEF 1, FUNCT 2;
begin :: Preliminaries: Some Properties of Ideals
reserve R for commutative Ring;
reserve A for non degenerated commutative Ring;
reserve I,J,q for Ideal of A;
reserve M,M1,M2 for Ideal of A/q;:: Generarization of ZMATRLIN:42
theorem :: IDEAL 3:1
for I be Ideal of A
for F be FinSequence of A
st for i being Nat st i in dom F holds F.i in I holds Sum F in I;
deﬁnition
let A;
func sqrt(A) −> Function of Ideals(A),Ideals(A) means:: IDEAL 3:def 1

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

10/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

for x be Element of Ideals (A) holds it.x = sqrt x;
end;
theorem :: IDEAL 3:2
for I be Ideal of A, F be non empty FinSequence of Ideals(A) holdsrng((%I)∗F) <> {} & rng F <> {} &meet rng((%I)∗F) c= the carrier of A;::[AM]Ex.1.12. iv) (/\F i % I) = /\(F i % I)
theorem :: IDEAL 3:3
for I be Ideal of A, F be non empty FinSequence of Ideals(A) holds(%I).(meet rng F) = meet rng((%I)∗F);
theorem :: IDEAL 3:4
for I be Ideal of A, F be non empty FinSequence of Ideals(A) holdsrng((sqrt(A))∗F) <> {} & rng F <> {};registration
let A;
let a be non empty FinSequence of Ideals(A);cluster meet (rng a) −> add−closed left−ideal right−ideal for Subset of A;
end;
reserve x for object;theorem :: IDEAL 3:5
x in Ideals A iﬀ x is Ideal of A;
theorem :: IDEAL 3:6
x in PRIMARY(A) iﬀ x is primary Ideal of A;
theorem :: IDEAL 3:7
PRIMARY(A) c= Ideals (A);theorem :: IDEAL 3:8
x in Spectrum A iﬀ x is prime Ideal of A;
theorem :: IDEAL 3:9
for I be Ideal of A, F be non empty FinSequence of Ideals(A) holds(sqrt(A)).(meet rng F) = meet rng((sqrt(A))∗F);
theorem :: IDEAL 3:10
for I be Ideal of A, F be non empty FinSequence of Ideals(A) holds(%I)∗F is non empty FinSequence of Ideals(A);deﬁnition
let A;
let I be Ideal of A;
attr I is primary decomposable means:: IDEAL 3:def 2
ex q be non empty ﬁnite Subset of PRIMARY(A) st
I = meet q;
end;registration
let A be non degenerated commutative Ring;cluster primary decomposable for Ideal of A;
end;
deﬁnition
let A;
let I be primary decomposable Ideal of A;
let q be non empty ﬁnite Subset of PRIMARY(A);pred q is a primary decomposition of I means:: IDEAL 3:def 3

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

11/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

I = meet q;
end;
reserve F for FinSequence of Ideals(A);::Th2SPEC2::: Spectrum(A) c= Ideals(A)reserve x for Element of A,
o for object;deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func prime divset(q) −> non empty ﬁnite Subset of Spectrum A equals:: IDEAL 3:def 4(sqrt(A)).:q;
end;
deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func PFactors(q) −> Function of prime divset(q), bool PRIMARY(A) means:: IDEAL 3:def 5
for x be Element of prime divset(q) holds ex p1 be prime Ideal of A st
x = p1 & it.x = (sqrt(A))”{p1} /\ q;
end;theorem :: IDEAL 3:11
for q be non empty ﬁnite Subset of PRIMARY(A),x1,x2 be Element of prime divset(q) holds
x1 <> x2 implies (PFactors(q)).x1 /\ (PFactors(q)).x2 = {};registration
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);cluster PFactors(q) −> one−to−one;end;theorem :: IDEAL 3:12
for q be non empty ﬁnite Subset of PRIMARY(A) holds
union(rng (PFactors(q))) = q;theorem :: IDEAL 3:13
for p1 be prime Ideal of A holds(sqrt(A))”{p1} /\ PRIMARY(A) = PRIMARY(A,p1);
theorem :: IDEAL 3:14
for q be non empty ﬁnite Subset of PRIMARY(A),p be prime Ideal of A st p in prime divset(q) holds(PFactors(q)).p is non empty ﬁnite Subset of PRIMARY(A,p) &(PFactors(q)).p = PRIMARY(A,p) /\ q;theorem :: IDEAL 3:15
for q be non empty ﬁnite Subset of PRIMARY(A),p be prime Ideal of A st p in prime divset(q) holds
meet((PFactors(q)).p) in PRIMARY(A,p);deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func Red(q) −> Function of prime divset(q), PRIMARY(A) means:: IDEAL 3:def 6
for x be Element of prime divset(q) holds it.x = meet((PFactors(q)).x);

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

12/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

end;
theorem :: IDEAL 3:16
for q be non empty ﬁnite Subset of PRIMARY(A),x1,x2 be Element of prime divset(q) holds(Red(q)).x1 = (Red(q)).x2 implies x1 = x2;
registration
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);cluster Red(q) −> one−to−one;end;theorem :: IDEAL 3:17
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &p1 in prime divset(q1) holds card (prime divset(q1) \{p1}) = n;::theorem Th9B::: for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,:: p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &:: p1 in prime divset(q1) holds:: not (PFactors(q1)).p1 c=:: union rng((PFactors(q1))|(prime divset(q1) \{p1}))
theorem :: IDEAL 3:18
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &p1 in prime divset(q1) holdsrng((PFactors(q1))|(prime divset(q1) \{p1})) /\ {(PFactors(q1)).p1} = {} &rng (PFactors(q1)) =rng((PFactors(q1))|(prime divset(q1) \{p1})) \/ {(PFactors(q1)).p1};
theorem :: IDEAL 3:19
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &p1 in prime divset(q1) holds(PFactors(q1)).p1 misses union rng((PFactors(q1))|(prime divset(q1) \{p1}));
theorem :: IDEAL 3:20
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &p1 in prime divset(q1) holdsrng((Red(q1))|(prime divset(q1) \{p1})) /\ {(Red(q1)).p1} = {} &rng (Red(q1)) = rng((Red(q1))|(prime divset(q1) \{p1})) \/ {(Red(q1)).p1} &rng(Red(q1)) /\ {(Red(q1)).p1} = {(Red(q1)).p1} &rng (Red(q1)) \ {(Red(q1)).p1} = rng((Red(q1))|(prime divset(q1) \{p1}));
theorem :: IDEAL 3:21
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &p1 in prime divset(q1) holds
meet rng Red(q1)= meet rng((Red(q1))|(prime divset(q1) \{p1})) /\ (Red(q1)).p1;::theorem Th10A0::: for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,:: p1 be prime Ideal of A st card prime divset(q1) = n+1 &:: p1 in (prime divset(q1)) holds:: ex qn be non empty ﬁnite Subset of PRIMARY(A) st:: (prime divset(q1) \{p1}) = prime divset(qn) &:: qn = q1 \(PFactors(q1)).p1 &:: PFactors(qn) = (PFactors(q1))|(prime divset(q1) \{p1}) &:: union rng(PFactors(qn)) = q1 \(PFactors(q1)).p1
deﬁnition
let A;

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

13/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

let q be non empty ﬁnite Subset of PRIMARY(A);attr q is minlength means:: IDEAL 3:def 7
card q =1 orfor q1 be Element of q holds meet(q \ {q1}) c/= q1;
end;::theorem Th001::: for q1 be non empty ﬁnite Subset of PRIMARY(A), p1 be prime Ideal of A:: st prime divset(q1) = {p1} holds q1 c= PRIMARY(A,p1)
theorem :: IDEAL 3:22
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &p1 in prime divset(q1) holds card (prime divset(q1) \{p1}) = n;theorem :: IDEAL 3:23
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A
st card prime divset(q1) = n+1 & p1 in (prime divset(q1)) holds
ex qn be non empty ﬁnite Subset of PRIMARY(A) st(prime divset(q1) \{p1}) = prime divset(qn) & qn = q1 \(PFactors(q1)).p1;
theorem :: IDEAL 3:24
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A
st card prime divset(q1) = n+1 & p1 in (prime divset(q1)) holds
ex qn be non empty ﬁnite Subset of PRIMARY(A) st(prime divset(q1) \{p1}) = prime divset(qn) & qn = q1 \(PFactors(q1)).p1 &union rng((PFactors(q1))|(prime divset(q1) \{p1})) = q1 \(PFactors(q1)).p1;
theorem :: IDEAL 3:25
for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,
p1 be prime Ideal of A st card prime divset(q1) = n+1 &p1 in (prime divset(q1)) holds
ex qn be non empty ﬁnite Subset of PRIMARY(A) st(prime divset(q1) \{p1}) = prime divset(qn) &qn = q1 \(PFactors(q1)).p1 &PFactors(qn) = (PFactors(q1))|(prime divset(q1) \{p1}) &union rng(PFactors(qn)) = q1 \(PFactors(q1)).p1;
theorem :: IDEAL 3:26
for q be non empty ﬁnite Subset of PRIMARY(A) holds
meet (union(rng PFactors(q))) = meet rng Red(q);::theorem Th9B::: for q1 be non empty ﬁnite Subset of PRIMARY(A), n be non zero Nat,:: p1 be prime Ideal of A st card(prime divset(q1)) = n+1 &:: p1 in prime divset(q1) holds:: not (PFactors(q1)).p1 c=:: union rng((PFactors(q1))|(prime divset(q1) \{p1}))
theorem :: IDEAL 3:27
for q be non empty ﬁnite Subset of PRIMARY(A) holds
meet q = meet rng Red(q);::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::theorem Th12::: for q be non empty ﬁnite Subset of PRIMARY(A) holds:: meet minimals(InclPoset(rng Red(q))) = meet rng Red(q);:: func UpperCone(S) −> Subset of A equals:::: ORDERS 2:def 8:: {a1 : for a2 st a2 in S holds a2 <MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

14/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition::theorem :: ORDERS 2:51:: a is minimal in the InternalRel of A iﬀ for b holds not b < a;::theorem Th2K::: for S be non empty Subset of Ideals(A),:: x be Element of RelStr(# S,RelIncl(S) #) holds:: x in minimals(RelStr(# S,RelIncl(S) #)) implies:: x is minimal in S & x is minimal wrt S,RelIncl(S)theorem :: IDEAL 3:28
for S be non empty ﬁnite Subset of Ideals(A) holds
minimals(RelStr(# S,RelIncl(S) #)) <> {};deﬁnition
let A;
let S be non empty ﬁnite Subset of Ideals(A);func minimals(S) −> non empty Subset of Ideals(A) equals:: IDEAL 3:def 8
minimals(RelStr(# S,RelIncl(S) #));
end;
deﬁnition
let A;
let S be non empty ﬁnite Subset of Ideals(A);func Upper(S) −> Function of minimals(S), bool S
means:: IDEAL 3:def 9
for x be Element of minimals(S) holds
ex x1 be Element of RelStr(# S,RelIncl(S) #) stx = x1 & it.x = UpperCone({x1}) \/ {x1};end;theorem :: IDEAL 3:29
for S be non empty ﬁnite Subset of Ideals(A) holds
Upper(S) is one−to−one;registration
let A;
let S be non empty ﬁnite Subset of Ideals(A);cluster Upper(S) −> one−to−one;end;theorem :: IDEAL 3:30
for S be non empty ﬁnite Subset of Ideals(A) holds
union rng Upper(S) = S;deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);let a be Element of rng Red(q);func Lower(a) −> Subset of rng Red(q) equals:: IDEAL 3:def 10{I where I is Element of rng Red(q) : I c< a };end;
theorem :: IDEAL 3:31
for S be non empty Subset of Ideals(A) holds
RelStr(# S,RelIncl(S) #) is Poset;
deﬁnition
let A;
let S be non empty ﬁnite Subset of Spectrum A;
attr S is without−embedded−prime means

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

15/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition:: IDEAL 3:def 11
for x,y be Element of S holds (x c/= y & y c/= x);end;
deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);attr q is reduced means:: IDEAL 3:def 12
card q =1 orfor q1 be Element of q holds meet(q \ {q1}) c/= q1;
end;
deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);attr q is radical−distinct means:: IDEAL 3:def 13
card q =1 orfor q1,q2 be Element of q st q1 <> q2 holds ex I1,I2 be Ideal of A st
q1 = I1 & q2 = I2 & sqrt I1 <> sqrt I2;
end;
deﬁnition
let A;
let S be non empty ﬁnite Subset of PRIMARY(A);attr S is minimal means:: IDEAL 3:def 14
S is radical−distinct reduced or
S is reduced radical−distinct;
end;
deﬁnition
let A;
let q be non empty ﬁnite Subset of Ideals(A);attr q is reduced means:: IDEAL 3:def 15
card q =1 orfor q1 be Element of q holds meet(q \ {q1}) c/= q1;
end;
deﬁnition
let A;
let q be non empty ﬁnite Subset of Ideals(A);attr q is radical−distinct means:: IDEAL 3:def 16
card q =1 orfor q1,q2 be Element of q st q1 <> q2 holds ex I1,I2 be Ideal of A st
q1 = I1 & q2 = I2 & sqrt I1 <> sqrt I2;
end;
deﬁnition
let A;
let S be non empty ﬁnite Subset of Ideals(A);attr S is minimal means:: IDEAL 3:def 17
S is radical−distinct reduced or
S is reduced radical−distinct;
end;::Lm12::: for q be non empty ﬁnite Subset of PRIMARY(A)MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

16/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition:: holds card(prime divset(q)) is Nat::theorem Th12::: for q be non empty ﬁnite Subset of PRIMARY(A):: holds prime divset(q) = prime divset(rng Red(q))
theorem :: IDEAL 3:32
for q be non empty ﬁnite Subset of PRIMARY(A)st card(prime divset(q)) > 1 holds rng Red(q) is radical−distinct;
theorem :: IDEAL 3:33
for q be non empty ﬁnite Subset of PRIMARY(A) st rng Red(q) <> {} holds
minimals(RelStr(# rng Red(q),RelIncl(rng Red(q)) #)) <> {} &rng Red(q) is non empty ﬁnite Subset of Ideals(A);deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func minimalRed(q) −> non empty ﬁnite Subset of Ideals(A) equals:: IDEAL 3:def 18
minimals(RelStr(# rng Red(q),RelIncl(rng Red(q)) #));
end;
deﬁnition
let A;
let q be non empty ﬁnite Subset of PRIMARY(A);func RedRng(q) −> non empty ﬁnite Subset of Ideals(A) equals:: IDEAL 3:def 19
rng Red(q);end;theorem :: IDEAL 3:34
for S be non empty ﬁnite Subset of Ideals(A),a1 be Element of RelStr(# S,RelIncl(S) #) st
UpperCone({a1}) <> {}holds a1 c= meet UpperCone({a1});
theorem :: IDEAL 3:35
for S be non empty ﬁnite Subset of Ideals(A),a0 be Element of minimals(S) holds a0 = meet((Upper(S)).a0);
theorem :: IDEAL 3:36
for S be non empty ﬁnite Subset of Ideals(A),a0 be Element of minimals(S), a be set st a in (Upper(S)).a0
holds a0 c= a;theorem :: IDEAL 3:37
for q be non empty ﬁnite Subset of PRIMARY(A) stcard(minimals(RedRng(q))) = 1 holds
meet minimals(RedRng(q)) = meet (union rng Upper(RedRng(q)));::theorem Th20Z::: for q be non empty ﬁnite Subset of PRIMARY(A),:: a0 be Element of minimals(RedRng(q)) holds a0 = meet((Upper(RedRng(q))).a0)
theorem :: IDEAL 3:38
for S be non empty Subset of Ideals(A),x be Element of RelStr(# S,RelIncl(S) #) holds
x in minimals(RelStr(# S,RelIncl(S) #)) impliesx is minimal in S & x is minimal wrt S,RelIncl(S);theorem :: IDEAL 3:39
for q be non empty ﬁnite Subset of PRIMARY(A) st rng Red(q) <> {} holds
minimals(RelStr(# rng Red(q),RelIncl(rng Red(q)) #)) <> {} &rng Red(q) is non empty ﬁnite Subset of Ideals(A);

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

17/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition

theorem :: IDEAL 3:40
for q be non empty ﬁnite Subset of PRIMARY(A)holds
meet union(rng Upper(RedRng(q))) = meet minimalRed(q);theorem :: IDEAL 3:41
for q be non empty ﬁnite Subset of PRIMARY(A)holds meet q = meet minimalRed(q);theorem :: IDEAL 3:42 :::::Copy from IDEAL 2, Th36
for Q be primary Ideal of A holds
sqrt Q is prime & for P be prime Ideal of A st Q c= P holds sqrt Q c= P;
theorem :: IDEAL 3:43
for q be non empty ﬁnite Subset of PRIMARY(A)holds minimalRed(q) is radical−distinct;
theorem :: IDEAL 3:44
for S be non empty ﬁnite Subset of Ideals(A),s1,s2 be Element of minimals(S) st s1 <> s2 holds
ex x be Element of A st x in s1 \ s2;theorem :: IDEAL 3:45
for S be non empty ﬁnite Subset of Ideals(A),s1,s2 be Element of minimals(S) st s1 <> s2 holds
s1 c/= s2 & s2 c/= s1;:: non empty is important::::::::::
deﬁnition
let A;
let I be Ideal of A;
attr I is primary decomposable means:: IDEAL 3:def 20
ex q be non empty one−to−one FinSequence of PRIMARY(A) st
I = meet rng q;
end;registration
let A be non degenerated commutative Ring;cluster primary decomposable for Ideal of A;
end;
deﬁnition
let A;
let I be primary decomposable Ideal of A;
let q be non empty one−to−one FinSequence of PRIMARY(A);pred q is a primary decomposition of I means:: IDEAL 3:def 21
I = meet rng q;
end;
deﬁnition
let A;
let I be primary decomposable Ideal of A;
mode primary decomposition of I −> non empty one−to−one
FinSequence of PRIMARY(A) means:: IDEAL 3:def 22
I = meet rng it;
end;
deﬁnition
let A;
let I be primary decomposable Ideal of A;
mode primary decomposition of I −> non empty one−to−one
FinSequence of PRIMARY(A) means

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

18/19

Mechanized Mathematics and Its Applications, Works in Progress

Primary Decomposition:: IDEAL 3:def 23
I = meet rng it;
end;reserve I for primary decomposable Ideal of A,
S for primary decomposition of I,
x for Element of A,
o for object;deﬁnition
let A;
let S be non empty FinSequence of PRIMARY(A);func prime div(S) −> non empty FinSequence of Spectrum A equals:: IDEAL 3:def 24(sqrt(A))∗S;end;
deﬁnition
let A;
let S be Element of (Ideals A)∗ ;func Trimming(S) −> Element of (Ideals A)∗ equals:: IDEAL 3:def 25(Del(S,1))ˆ<∗(the carrier of A)∗> if meet(rng Del(S,1)) = meet rng S
otherwise (Del(S,1))ˆ<∗S.1∗>;
end;::deﬁnition:: let A;:: let n be Nat;:: let S be Element of (Ideals A)∗ ;:: func Trimming(S,n) −> Function of (Ideals A)∗ , (Ideals A)∗ means:::: IDEAL 3:def 26:: for x be Element of (Ideals A)∗ holds it.x = Trimming(x);::end;
deﬁnition
let A;
let n be Nat such that0 <> n;let S be Element of (Ideals A)∗ ;func Trimming(S,n) −> Element of (Ideals A)∗ means:: IDEAL 3:def 27
ex f being FinSequence of (Ideals A)∗ st
it = f.len f & len f = n & f.1 = S &for i being Nat st i in dom f & i+1 in dom f holds
f.(i+1) = Trimming(f/.i);end;

MMA-WiP (2024), vol.6, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2024.6.1 - ISSN 2434-5458 (Online)

19/19