# 有限雙邊理想：在上三角矩陣環中分開核對左吸收與右吸收 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-two-sided-ideal/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-finite-two-sided-ideal-01 · production-20261019-adopted-96 ## 目標與範圍 父環 U 是 𝔽₂ 上 2×2 上三角矩陣環（元素記為 (a,b,c)，代表第一行 (a,b)、第二行 (0,c)），已通過有限含一環資格。（一）證明 I={(0,0,0),(0,1,0)} 是 U 的雙邊理想。（二）證明 L={(0,0,0),(1,0,0)} 滿足左吸收，但不是雙邊理想。（三）證明對角子環 D={(a,0,c)} 含 1 卻不是理想。（四）說明 {0} 與 U 本身是雙邊理想。 在 MKO 的範圍內工作：父環以完整雙表通過有限含一環資格，候選子集由互異載體元素完整列出（假設 a1）；左吸收與右吸收分開量化，並以對全部父環元素成立的公式證書核對，不以抽樣代替（假設 a2）。不處理商環（下一節點），不重新核對父環公理，不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - matrix_product_def - mul_zero - and_intro_elim - quantifier_negation - numeric_evaluation - G1 — U 的載體是 8 個三元組 (a,b,c)∈{0,1}³；加法逐項 mod 2；乘法 (a,b,c)(a',b',c')=(aa', ab'+bc', cc') mod 2（由矩陣乘積得到）。零元 (0,0,0)，單位元 1_U=(1,0,1)。 - G2 — U 已由父節點以完整加法表與乘法表通過有限含一環資格；本稿不重新核對環公理。 - G3 — 候選子集：I={(0,0,0),(0,1,0)}；L={(0,0,0),(1,0,0)}；D={(0,0,0),(1,0,0),(0,0,1),(1,0,1)}，即所有 (a,0,c)。 - U — 𝔽₂ 上 2×2 上三角矩陣環，8 個元素 - (a,b,c) — 第一行 (a,b)、第二行 (0,c) 的矩陣，a,b,c∈{0,1} - E_{11},E_{12},E_{22} — (1,0,0)、(0,1,0)、(0,0,1) - 1_U=(1,0,1) — U 的乘法單位元 - I,\ L,\ D — 三個候選子集 - \beta\in\{0,1\} — I 或 L 中元素的參數 ## 規則與來源 - matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。 - set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - add_zero · prerequisite — 加法單位元：u+0=u。 - contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - mul_one · prerequisite — 乘法單位元：1·u=u。 - subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。 - mko_ideal_def · cited — 給有限含一環 R 與完整子集 I。I 須非空、對加法及加法逆元封閉，並對所有 r∈R、x∈I 同時有 rx∈I 與 xr∈I。資格永遠綁定同一父環；左吸收與右吸收分開量化。 · mko-finite-two-sided-ideal - f2_arith · prerequisite — 𝔽₂={0,1} 以 mod 2 運算：0+0=0、0+1=1、1+1=0；−0=0、−1=1；0·t=0、1·1=1。 - one_sided_subring_def · prerequisite — 左理想：非空、對加法與加法逆元封閉，且對所有 r∈R、x∈J 有 rx∈J（右理想對稱地要求 xr∈J）。子環：含 1、對加法、加法逆元與乘法封閉的子集。 - L_one_in_ideal · lemma — 在含一環 R 中，若滿足右吸收（xr∈J）的子集 J 含 1，則 J=R。 ## 逐步主鏈 S01 · definition操作前 I\ \text{two-sided ideal of}\ U 操作後 I\subseteq U,\ I\neq\varnothing,\ I+I\subseteq I,\ -I\subseteq I,\ \forall r\,\forall x:\ rx\in I,\ \forall r\,\forall x:\ xr\in I 條件：無 規則：mko_ideal_def · 依賴：mko_ideal_def, G2 葉節點依據：mko_ideal_def + def_unfold 依 MKO 展開雙邊理想的六項責任：是父環 U 的子集、非空、對加法封閉、對加法逆元封閉、左吸收、右吸收。兩個吸收條件各自量化全部 r∈U 與 x∈I，必須分開核對。父環固定為 G2 的 U。 S02 · equivalent操作前 I=\{(0,0,0),(0,1,0)\} 操作後 I=\{(0,\beta,0):\beta\in\{0,1\}\}\subseteq U,\ \ (0,0,0)\in I 條件：無 規則：set_builder · 依賴：G1, G3, S01 葉節點依據：set_builder + set_extensionality I 的兩個元素是互異的載體元素，都是 {0,1}³ 中的三元組，所以 I⊆U；用參數 β 把 I 寫成 {(0,β,0)}，β=0 給零元、β=1 給 E₁₂。零元在 I 中，所以 I 非空。 S03 · implies操作前 (0,\beta,0)+(0,\beta',0) 操作後 (0,\ (\beta+\beta')\bmod 2,\ 0)\in I 條件：無 規則：f2_arith · 依賴：S02, G1, f2_arith 葉節點依據：f2_arith + set_builder 加法逐項 mod 2：第一、三項 0+0=0，第二項 β+β' mod 2 屬於 {0,1}，所以和仍是 (0,β'',0) 的形式，屬於 I。這涵蓋全部 4 個有序和（0+0=0、0+E₁₂=E₁₂、E₁₂+0=E₁₂、E₁₂+E₁₂=0）。 S04 · implies操作前 -(0,\beta,0) 操作後 (0,\ (-\beta)\bmod 2,\ 0)=(0,\beta,0)\in I 條件：無 規則：f2_arith · 依賴：S02, f2_arith 葉節點依據：f2_arith + add_inverse 加法逆元逐項取：−0=0，−β mod 2=β（因 −1≡1）。所以每個元素是自己的加法逆元，逆元仍在 I 中。核對：(0,β,0)+(0,β,0)=(0,2β mod 2,0)=(0,0,0)。 S05 · implies操作前 r\cdot x=(a,b,c)(0,\beta,0),\ \ r\in U,\ x\in I 操作後 r\cdot x=(0,\ a\beta\bmod 2,\ 0)\in I 條件：無 規則：matrix_product_def · 依賴：G1, S02 葉節點依據：matrix_product_def + mul_zero + f2_arith 左吸收：用 G1 的乘法公式，r=(a,b,c) 任意、x=(0,β,0) 任意，乘積是 (a·0, aβ+b·0, c·0)。子步 S05.1、S05.2 逐項計算：第一、三項為 0，第二項 aβ mod 2∈{0,1}。所以 rx 屬於 I。公式對全部 8 個 r 與 2 個 x（16 個乘積）同時成立。 S06 · implies操作前 x\cdot r=(0,\beta,0)(a,b,c),\ \ r\in U,\ x\in I 操作後 x\cdot r=(0\cdot a,\ 0\cdot b+\beta c,\ 0\cdot c)=(0,\ \beta c\bmod 2,\ 0)\in I 條件：無 規則：matrix_product_def · 依賴：G1, S02 葉節點依據：matrix_product_def + mul_zero + f2_arith 右吸收必須另外核對，因為 U 不交換。乘法公式給 xr=(0·a, 0·b+βc, 0·c)：第一、三項為 0，第二項 βc mod 2∈{0,1}。所以對全部 r∈U、x∈I，xr∈I。 S07 · implies操作前 \text{S02 to S06} 操作後 I=\{0,E_{12}\}\ \text{is a two-sided ideal of}\ U 條件：無 規則：and_intro_elim · 依賴：S01, S02, S03, S04, S05, S06 葉節點依據：and_intro_elim + mko_ideal_def 六項責任都已證明：子集與非空（S02）、加法封閉（S03）、逆元封閉（S04）、左吸收（S05）、右吸收（S06）。依合取引入與 S01 的定義，I 是 U 的雙邊理想。 S08 · implies操作前 L=\{(\beta,0,0):\beta\in\{0,1\}\},\ \ r=(a,b,c) 操作後 r\cdot(\beta,0,0)=(a\beta,\ a\cdot 0+b\cdot 0,\ c\cdot 0)=(a\beta\bmod 2,0,0)\in L 條件：無 規則：matrix_product_def · 依賴：G1, G3, one_sided_subring_def, f2_arith 葉節點依據：matrix_product_def + mul_zero + f2_arith + one_sided_subring_def L 非空，E₁₁+E₁₁=(0,0,0)、−E₁₁=E₁₁，所以加法部分與 I 相同地成立。左吸收：對任意 r=(a,b,c)，r(β,0,0)=(aβ,0,0)∈L。所以 L 是左理想。 S09 · implies操作前 E_{11}\cdot E_{12}=(1,0,0)(0,1,0) 操作後 E_{11}E_{12}=(0,\ 1\cdot1+0\cdot0,\ 0)=(0,1,0)\notin L\ \Rightarrow\ L\ \text{not two-sided} 條件：無 規則：quantifier_negation · 依賴：S08, G1 葉節點依據：quantifier_negation + matrix_product_def + numeric_evaluation 取 x=E₁₁∈L、r=E₁₂∈U，右乘積 xr=(1·0, 1·1+0·0, 0·0)=(0,1,0)。L 的元素第二項都是 0，所以 (0,1,0)∉L。右吸收的全稱命題有一個反例，L 不是雙邊理想。這正是 MKO 指出的「只核左吸收」的誤解。 S10 · implies操作前 D=\{(a,0,c)\},\ \ (a,0,c)(a',0,c') 操作後 (aa',\ a\cdot0+0\cdot c',\ cc')=(aa',0,cc')\in D,\ \ 1_U=(1,0,1)\in D 條件：無 規則：one_sided_subring_def · 依賴：G1, G3, one_sided_subring_def 葉節點依據：one_sided_subring_def + matrix_product_def + mul_zero D 是子環：兩個對角元的乘積第二項為 a·0+0·c'=0，仍是對角；加法逐項保持第二項為 0；每個元素是自己的加法逆元；單位元 (1,0,1) 在 D 中。MKO 提醒：子環不能與理想混稱，S11 說明 D 不是理想。 S11 · implies操作前 1_U\in D,\ \ E_{12}\notin D 操作後 D\ \text{is not an ideal};\ \text{witness}\ E_{12}\cdot E_{22}=(0,1,0)\notin D 條件：無 規則：L_one_in_ideal · 依賴：S10, G1 葉節點依據：contrapositive + matrix_product_def + numeric_evaluation 依引理 L_one_in_ideal，若 D 滿足右吸收且含 1，則 D=U；但 E₁₂=(0,1,0)∉D，所以 D 不滿足右吸收。具體見證：E₁₂E₂₂=(0·0, 0·0+1·1, 0·1)=(0,1,0)∉D（左吸收亦失敗，r=E₁₂、x=E₂₂）。引理在子步 S11.1、S11.2 證明。 S12 · implies操作前 \{0\},\ U 操作後 r0=0r=0\in\{0\};\ \ rx,xr\in U\ \Rightarrow\ \{0\},\ U\ \text{two-sided ideals} 條件：無 規則：mko_ideal_def · 依賴：G1, mko_ideal_def 葉節點依據：mko_ideal_def + mul_zero + add_zero 零理想：0+0=0、−0=0，且對所有 r，r·0=0·r=0（mul_zero 對矩陣逐項成立）。整個環：乘法對 U 封閉，所以吸收自動成立。MKO 指出這兩個都是雙邊理想。 S13 · implies操作前 \text{S07},\ \text{S09},\ \text{S11},\ \text{S12} 操作後 I\ \text{two-sided};\ L\ \text{left only};\ D\ \text{subring, not ideal};\ \{0\},U\ \text{two-sided} 條件：無 規則：and_intro_elim · 依賴：S07, S08, S09, S10, S11, S12 葉節點依據：and_intro_elim 合併四個任務：I={0,E₁₂} 是雙邊理想；L={0,E₁₁} 是左理想但不是雙邊理想；對角子環 D 不是理想；{0} 與 U 是雙邊理想。所有判定都綁定同一父環 U。 ## 局部子步與引理 S05.1 · equivalent操作前 (a\cdot 0,\ \ast,\ c\cdot 0) 操作後 (0,\ \ast,\ 0) 條件：無 規則：mul_zero · 依賴：G1, mul_zero 葉節點依據：mul_zero 第一項 aa' 中 a'=0，第三項 cc' 中 c'=0；任何數乘 0 得 0。 S05.2 · implies操作前 a\beta+b\cdot 0 操作後 a\beta\bmod 2\in\{0,1\} 條件：無 規則：f2_arith · 依賴：S05.1, f2_arith 葉節點依據：f2_arith + mul_zero + add_zero 第二項 ab'+bc' 中 b'=β、c'=0，所以是 aβ+0=aβ，取 mod 2 後屬於 {0,1}。因此乘積具有 (0,β'',0) 的形式，屬於 I。 S11.1 · implies操作前 1\in J,\ \ \forall x\in J\ \forall r\in R:\ xr\in J 操作後 \forall r\in R:\ r=1\cdot r\in J 條件：無 規則：forall_elim · 依賴：one_sided_subring_def 葉節點依據：forall_elim + mul_one 在右吸收中取 x=1：對每個 r∈R，1·r∈J；而 1·r=r（單位元），所以 r∈J。 S11.2 · implies操作前 R\subseteq J,\ \ J\subseteq R 操作後 J=R 條件：無 規則：set_extensionality · 依賴：S11.1, set_extensionality 葉節點依據：set_extensionality + subset_def S11.1 給 R⊆J，J 本來就是 R 的子集，依集合外延性 J=R。S11.1 與 S11.2 合起來證得引理 L_one_in_ideal。 ## 逐步反向審查 - S13 · sufficient_goal_reduction · S07, S09, S11, S12, and_intro_elim — 目標 G 是四項判定的合取；H 由 S07、S09、S11、S12 正向證得，H⇒G 由合取引入，沒有把 G 當作前提。 - S12 · premise_audit · mko_ideal_def, mul_zero — 零乘任何元素為零是環公理的推論；U 的封閉性來自父環資格（G2）。 - S11.2 · premise_audit · S11.1, set_extensionality — 兩個方向的包含都已具備，集合相等。 - S11.1 · premise_audit · forall_elim, mul_one — 需要 1∈J 與單位元性質 1·r=r；只用右吸收的一個特例。 - S11 · premise_audit · S10, L_one_in_ideal, contrapositive — 使用引理的逆否：J≠R 且 1∈J ⇒ J 不滿足右吸收；具體乘積由 N6 核對。 - S10 · premise_audit · one_sided_subring_def, matrix_product_def — 子環要求的是對 D 內元素的乘法封閉，不是對全部 r∈U 的吸收；不宣稱 D 是理想。 - S09 · premise_audit · S08, quantifier_negation — 一個反例足以否定（N5）；S08 的左吸收仍然成立，兩者不矛盾。 - S08 · premise_audit · one_sided_subring_def, matrix_product_def, f2_arith — 這只證明了左吸收；MKO 要求右吸收另外量化，見 S09。 - S07 · sufficient_goal_reduction · S01, S02, S03, S04, S05, S06, and_intro_elim — 目標 G：I 是雙邊理想。足夠條件 H：六項責任；H⇒G 由 S01。H 的每一項都由 G1 到 G3 正向證得，沒有把 G 當作前提。 - S06 · premise_audit · G1, matrix_product_def, mul_zero — 與 S05 是不同的乘積（左右因子對調），不能由 S05 推出；這裡獨立計算（N4）。 - S05.2 · premise_audit · f2_arith, S05.1 — 只需第二項落在 {0,1}；I 對第二項沒有其他限制。 - S05.1 · inverse_equivalence · mul_zero — a·0=0 是恆等式，兩邊同值。 - S05 · premise_audit · G1, S02, matrix_product_def — a、b、c、β 沒有被指定數值，所以這是全稱證書，不是抽樣；N3 在全部 4 個 (a,c) 組合上重算第一、三項。 - S04 · premise_audit · f2_arith — 依賴特徵 2 的算術（N2）；在其他環中加法逆元不一定是自己，必須另外核對。 - S03 · premise_audit · f2_arith, S02 — 用到的是 𝔽₂ 加法封閉於 {0,1}（N1 核 1+1=0）；不宣稱反向。 - S02 · inverse_equivalence · set_builder, set_extensionality — β 取遍 {0,1} 恰好列出 I 的兩個元素，兩種寫法是同一集合。 - S01 · premise_audit · mko_ideal_def, G2 — 只展開定義；若換了父環（例如把 I 看成另一個環的子集），結論不能沿用。 ## 錯誤控制與反例 只核左吸收不夠MKO 指出的誤解之一是只核左吸收。L={0,E₁₁} 對所有 r 滿足 rx∈L，但 E₁₁E₁₂=E₁₂∉L。在非交換環中 rx 與 xr 是不同的乘積，必須分開對全部父環元素核對（S05、S06 分別處理）。 乘法封閉不足以判定理想另一個誤解是只核乘法封閉。D 對 D 內乘法封閉且含 1，是子環，但理想要求吸收所有父環元素；E₁₂E₂₂=E₁₂∉D。更一般地，含 1 且吸收的子集必是整個環（引理 L_one_in_ideal），所以真子環若含 1 就不可能是理想。 資格綁定同一父環同一個子集在不同父環中結論可能不同：例如 L 若被看成對角子環 D 的子集，D 交換，L 在 D 中是雙邊理想（(a,0,c)(β,0,0)=(aβ,0,0)=(β,0,0)(a,0,c)）；但在 U 中不是。所以每個判定都必須寫明父環。 - L={0,E₁₁} 對所有 r∈U 有 rx∈L，所以 L 是 U 的雙邊理想 → reject — 右吸收失敗：E₁₁E₁₂=(0,1,0)∉L。 - 對角集合 D 對乘法封閉且含 1，所以是 U 的理想 → reject — E₁₂E₂₂=(0,1,0)∉D；含 1 的理想必為整個 U。 - 抽查 r=1_U 與 r=E₁₁ 時 rx、xr 都在 I 中，所以 I 是雙邊理想 → reject — 結論雖然正確，但抽查不是證明；需要 S05、S06 對全部 8 個 r 的公式證書。 - L 在 D 中是雙邊理想，所以 L 在 U 中也是雙邊理想 → reject — 資格綁定父環；在 U 中 E₁₁E₁₂=E₁₂∉L。 ## 結論與限制 在 𝔽₂ 上 2×2 上三角矩陣環 U 中：I={(0,0,0),(0,1,0)} 非空、對加法與逆元封閉，且對所有 r∈U 有 rx=(0,aβ,0)∈I、xr=(0,βc,0)∈I，所以是雙邊理想。L={(0,0,0),(1,0,0)} 有左吸收，但 E₁₁E₁₂=E₁₂∉L，不是雙邊理想。對角子環 D 含 1 卻 D≠U，E₁₂E₂₂=E₁₂∉D，不是理想。{0} 與 U 是雙邊理想。 - U 的有限含一環資格取自父節點（G2），本稿未重新核對環公理；乘法公式由矩陣乘積導出，8×8 完整表未逐格印出。 - 第三個負向控制的主張結論本身為真，被拒絕的是「抽查即證明」的推理。 ## 驗證及來源綁定 7 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 2b3540b5dbb78a14560841645c8bd368269c59a972c859b94548f2dadb8878eb - original source SHA-256: 2b3540b5dbb78a14560841645c8bd368269c59a972c859b94548f2dadb8878eb - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-two-sided-ideal-01.json)