# C₄到C₂的kernel、fibers與單射性

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

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

derivation-mko-finite-group-homomorphism-kernel-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

f:C₄→C₂，f(a)=a mod2的kernel為{0,2}且正規；fibers是其cosets，f非單射。

兩完整加法群表與完整total homomorphism；不提前建商或第一同構。





## 已知條件與符號


- calc


- G1 — G={0,1,2,3}採模4加法，Q={0,1}採模2加法；f表依序[0,1,0,1]。


- K — 來源kernel子群
- f — 完整total homomorphism





## 規則與來源


- calc · prerequisite — 假設精確整數模算術與有限群、同態、preimage定義；本例群運算用加法記號。
- mko_definition · cited — 來源群與目標群都須由完整Cayley table認證，f須是complete total map並逐對滿足f(xy)=f(x)f(y)。kernel是目標identity的完整preimage，需直接驗subgroup與對所有g,k的gkg^{-1} closure。對任意a,b，f(a)=f(b)恰當a^{-1}b∈ker f，因此nonempty fibers是kernel cosets。kernel只含來源identity恰當f injective。非同態不得套kernel-normality；本節點不提前宣稱quotient或第一同構定理。 · mko-finite-group-homomorphism-kernel





## 逐步主鏈

S01 · implies操作前

G=C_4,\quad Q=C_2

操作後

\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|cc}+&0&1\\\hline 0&0&1\\1&1&0\\\end{array}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

兩個完整群表共20格。加法結合律由整數取餘下降，identity均0；G逆元表0,3,2,1，Q逆元0,1，皆兩側驗。



S02 · implies操作前

f:G\to Q

操作後

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

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

四個來源各有一個合法目標值，故total map。



S03 · implies操作前

f((a+b)\bmod4)=((a+b)\bmod4)\bmod2

操作後

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

條件：無

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

葉節點依據：calc

完整16格左右共用此值；因4是2倍數，先mod4不改parity，所以每對皆保群運算。



S04 · implies操作前

K=f^{-1}(\{0_Q\})

操作後

K=\{0,2\}

條件：無

規則：mko_definition · 依賴：G1, S02, S03

葉節點依據：mko_definition

完整mapping表中恰0與2送到目標identity0。



S05 · implies操作前

K=\{0,2\}

操作後

0\in K;\quad0+0=0,0+2=2,2+0=2,2+2=0;\quad-0=0,-2=2\ (\bmod4)

條件：無

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

葉節點依據：calc

全部四積與兩逆元都在K，直接認證子群。



S06 · implies操作前

g=0,1,2,3,\quad k=0,2

操作後

\begin{array}{c|cc}g+k-g&0&2\\\hline0&0&2\\1&0&2\\2&0&2\\3&0&2\end{array}

條件：無

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

葉節點依據：calc

完整8格共軛都等k，因此K正規，未只因命名kernel就跳過。



S07 · equivalent操作前

f^{-1}(0)=\{0,2\},\quad f^{-1}(1)=\{1,3\}

操作後

f(a)=f(b)\iff b-a\in K;\quad f^{-1}(0)=0+K,\ f^{-1}(1)=1+K

條件：無

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

葉節點依據：calc

兩fiber完整覆蓋G；同parity恰當差是偶類，直接證fiber-coset等價。



S08 · implies操作前

0\ne2,\quad f(0)=f(2)=0

操作後

f\text{ not injective},\quad K\ne\{0\}

條件：無

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

葉節點依據：calc

明示collision與nontrivial kernel相符，否證單射。



S09 · implies操作前

f(a)=f(b)\iff b-a\in K

操作後

K=\{0\}\iff f\text{ injective}

條件：無

規則：mko_definition · 依賴：G1, S03, S04, S07, S08

葉節點依據：mko_definition

若K只有0，等像迫a=b；若f單射，f(k)=f(0)=0迫k=0。兩方向清楚。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S09 · premise_audit · G1, S03, S04, S07, S08 — 此條件等價與本例都非的結果一致，未提前聲稱商同構。
- S08 · premise_audit · G1, S02, S04, S07 — 一個collision足夠否證，不能因f命中全部Q就稱單射。
- S07 · inverse_equivalence · G1, S01, S04, S06 — 加法式b−a對應乘法式a⁻¹b，必用來源同一運算。
- S06 · premise_audit · G1, S01, S03, S05 — normality使用已核homomorphism模型；任意map的identity preimage未必子群。
- S05 · premise_audit · G1, S01, S04 — 加法記號的inverse是負號mod4，不是有理倒數。
- S04 · premise_audit · G1, S02, S03 — kernel元素在來源G，不是目標中的值0、1。
- S03 · premise_audit · G1, S01, S02 — 不是只核generators；完整公式與16格同時覆蓋全部。
- S02 · premise_audit · G1, S01 — total map尚非homomorphism，保乘法責任留下一步。
- S01 · premise_audit · G1 — 父群資格先完成，不能只給f陣列便套kernel定理。





## 錯誤控制與反例

目標identitykernel取目標0的完整preimage，不是來源0的單一名稱。

先同態全部16對保群運算後才使用kernel結論。


- 任意total map的identity preimage都正規。 → reject — C₄→C₂的g=[0,0,1,1]有preimage{0,1}，1+1=2不在內，且不保運算。
- K={0}。 → reject — f(2)=0亦在kernel。
- f滿射所以單射。 → reject — f(0)=f(2)，來源有collision。





## 結論與限制

f:C₄→C₂，f(a)=a mod2的kernel為{0,2}且正規；fibers是其cosets，f非單射。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bcd46de77dc90f619f8492cc26c9e5e506e7f2107662144b4c6d8ff101c244b0
- original source SHA-256: bcd46de77dc90f619f8492cc26c9e5e506e7f2107662144b4c6d8ff101c244b0
- 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-group-homomorphism-kernel-01.json)