# 非滿射同態的正確image同構

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

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

derivation-mko-first-isomorphism-theorem-finite-groups-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

f:C₄→C₄,f(a)=2a mod4給C₄/{0,2}≅{0,2}，不是整個codomain C₄。

完整finite homomorphism、kernel、image、quotient及induced map，全代表核對。





## 已知條件與符號


- calc


- G1 — G=Q=C₄，兩者皆採下列完整模4加法表；f(0)=0,f(1)=2,f(2)=0,f(3)=2。


- K,I — 來源kernel與目標image
- \bar f — 由coset到image的映射





## 規則與來源


- calc · prerequisite — 假設精確模4算術與群、同態、商coset、同構的定義；加法記號。
- mko_definition · cited — 來源與目標均須以完整Cayley table認證，f為complete total homomorphism；kernel、image與quotient cosets先完整建立。誘導映射bar f(g ker f)=f(g)必須對每個coset的所有representatives給同值，並完整驗乘法保存、injective與surjective-to-image。若f不surjective，結論仍僅為G/ker f≅im f，不得把image換成整個codomain。有限枚舉只證指定模型；非同態不得套用定理。 · mko-first-isomorphism-theorem-finite-groups





## 逐步主鏈

S01 · implies操作前

G=Q=C_4

操作後

\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}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

來源與目標是同一完整四元素群模型，各有此16格表；結合律由整數下降，identity0、逆元0,3,2,1全部核。



S02 · implies操作前

f:G\to Q

操作後

(f(0),f(1),f(2),f(3))=(0,2,0,2)

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

完整total map的四個值都屬Q。



S03 · implies操作前

f((a+b)\bmod4)\equiv2(a+b)\pmod4

操作後

\begin{array}{c|cccc}f(a+b)&0&1&2&3\\\hline 0&0&2&0&2\\1&2&0&2&0\\2&0&2&0&2\\3&2&0&2&0\\\end{array}\quad=f(a)+f(b)\ (\bmod4)

條件：無

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

葉節點依據：calc

全部16pairs由分配律與取餘保持同值，完整驗同態。



S04 · implies操作前

K=f^{-1}(0),\quad I=f(G)

操作後

K=\{0,2\},\quad I=\{0,2\};\quad0+0=0,0+2=2,2+0=2,2+2=0\ (\bmod4)

條件：無

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

葉節點依據：calc

完整preimage與image皆明列；四乘積與逆元0,2給子群，g+k−g=k對所有g證K正規。



S05 · implies操作前

A=0+K=2+K,\quad B=1+K=3+K

操作後

A=\{0,2\},\quad B=\{1,3\},\quad A\sqcup B=G

條件：無

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

葉節點依據：calc

全部四cosets去重成完整兩類partition。



S06 · implies操作前

a,b=0,1,2,3

操作後

\begin{array}{c|cccc}(a+b)+K&0&1&2&3\\\hline 0&A&B&A&B\\1&B&A&B&A\\2&A&B&A&B\\3&B&A&B&A\\\end{array}\qquad\begin{array}{c|cc}+&A&B\\\hline A&A&B\\B&B&A\\\end{array}

條件：無

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

葉節點依據：calc

完整16格代表pair類指標在四個2×2區塊各常值，證商加法良定並得到全部四格商表。



S07 · implies操作前

\bar f(a+K)=f(a)

操作後

f(0)=f(2)=0\Rightarrow\bar f(A)=0;\quad f(1)=f(3)=2\Rightarrow\bar f(B)=2

條件：無

規則：calc · 依賴：G1, S02, S05, S06

葉節點依據：calc

兩cosets全部代表值一致，先證induced map代表獨立。



S08 · implies操作前

A+A=A,A+B=B,B+A=B,B+B=A

操作後

0+0=0,0+2=2,2+0=2,2+2=0\ (\bmod4)

條件：無

規則：calc · 依賴：G1, S04, S06, S07

葉節點依據：calc

四個商product的像與I中product逐對相符，所以bar f是homomorphism。



S09 · implies操作前

\bar f(A)=0\ne2=\bar f(B)

操作後

\bar f\text{ injective and onto }I=\{0,2\}

條件：無

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

葉節點依據：calc

兩個來源像不同證injective，全部I元素皆命中證surjective-to-image。



S10 · implies操作前

\bar f:G/K\to I\text{ well-defined bijective homomorphism}

操作後

G/K\cong I\subsetneq Q

條件：無

規則：mko_definition · 依賴：G1, S06, S07, S08, S09

葉節點依據：mko_definition

完整良定、保群運算與雙射三責任成立，認證指定模型第一同構結論。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S10 · premise_audit · G1, S06, S07, S08, S09 — 此finite certificate不取代一般抽象證明；也不把proper image偷換整個Q。
- S09 · premise_audit · G1, S04, S07 — 未命中codomain的1、3，因此不能寫surjective onto Q。
- S08 · premise_audit · G1, S04, S06, S07 — 兩邊使用不同載體但對應相同四格，不能只以大小2推同構。
- S07 · premise_audit · G1, S02, S05, S06 — 不能只選0、1然後忽略2、3，四個代表皆已核。
- S06 · premise_audit · G1, S01, S04, S05 — 由父結合律下降，加上identity A、inverse A與B各自身，商群資格完整。
- S05 · premise_audit · G1, S01, S04 — 商元素是sets A、B，非某一唯一代表0、1。
- S04 · premise_audit · G1, S01, S02, S03 — K位於來源，I位於目標，即使數字集合相同仍有不同角色。
- S03 · premise_audit · G1, S01, S02 — 不能只看cardinality或f(0)=0便稱同態。
- S02 · premise_audit · G1, S01 — Q含1、3但f不一定命中，保留image與codomain界線。
- S01 · premise_audit · G1 — 相同模型不等於f恒等，f仍需獨立檢查。





## 錯誤控制與反例

image界線結論只到I={0,2}，f不滿射時不可換Q。

代表先核先查A的0、2及B的1、3，再談induced map。


- G/K≅Q因f是同態。 → reject — G/K有2元素而Q有4，f未滿射。
- 只看|G/K|=|I|便證同構。 → reject — 需實際bar f並驗全部product與代表獨立；數目不提供運算證書。
- bar f(B)可依代表1或3取不同值。 → reject — f(1)=f(3)=2，良定性要求同值。





## 結論與限制

f:C₄→C₄,f(a)=2a mod4給C₄/{0,2}≅{0,2}，不是整個codomain C₄。







## 驗證及來源綁定

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


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

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