# 子群與群同態：在 ℤ/4 與 ℤ/2 的完整表上核對

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

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

derivation-mko-subgroup-homomorphism-01 · production-20261019-adopted-96



## 目標與範圍

G={0,1,2,3} 以 (a+b) mod 4 為運算，K={0,1} 以 (a+b) mod 2 為運算，兩者都給出完整 Cayley 表。（一）證明 H={0,2} 是 G 的子群，H'={0,1} 不是；（二）證明映射表 f(0)=0、f(1)=1、f(2)=0、f(3)=1 是同態 G→K（涵蓋全部 16 個輸入對）；（三）求 kernel 與 image，說明 f 滿射但不單射，因此不是同構；（四）說明常數映射 h≡1 不是同態。

只處理題目給定的兩個有限群與映射表（MKO 假設 a1）；結論只屬於這兩個指定的有限群，不外推到任意群，也不把同態當同構（MKO 假設 a2）。G 與 K 是群作為已知前提（可依 mko-finite-group 的方法窮舉核對）。不處理陪集、正規子群或同構定理；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- division_algorithm
- function_def
- injective_surjective_def
- numeric_evaluation


- G1 — 來源群 G={0,1,2,3}，Cayley 表的第 a 行（row）依序為 a*0、a*1、a*2、a*3：0,1,2,3；1,2,3,0；2,3,0,1；3,0,1,2，即 a*b=(a+b) mod 4；單位元為 0。(G,*) 是有限群。
- G2 — 目標群 K={0,1}，Cayley 表兩行（row）為 0,1；1,0，即 a⊕b=(a+b) mod 2；單位元為 0。(K,⊕) 是有限群。
- G3 — 映射表：f(0)=0，f(1)=1，f(2)=0，f(3)=1；h(0)=h(1)=h(2)=h(3)=1。
- G4 — 候選子集 H={0,2} 與 H'={0,1}。


- G=\{0,1,2,3\},\ a*b=(a+b)\bmod 4 — 來源群
- K=\{0,1\},\ a\oplus b=(a+b)\bmod 2 — 目標群
- H,\ H' — 兩個候選子集
- f,\ h — 兩個候選映射
- \ker f,\ \operatorname{im} f — 核與像





## 規則與來源


- division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- group_axioms · prerequisite — 群公理：集合 G 配二元運算，滿足結合律、有單位元 e（eg=ge=g）、每個元素 g 有反元素 g⁻¹（gg⁻¹=g⁻¹g=e）。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- 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)。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- mko_subhom_def · cited — 有限群 G 的非空子集 H 若對運算封閉、含單位元且對逆元封閉，則為子群。群同態 f:G→K 滿足 f(a*b)=f(a)*f(b)；同態不自動為單射。 · mko-subgroup-homomorphism
- mod_notation · prerequisite — 對整數 x 與正整數 m，x mod m 表示除法演算法中的餘數 r：唯一滿足 0≤r<m 且 x=mq+r（q 為整數）的 r。
- finite_exhaustion · prerequisite — 在有限集合上，對全部元素（或全部有序對）的命題成立，當且僅當它在列出的每一個情形都成立；逐一核完是該有限模型的完整證明，但不推及其他集合。
- kernel_image_def · prerequisite — 對 f:G→K，ker f={a∈G ∣ f(a)=e_K}（映到目標單位元的來源元素），im f={f(a) ∣ a∈G}（所有映射值）。
- L_same_rem · lemma — 設 m 為正整數、x、y 為整數。若 x−y=mk（k 為整數），則 x mod m=y mod m。





## 逐步主鏈

S01 · definition操作前

H\subseteq G,\ f:G\to K

操作後

H\neq\varnothing,\ HH\subseteq H,\ e\in H,\ H^{-1}\subseteq H;\ \forall a,b:\ f(a*b)=f(a)\oplus f(b)

條件：無

規則：mko_subhom_def · 依賴：mko_subhom_def, G1, G2

葉節點依據：mko_subhom_def + group_axioms

依 MKO，子群要核四件事：非空、封閉、含單位元、對逆元封閉；同態要對全部輸入對滿足 f(a*b)=f(a)⊕f(b)。MKO 也提醒同態不自動為單射。



S02 · implies操作前

H=\{0,2\}

操作後

H\neq\varnothing,\ H\subseteq G

條件：無

規則：subset_def · 依賴：G1, G4

葉節點依據：subset_def

H 含 0，所以非空；它的兩個元素 0、2 都在 G 中，所以 H⊆G。



S03 · implies操作前

a,b\in H

操作後

0*0=0,\ 0*2=2,\ 2*0=2,\ 2*2=0\ \in H

