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

目標與範圍

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。

逐步主鏈

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)

H=\{0,2\}

H\neq\varnothing,\ H\subseteq G

a,b\in H

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

e_G=0

e_G\in H

a\in H

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

\text{nonempty, closed, identity, inverses}

H\ \text{is a subgroup of } G

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

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

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

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

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

x\bmod m=y\bmod m

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

(a+b)\bmod 2

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

(a+b)\bmod 2

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)

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

\{0,2\}=H

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

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

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

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

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

局部子步與引理

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

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

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

y\bmod m=r=x\bmod m

逐步反向審查

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