非滿射同態的正確image同構

目標與範圍

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

逐步主鏈

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}

f:G\to Q

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

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)

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)

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

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

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}

\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

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)

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

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

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

G/K\cong I\subsetneq Q

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）