條件：無

規則：finite_exhaustion · 依賴：G1, S02

葉節點依據：finite_exhaustion + numeric_evaluation

H 有 2²=4 個有序對，查 G 的表：0*0=0，0*2=2，2*0=2，2*2=(2+2) mod 4=0。四個輸出都在 H，所以 H 封閉。



S04 · implies操作前

e_G=0

操作後

e_G\in H

條件：無

規則：set_builder · 依賴：G1, S02

葉節點依據：group_axioms + set_builder

G 的單位元是 0（表的第 0 行（row）與第 0 列（column）都是 0,1,2,3），而 0∈H。



S05 · implies操作前

a\in H

操作後

0^{-1}=0\in H,\ 2^{-1}=2\in H

條件：無

規則：finite_exhaustion · 依賴：G1, S04

葉節點依據：finite_exhaustion + group_axioms

0*0=0，所以 0 的逆元是 0；2*2=0 而且運算對稱位置相同，所以 2 的雙側逆元是 2。兩個逆元都在 H 中。



S06 · implies操作前

\text{nonempty, closed, identity, inverses}

操作後

H\ \text{is a subgroup of } G

條件：無

規則：mko_subhom_def · 依賴：S02, S03, S04, S05

葉節點依據：mko_subhom_def + and_intro_elim

四個條件分別由 S02 到 S05 給出，依 MKO 的定義 H 是 G 的子群。



S07 · implies操作前

H'=\{0,1\},\ 1*1

操作後

1*1=2\notin H'\ \Rightarrow\ H'\ \text{not a subgroup}

條件：無

規則：mko_subhom_def · 依賴：G1, G4

葉節點依據：mko_subhom_def + quantifier_negation + numeric_evaluation

H' 非空且含單位元 0，但 1*1=(1+1) mod 4=2 不在 H' 中，封閉失敗，所以 H' 不是子群。另外 1 的逆元是 3，也不在 H' 中。



S08 · implies操作前

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

操作後

f:G\to K,\ f(a)=a\bmod 2

條件：無

規則：function_def · 依賴：G3, G2, mod_notation

葉節點依據：function_def + finite_exhaustion + mod_notation

映射表對 G 的每個元素恰給一個 K 中的值，所以 f 是函數 G→K。四格逐一比對：0、1、2、3 除以 2 的餘數是 0、1、0、1，所以 f(a)=a mod 2。



S09 · implies操作前

x-y=mk,\ k\in\mathbb{Z}

操作後

x\bmod m=y\bmod m

條件：m>0

規則：L_same_rem · 依賴：division_algorithm, mod_notation

葉節點依據：division_algorithm + mod_notation

同態的論證需要引理 L_same_rem：相差 m 的整數倍的兩個整數，除以 m 的餘數相同。證明在 S09.1、S09.2，只用除法演算法的存在與唯一性。



S10 · equivalent操作前

f(a*b)=((a+b)\bmod 4)\bmod 2

操作後

(a+b)\bmod 2

條件：a,b\in G

規則：L_same_rem · 依賴：S08, S09, G1, division_algorithm

葉節點依據：L_same_rem + division_algorithm + divides_def + eq_replace

設 a+b=4q+s，s=(a+b) mod 4。則 s−(a+b)=−4q=2·(−2q) 是 2 的整數倍，依引理（m=2），s mod 2=(a+b) mod 2。a、b 是 G 中任意元素。



S11 · equivalent操作前

f(a)\oplus f(b)=(a\bmod 2+b\bmod 2)\bmod 2

操作後

(a+b)\bmod 2

條件：a,b\in G

規則：L_same_rem · 依賴：S08, S09, G2, division_algorithm

葉節點依據：L_same_rem + division_algorithm + eq_replace

設 a=2p+r₁、b=2p'+r₂（r₁=a mod 2、r₂=b mod 2）。則 (r₁+r₂)−(a+b)=−2(p+p') 是 2 的倍數，依引理 (r₁+r₂) mod 2=(a+b) mod 2。



S12 · implies操作前

f(a*b)=(a+b)\bmod 2=f(a)\oplus f(b)

操作後

\forall a,b\in G:\ f(a*b)=f(a)\oplus f(b)

條件：無

規則：eq_refl_symm_trans · 依賴：S10, S11

葉節點依據：eq_refl_symm_trans + forall_intro

兩邊都等於 (a+b) mod 2，依等號的傳遞相等。S10、S11 對任意 a、b 成立，所以涵蓋全部 4²=16 個輸入對（MKO 第二段）。N5 另外逐一窮舉 16 對作交叉核對。f 是同態。



S13 · equivalent操作前

