# Z/4Z 對偶數理想取商

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-quotient-ring/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-finite-quotient-ring-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

I={0,2}為proper雙邊理想，R/I有兩個cosets及良定雙表。

完整四元素父環與二元素商環，不把任意proper理想商都稱域。





## 已知條件與符號


- calc


- G1 — R=Z/4Z，I={0,2}；父環運算為模4加乘。


- R — 模4父環
- I — 偶數理想
- E,O — 完整加法cosets





## 規則與來源


- calc · prerequisite — 假設整數同餘與環法則；理想需加法子群及左右吸收。
- mko_definition · cited — a約b iff a-b屬I。classes為加法cosets；[a]+[b]=[a+b]、[a][b]=[ab]。完整核代表元獨立。本專案含一環要求1不等於0，因此排除I=R的退化zero ring。 · mko-finite-quotient-ring





## 逐步主鏈

S01 · implies操作前

R=\{0,1,2,3\}

操作後

\begin{array}{c|cccc}+&0&1&2&3\\\hline 0&0&1&2&3\\1&1&2&3&0\\2&2&3&0&1\\3&3&0&1&2\\\end{array}\qquad\begin{array}{c|cccc}*&0&1&2&3\\\hline 0&0&0&0&0\\1&0&1&2&3\\2&0&2&0&2\\3&0&3&2&1\\\end{array}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

列出父環全部32格。整數環法則因模4同餘與加乘相容而下降。



S02 · implies操作前

I=\{0,2\}

操作後

0+0=0,\ 0+2=2,\ 2+0=2,\ 2+2=0;\quad -0=0,-2=2

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

列出I全部加法與逆元，證加法子群。



S03 · implies操作前

r\in R,\quad i\in I

操作後

r0=0r=0;\quad(0,1,2,3)2=(0,2,0,2)=2(0,1,2,3)

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

所有左右乘積落在I。1不在I，因此I是proper雙邊理想。



S04 · implies操作前

a\sim b\iff a-b\in I

操作後

E=0+I=2+I=\{0,2\},\quad O=1+I=3+I=\{1,3\}

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

同餘即同奇偶，完整列出全部cosets並去重。



S05 · implies操作前

a'=a+i,\quad b'=b+j,\quad i,j\in I

操作後

(a'+b')-(a+b)=i+j\in I

條件：無

規則：calc · 依賴：G1, S02, S04

葉節點依據：calc

換任意同類代表後，和只差理想元素，因此加法良定。



S06 · implies操作前

a'=a+i,\quad b'=b+j

操作後

a'b'-ab=aj+ib+ij\in I

條件：無

規則：calc · 依賴：G1, S02, S03, S04

葉節點依據：calc

左右吸收與加法封閉使三項全在I，證乘法對所有代表元良定。



S07 · implies操作前

R/I=\{E,O\}

操作後

\begin{array}{c|cc}+&E&O\\\hline E&E&O\\O&O&E\\\end{array}\qquad\begin{array}{c|cc}*&E&O\\\hline E&E&E\\O&E&O\\\end{array}

條件：無

規則：calc · 依賴：G1, S01, S04, S05, S06

葉節點依據：calc

以完整父表計每對類的結果；前兩步證所有代表替換均保持此類。



S08 · implies操作前

0+I=E,\quad1+I=O

操作後

E\ne O,\quad R/I\text{ is a unital quotient ring}

條件：無

規則：mko_definition · 依賴：G1, S03, S05, S06, S07

葉節點依據：mko_definition

1不在I給商中1≠0；環恆等式由良定商運算繼承。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S03, S05, S06, S07 — 若I=R只剩一類且1=0，會違反本專案含一環慣例。
- S07 · premise_audit · G1, S01, S04, S05, S06 — 商表各有四格，E是零類，O是一類。
- S06 · premise_audit · G1, S02, S03, S04 — 非交換父環也須保留乘積順序aj、ib；此例父環雖交換仍不能略理想條件。
- S05 · premise_audit · G1, S02, S04 — i、j可取I全部元素，不只固定一組代表。
- S04 · premise_audit · G1, S03 — E與O互斥且聯集是R，商元素不是單一0或1。
- S03 · premise_audit · G1, S01, S02 — 左右兩邊皆核；不能僅由I大小就判為理想。
- S02 · premise_audit · G1, S01 — 元素2的逆元仍在I；非空與加法封閉均已核。
- S01 · premise_audit · G1 — 加法零0與乘法一1不同；不能只保留商表來取代父環。





## 錯誤控制與反例

理想先行先核加法子群與雙邊吸收，再定義商乘法。

代表替換a'b'−ab三項均須落I；只核0、1代表的四格不夠。


- R/I={0,1}作為父環子集。 → reject — 載體是E、O兩個coset集合；0、1只是可選代表。
- I=R也符合本專案1≠0要求。 → reject — 此時0+I=1+I=R。
- proper理想的商必為域。 → reject — Z/4Z的零理想proper，但商仍有非零2且2²=0。





## 結論與限制

I={0,2}為proper雙邊理想，R/I有兩個cosets及良定雙表。







## 驗證及來源綁定

1 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: c45f9867151cba8da988134e5c080121c96a4971332e3fd16a292f9facd2df8b
- original source SHA-256: c45f9867151cba8da988134e5c080121c96a4971332e3fd16a292f9facd2df8b
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-finite-quotient-ring-01.json)