# Subgroups and homomorphisms: auditing on the complete tables of ℤ/4 and ℤ/2

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-subgroup-homomorphism/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

G={0,1,2,3} with operation (a+b) mod 4 and K={0,1} with operation (a+b) mod 2 are given by complete Cayley tables. (1) Prove that H={0,2} is a subgroup of G and H'={0,1} is not; (2) prove that the mapping table f(0)=0, f(1)=1, f(2)=0, f(3)=1 is a homomorphism G→K, covering all 16 input pairs; (3) find the kernel and the image, and show that f is surjective but not injective, hence not an isomorphism; (4) show that the constant map h≡1 is not a homomorphism.

Treats only the two given finite groups and mapping tables (MKO assumption a1); conclusions concern these two specified finite groups only, are not extended to arbitrary groups, and do not treat homomorphisms as isomorphisms (MKO assumption a2). That G and K are groups is a given premise (checkable exhaustively as in mko-finite-group). Cosets, normal subgroups and the isomorphism theorems are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- division_algorithm
- function_def
- injective_surjective_def
- numeric_evaluation


- G1 — Source group G={0,1,2,3}; row a of its Cayley table lists a*0, a*1, a*2, a*3: 0,1,2,3; 1,2,3,0; 2,3,0,1; 3,0,1,2, that is a*b=(a+b) mod 4; the identity is 0. (G,*) is a finite group.
- G2 — Target group K={0,1}; its Cayley table has rows 0,1 and 1,0, that is a⊕b=(a+b) mod 2; the identity is 0. (K,⊕) is a finite group.
- G3 — Mapping tables: f(0)=0, f(1)=1, f(2)=0, f(3)=1; h(0)=h(1)=h(2)=h(3)=1.
- G4 — Candidate subsets H={0,2} and H'={0,1}.


- G=\{0,1,2,3\},\ a*b=(a+b)\bmod 4 — the source group
- K=\{0,1\},\ a\oplus b=(a+b)\bmod 2 — the target group
- H,\ H' — the two candidate subsets
- f,\ h — the two candidate maps
- \ker f,\ \operatorname{im} f — the kernel and the image





## Rules and sources


- division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
- function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
- injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- group_axioms · prerequisite — Group axioms: a set G with a binary operation that is associative, has an identity e (eg=ge=g), and in which every g has an inverse g⁻¹ (gg⁻¹=g⁻¹g=e).
- subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
- eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
- mko_subhom_def · cited — A nonempty subset H of a finite group G is a subgroup if it is closed under the operation, contains the identity and is closed under inverses. A homomorphism f:G→K satisfies f(a*b)=f(a)*f(b). A homomorphism is not automatically injective. · mko-subgroup-homomorphism
- mod_notation · prerequisite — For an integer x and a positive integer m, x mod m denotes the remainder r of the division algorithm: the unique r with 0≤r<m and x=mq+r for some integer q.
- finite_exhaustion · prerequisite — On a finite set, a statement about all elements (or all ordered pairs) holds exactly when it holds in each listed case; checking every case is a complete proof for that finite model, but says nothing about other sets.
- kernel_image_def · prerequisite — For f:G→K, ker f={a∈G ∣ f(a)=e_K} (the source elements sent to the target identity) and im f={f(a) ∣ a∈G} (all mapped values).
- L_same_rem · lemma — Let m be a positive integer and x, y integers. If x−y=mk for an integer k, then x mod m=y mod m.





## Main derivation

S01 · definitionBefore

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

After

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

Conditions: none

Rule: mko_subhom_def · Uses: mko_subhom_def, G1, G2

Leaf basis: mko_subhom_def + group_axioms

By the MKO a subgroup needs four checks: nonempty, closed, contains the identity, closed under inverses; a homomorphism must satisfy f(a*b)=f(a)⊕f(b) for every input pair. The MKO also warns that a homomorphism is not automatically injective.



S02 · impliesBefore

H=\{0,2\}

After

H\neq\varnothing,\ H\subseteq G

Conditions: none

Rule: subset_def · Uses: G1, G4

Leaf basis: subset_def