\ker f=\{a\in G\mid f(a)=0\}

操作後

\{0,2\}=H

條件：無

規則：kernel_image_def · 依賴：S08, G2, kernel_image_def

葉節點依據：kernel_image_def + set_builder + finite_exhaustion

目標單位元是 0。逐一查：f(0)=0、f(1)=1、f(2)=0、f(3)=1，所以 ker f={0,2}，正是 S06 的子群 H。



S14 · implies操作前

\operatorname{im} f,\ f(0)=f(2)

操作後

\operatorname{im} f=\{0,1\}=K;\ f\ \text{surjective, not injective}

條件：無

規則：injective_surjective_def · 依賴：S08, S13, kernel_image_def

葉節點依據：injective_surjective_def + kernel_image_def + finite_counting_basics

像集是所有映射值 {0,1}=K，所以 f 滿射。但 f(0)=f(2)=0 而 0≠2，所以 f 不是單射；kernel 不只含單位元也反映了這點。|im f|=2<4=|G|，MKO 第三段說 image 大小等於來源大小才可能單射。f 不是雙射，因此不是同構。



S15 · implies操作前

h(0*0)\ \text{vs}\ h(0)\oplus h(0)

操作後

1\neq 0=1\oplus 1\ \Rightarrow\ h\ \text{not a homomorphism}

條件：無

規則：quantifier_negation · 依賴：G3, G1, G2

葉節點依據：quantifier_negation + numeric_evaluation

h(0*0)=h(0)=1，但 h(0)⊕h(0)=1⊕1=(1+1) mod 2=0。1≠0，同態條件在 (0,0) 失敗；依量詞否定，h 不是同態。一個失敗對就足以否定，但要肯定同態，論證必須涵蓋全部 16 對。



S16 · implies操作前

H,\ H',\ f,\ h

操作後

H\le G,\ H'\not\le G,\ f\ \text{hom.},\ \ker f=H,\ \operatorname{im} f=K,\ f\ \text{not injective},\ h\ \text{not hom.}

條件：無

規則：and_intro_elim · 依賴：S06, S07, S12, S13, S14, S15

葉節點依據：and_intro_elim

合併全部結論；它們只屬於 G 與 K 這兩個指定的有限群。







## 局部子步與引理

S09.1 · theorem_application操作前

x\in\mathbb{Z},\ m>0

操作後

x=mq+r,\ 0\le r<m,\ r=x\bmod m

條件：m>0

規則：division_algorithm · 依賴：division_algorithm, mod_notation

葉節點依據：division_algorithm + mod_notation

對 x 與正整數 m 使用除法演算法：有整數 q、r 使 x=mq+r 且 0≤r<m；依記號 r=x mod m。



S09.2 · implies操作前

y=x-mk=m(q-k)+r,\ 0\le r<m

操作後

y\bmod m=r=x\bmod m

條件：q-k\in\mathbb{Z}

規則：division_algorithm · 依賴：S09.1, division_algorithm

葉節點依據：division_algorithm + distributive + eq_replace

y=x−mk=m(q−k)+r，q−k 是整數且 0≤r<m，所以 (q−k, r) 正是 y 除以 m 的商與餘數；依唯一性，y mod m=r=x mod m。S09.1 與 S09.2 合起來證得引理 L_same_rem。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S06, S07, S12, S13, S14, S15, and_intro_elim — 目標：全部判定。足夠條件：各步已證結論；由合取引入推出目標，沒有把目標當作前提。
- S15 · sufficient_goal_reduction · G3, quantifier_negation, mko_subhom_def — 目標：h 不是同態。足夠條件：一個輸入對違反條件；由定義推出目標。此對由查表直接得到，沒有把目標當作前提。
- S14 · premise_audit · injective_surjective_def, kernel_image_def, numeric_evaluation — 否定單射只需一對不同元素有相同像；滿射需要 K 的每個元素都被取到，兩者都已逐一核對。
- S13 · inverse_equivalence · kernel_image_def, set_builder, finite_exhaustion — 四個元素逐一判定，集合建構記號的成員條件是雙向的。
- S12 · premise_audit · S10, S11, eq_refl_symm_trans, forall_intro — ∀ 引入要求 a、b 沒有被特別取值，S10、S11 確實沒有；這不是抽樣。
- S11 · inverse_equivalence · L_same_rem, eq_replace — 與 S10 相同，是相等式子的互換，雙向成立。
- S10 · inverse_equivalence · L_same_rem, eq_replace — 兩邊是同一個整數，相等式子互換，雙向成立。關鍵是 2 整除 4。
- S09.2 · premise_audit · S09.1, division_algorithm, distributive — 關鍵是除法演算法的唯一性。
- S09.1 · premise_audit · division_algorithm, mod_notation — 除法演算法要求除數為正整數。
- S09 · premise_audit · L_same_rem — 需要 m>0 與 k 為整數；只宣稱這個方向。
- S08 · premise_audit · function_def, mod_notation, finite_exhaustion — 公式只是映射表的另一種寫法，靠四格逐一相符；這只對這張表成立。
- S07 · sufficient_goal_reduction · G1, mko_subhom_def, numeric_evaluation — 目標：H' 不是子群。足夠條件：某個條件失敗；一個不在 H' 的乘積就夠了。含單位元並不能補救。
- S06 · sufficient_goal_reduction · S02, S03, S04, S05, mko_subhom_def — 目標 G：H 是子群。足夠條件：四個條件同時成立；由定義推出目標。四者都由表正向證成，沒有把目標當作前提。
- S05 · premise_audit · G1, finite_exhaustion, group_axioms — 逆元是在 G 中取的，然後檢查它是否落在 H；H 的兩個元素都查過。
- S04 · premise_audit · G1, G4 — 必須是 G 的單位元在 H 中，而不是 H 自己另選一個元素。
- S03 · premise_audit · G1, finite_exhaustion — 4 個有序對都查過；封閉只是四個條件之一，S04、S05 另外核。
- S02 · premise_audit · subset_def, G4 — 兩個元素逐一核對；這一步不涉及運算。
- S01 · premise_audit · mko_subhom_def, G1, G2 — 此步只列出要核的條件，不推出新事實。





