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

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

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

Substeps and lemmas

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

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 subgroup

One 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 isomorphism

Another 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 pair

Consider 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)