H contains 0, so it is nonempty; both of its elements 0 and 2 lie in G, so H⊆G.



S03 · impliesBefore

a,b\in H

After

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

Conditions: none

Rule: finite_exhaustion · Uses: G1, S02

Leaf basis: finite_exhaustion + numeric_evaluation

H has 2²=4 ordered pairs; reading G's table: 0*0=0, 0*2=2, 2*0=2 and 2*2=(2+2) mod 4=0. All four outputs lie in H, so H is closed.



S04 · impliesBefore

e_G=0

After

e_G\in H

Conditions: none

Rule: set_builder · Uses: G1, S02

Leaf basis: group_axioms + set_builder

The identity of G is 0 (row 0 and column 0 of the table are both 0,1,2,3), and 0∈H.



S05 · impliesBefore

a\in H

After

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

Conditions: none

Rule: finite_exhaustion · Uses: G1, S04

Leaf basis: finite_exhaustion + group_axioms

0*0=0, so the inverse of 0 is 0; 2*2=0 on both sides, so the two-sided inverse of 2 is 2. Both inverses lie in H.



S06 · impliesBefore

\text{nonempty, closed, identity, inverses}

After

H\ \text{is a subgroup of } G

Conditions: none

Rule: mko_subhom_def · Uses: S02, S03, S04, S05

Leaf basis: mko_subhom_def + and_intro_elim

The four conditions come from S02 to S05, so by the MKO's definition H is a subgroup of G.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: mko_subhom_def · Uses: G1, G4

Leaf basis: mko_subhom_def + quantifier_negation + numeric_evaluation

H' is nonempty and contains the identity 0, but 1*1=(1+1) mod 4=2 is not in H', so closure fails and H' is not a subgroup. Moreover the inverse of 1 is 3, which is not in H' either.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: function_def · Uses: G3, G2, mod_notation

Leaf basis: function_def + finite_exhaustion + mod_notation

The mapping table assigns exactly one value in K to each element of G, so f is a function G→K. Comparing the four cells: the remainders of 0, 1, 2, 3 on division by 2 are 0, 1, 0, 1, so f(a)=a mod 2.



S09 · impliesBefore

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

After

x\bmod m=y\bmod m

Conditions: m>0

Rule: L_same_rem · Uses: division_algorithm, mod_notation

Leaf basis: division_algorithm + mod_notation

The homomorphism argument needs Lemma L_same_rem: two integers that differ by an integer multiple of m leave the same remainder on division by m. The proof is in S09.1 and S09.2 and uses only existence and uniqueness in the division algorithm.



S10 · equivalentBefore

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

After

(a+b)\bmod 2

Conditions: a,b\in G

Rule: L_same_rem · Uses: S08, S09, G1, division_algorithm

Leaf basis: L_same_rem + division_algorithm + divides_def + eq_replace

Write a+b=4q+s with s=(a+b) mod 4. Then s−(a+b)=−4q=2·(−2q) is an integer multiple of 2, so by the lemma (m=2), s mod 2=(a+b) mod 2. Here a and b are arbitrary elements of G.



S11 · equivalentBefore

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

After

(a+b)\bmod 2

Conditions: a,b\in G

Rule: L_same_rem · Uses: S08, S09, G2, division_algorithm

Leaf basis: L_same_rem + division_algorithm + eq_replace

Write a=2p+r₁ and b=2p'+r₂ (r₁=a mod 2, r₂=b mod 2). Then (r₁+r₂)−(a+b)=−2(p+p') is a multiple of 2, so by the lemma (r₁+r₂) mod 2=(a+b) mod 2.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: eq_refl_symm_trans · Uses: S10, S11

Leaf basis: eq_refl_symm_trans + forall_intro

Both sides equal (a+b) mod 2, so they are equal by transitivity. S10 and S11 hold for arbitrary a, b, so all 4²=16 input pairs are covered (MKO paragraph 2). N5 separately enumerates the 16 pairs as a cross-check. f is a homomorphism.



S13 · equivalentBefore

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

After

\{0,2\}=H

Conditions: none

Rule: kernel_image_def · Uses: S08, G2, kernel_image_def

Leaf basis: kernel_image_def + set_builder + finite_exhaustion