## 錯誤控制與反例

只核閉合不等於子群MKO 指出的誤解之一是只核閉合就叫子群。空集合對運算（空泛地）封閉，卻不含單位元；在無限群 (ℤ,+) 中，自然數 ℕ 封閉且含 0，但 1 在 ℕ 中沒有逆元。對有限群，非空且封閉的子集其實必為子群（標準定理，本稿未證也未使用）；本稿依 MKO 逐一核四個條件。

同態不一定單射或同構MKO 的另一個誤解是把每個同態都當單射或同構。f 是同態，但 f(0)=f(2)，kernel={0,2} 不只含單位元；|G|=4≠2=|K|，兩者之間根本沒有雙射。

同態要核全部輸入對考慮 h'(0)=0、h'(1)=1、h'(2)=1、h'(3)=0。含 0 的輸入對都會通過（h'(0)=0 是目標單位元），但 h'(1*1)=h'(2)=1，而 h'(1)⊕h'(1)=0。只抽查含單位元的輸入對會誤判。本稿以對任意 a、b 成立的 S10 到 S12 涵蓋 f 的 16 對，並以 N5 窮舉交叉核對。


- H'={0,1} 含單位元 0，所以是子群 → reject — 1*1=2∉H'，封閉失敗；1 的逆元 3 也不在 H'。
- f 是同態，所以 f 是單射 → reject — f(0)=f(2)=0 而 0≠2。
- f 是同構 G≅K → reject — |G|=4≠2=|K|，沒有雙射。
- h'（0↦0、1↦1、2↦1、3↦0）是同態，因為對每個 a 都有 h'(0*a)=h'(0)⊕h'(a) → reject — h'(1*1)=h'(2)=1，而 h'(1)⊕h'(1)=0。
- 常數映射 h≡1 是同態 → reject — h(0*0)=1≠0=h(0)⊕h(0)。





## 結論與限制

H={0,2} 非空、封閉、含單位元 0 且對逆元封閉，是 G 的子群；H'={0,1} 因 1*1=2∉H' 不是子群。f(a)=a mod 2 對全部 16 個輸入對滿足 f(a*b)=f(a)⊕f(b)，是同態；ker f={0,2}=H，im f={0,1}=K，f 滿射但因 f(0)=f(2) 不是單射，也不是同構。常數映射 h≡1 在 (0,0) 違反同態條件。


- G 與 K 是群作為前提（G1、G2），本稿沒有重新核它們的群公理；結論只屬於這兩個指定的有限群（MKO 假設 a2）。不處理陪集、正規子群、商群與同構定理（MKO 的 formal next）。
- N5 是對全部 16 個輸入對的有限窮舉，對這個模型是完整的交叉核對；它依賴 S08 的公式 f(a)=a mod 2 重現映射表，S10 到 S12 的論證不依賴它。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: b770b6bc3f247912cf3bc8b6e85e939ce34d84eb71296cbfb81183aa78d3a291
- original source SHA-256: b770b6bc3f247912cf3bc8b6e85e939ce34d84eb71296cbfb81183aa78d3a291
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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