The target identity is 0. Checking each element: f(0)=0, f(1)=1, f(2)=0, f(3)=1, so ker f={0,2}, which is exactly the subgroup H of S06.



S14 · impliesBefore

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

After

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

Conditions: none

Rule: injective_surjective_def · Uses: S08, S13, kernel_image_def

Leaf basis: injective_surjective_def + kernel_image_def + finite_counting_basics

The image, all mapped values, is {0,1}=K, so f is surjective. But f(0)=f(2)=0 with 0≠2, so f is not injective; the kernel containing more than the identity reflects this. |im f|=2<4=|G|, and the MKO's third paragraph says injectivity is possible only when the image is as large as the source. f is not a bijection, hence not an isomorphism.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: quantifier_negation · Uses: G3, G1, G2

Leaf basis: quantifier_negation + numeric_evaluation

h(0*0)=h(0)=1, but h(0)⊕h(0)=1⊕1=(1+1) mod 2=0. Since 1≠0, the homomorphism condition fails at (0,0); by quantifier negation h is not a homomorphism. One failing pair suffices to reject, whereas establishing a homomorphism requires an argument covering all 16 pairs.



S16 · impliesBefore

H,\ H',\ f,\ h

After

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

Conditions: none

Rule: and_intro_elim · Uses: S06, S07, S12, S13, S14, S15

Leaf basis: and_intro_elim

Combine all conclusions; they concern only the two specified finite groups G and K.







## Substeps and lemmas

S09.1 · theorem_applicationBefore

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

After

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

Conditions: m>0

Rule: division_algorithm · Uses: division_algorithm, mod_notation

Leaf basis: division_algorithm + mod_notation

Apply the division algorithm to x and the positive integer m: there are integers q, r with x=mq+r and 0≤r<m; by the notation r=x mod m.



S09.2 · impliesBefore

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

After

y\bmod m=r=x\bmod m

Conditions: q-k\in\mathbb{Z}

Rule: division_algorithm · Uses: S09.1, division_algorithm

Leaf basis: division_algorithm + distributive + eq_replace

y=x−mk=m(q−k)+r with q−k an integer and 0≤r<m, so (q−k, r) is exactly the quotient and remainder of y on division by m; by uniqueness, y mod m=r=x mod m. S09.1 and S09.2 together prove Lemma L_same_rem.







## Reverse audits


- S16 · sufficient_goal_reduction · S06, S07, S12, S13, S14, S15, and_intro_elim — Goal: all decisions. Sufficient condition: the conclusions proved in the listed steps, which give the goal by conjunction introduction; the goal is never used as a premise.
- S15 · sufficient_goal_reduction · G3, quantifier_negation, mko_subhom_def — Goal: h is not a homomorphism. Sufficient condition: one input pair violates the condition, which gives the goal by the definition. That pair is read directly from the tables; the goal is never used as a premise.
- S14 · premise_audit · injective_surjective_def, kernel_image_def, numeric_evaluation — Refuting injectivity needs one pair of distinct elements with the same image; surjectivity needs every element of K to be hit; both are checked explicitly.
- S13 · inverse_equivalence · kernel_image_def, set_builder, finite_exhaustion — All four elements are tested, and set-builder membership is two-way.
- S12 · premise_audit · S10, S11, eq_refl_symm_trans, forall_intro — ∀-introduction needs a, b to carry no special values, and in S10 and S11 they carry none; this is not sampling.
- S11 · inverse_equivalence · L_same_rem, eq_replace — As in S10, this replaces equals by equals and holds both ways.
- S10 · inverse_equivalence · L_same_rem, eq_replace — Both sides are the same integer, so replacing equals works both ways. The key fact is that 2 divides 4.
- S09.2 · premise_audit · S09.1, division_algorithm, distributive — The key is uniqueness in the division algorithm.
- S09.1 · premise_audit · division_algorithm, mod_notation — The division algorithm needs a positive divisor.
- S09 · premise_audit · L_same_rem — It needs m>0 and an integer k; only this direction is claimed.
- S08 · premise_audit · function_def, mod_notation, finite_exhaustion — The formula is another description of the mapping table, resting on all four cells matching; it holds for this table only.
- S07 · sufficient_goal_reduction · G1, mko_subhom_def, numeric_evaluation — Goal: H' is not a subgroup. Sufficient condition: one condition fails; a single product outside H' suffices. Containing the identity does not rescue it.
- S06 · sufficient_goal_reduction · S02, S03, S04, S05, mko_subhom_def — Goal: H is a subgroup. Sufficient condition: the four conditions together, which give the goal by the definition. All four are proved forwards from the table; the goal is never used as a premise.
- S05 · premise_audit · G1, finite_exhaustion, group_axioms — Inverses are taken in G and then tested for membership in H; both elements of H are checked.
- S04 · premise_audit · G1, G4 — It must be the identity of G that lies in H, not some element H picks for itself.
- S03 · premise_audit · G1, finite_exhaustion — All 4 ordered pairs are checked; closure is only one of the four conditions, and S04 and S05 check the rest.
- S02 · premise_audit · subset_def, G4 — Both elements are checked; the operation plays no role here.
- S01 · premise_audit · mko_subhom_def, G1, G2 — This step only lists the conditions to check and derives no new fact.





## Error controls and negative controls

Checking closure alone does not define a subgroupOne mistake the MKO names is calling a set a subgroup after checking closure only. The empty set is (vacuously) closed but contains no identity; in the infinite group (ℤ,+) the natural numbers ℕ are closed and contain 0, but 1 has no inverse in ℕ. For finite groups a nonempty closed subset is in fact a subgroup (a standard theorem, neither proved nor used here); this guide checks all four conditions as the MKO prescribes.

A homomorphism need not be injective or an isomorphismAnother mistake identified in the MKO is treating every homomorphism as injective or an isomorphism. f is a homomorphism, but f(0)=f(2) and the kernel {0,2} contains more than the identity; since |G|=4≠2=|K| there is no bijection between them at all.

A homomorphism proof must cover every input pairConsider h'(0)=0, h'(1)=1, h'(2)=1, h'(3)=0. Every input pair containing 0 passes (h'(0)=0 is the target identity), but h'(1*1)=h'(2)=1 while h'(1)⊕h'(1)=0. Sampling only pairs containing the identity would misjudge it. This guide covers the 16 pairs of f with S10 to S12, valid for arbitrary a, b, and cross-checks by enumeration in N5.


- H'={0,1} contains the identity 0, so it is a subgroup → reject — 1*1=2∉H', so closure fails; the inverse 3 of 1 is not in H' either.
- f is a homomorphism, so f is injective → reject — f(0)=f(2)=0 although 0≠2.
- f is an isomorphism G≅K → reject — |G|=4≠2=|K|, so there is no bijection.
- h' (0↦0, 1↦1, 2↦1, 3↦0) is a homomorphism because h'(0*a)=h'(0)⊕h'(a) for every a → reject — h'(1*1)=h'(2)=1 while h'(1)⊕h'(1)=0.
- The constant map h≡1 is a homomorphism → reject — h(0*0)=1≠0=h(0)⊕h(0).





## Result and limitations

H={0,2} is nonempty, closed, contains the identity 0 and is closed under inverses, so it is a subgroup of G; H'={0,1} is not, since 1*1=2∉H'. f(a)=a mod 2 satisfies f(a*b)=f(a)⊕f(b) for all 16 input pairs, so it is a homomorphism; ker f={0,2}=H and im f={0,1}=K; f is surjective but, since f(0)=f(2), not injective and not an isomorphism. The constant map h≡1 violates the homomorphism condition at (0,0).


- That G and K are groups is a premise (G1, G2); their group axioms are not re-checked here. The conclusions concern only these two specified finite groups (MKO assumption a2). Cosets, normal subgroups, quotient groups and the isomorphism theorems (the MKO's formal next) are not treated.
- N5 is a finite enumeration of all 16 input pairs, a complete cross-check for this model; it relies on the formula f(a)=a mod 2 of S08 reproducing the mapping table, and the argument of S10 to S12 does not depend on it.





## Verification and source binding

11 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-subgroup-homomorphism-01.json)