# Kernel, fibers and injectivity from C4 to C2

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

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-finite-group-homomorphism-kernel-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For f:C4 to C2, f(a)=a mod 2, the normal kernel is {0,2}; fibers are its cosets and f is not injective.

Two complete additive-group tables and a total homomorphism, without quotient or first-isomorphism construction.





## Givens and symbols


- calc


- G1 — G={0,1,2,3} under addition modulo 4, Q={0,1} under addition modulo 2; f's aligned table is [0,1,0,1].


- K — source kernel subgroup
- f — complete total homomorphism





## Rules and sources


- calc · prerequisite — Assume exact modular integer arithmetic and definitions of finite groups, homomorphisms and preimages; use additive notation here.
- mko_definition · cited — Both groups require complete Cayley-table qualification. f is a total mapping and must satisfy f(x*y)=f(x)*f(y) for every pair. Its kernel is the entire target-identity preimage, with subgroup and all-g conjugation closure checked directly. f(a)=f(b) exactly when a^(-1)*b belongs to the kernel, so each nonempty fiber is a kernel coset. The kernel is the source-identity singleton exactly when f is injective. Nonhomomorphisms cannot invoke these theorems; quotient/image isomorphism is not claimed here. · mko-finite-group-homomorphism-kernel





## Main derivation

S01 · impliesBefore

G=C_4,\quad Q=C_2

After

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

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The two full tables contain 20 entries. Integer associativity descends; both identities are 0, with full inverse lists 0,3,2,1 and 0,1, valid on both sides.



S02 · impliesBefore

f:G\to Q

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Each of the four source elements has one legal target value, making a total map.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

All 16 pairs have the displayed value on both sides; reducing modulo 4 preserves parity, so every pair respects the operation.



S04 · impliesBefore

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

After

K=\{0,2\}

Conditions: none

Rule: mko_definition · Uses: G1, S02, S03

Leaf basis: mko_definition

Exactly 0 and 2 map to target identity 0 in the complete mapping table.



S05 · impliesBefore

K=\{0,2\}

After

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

Conditions: none

Rule: calc · Uses: G1, S01, S04

Leaf basis: calc

All four sums and both inverses stay in K, directly qualifying the subgroup.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01, S03, S05

Leaf basis: calc

All eight conjugation entries equal k, directly proving normality rather than skipping it because of the name kernel.



S07 · equivalentBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01, S04, S06

Leaf basis: calc

The two fibers cover G; equal parity is exactly an even residue difference, directly proving the fiber/coset equivalence.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S02, S04, S07

Leaf basis: calc

The explicit collision agrees with a nontrivial kernel and refutes injectivity.



S09 · impliesBefore

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

After

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

Conditions: none

Rule: mko_definition · Uses: G1, S03, S04, S07, S08

Leaf basis: mko_definition

If K={0}, equal images force a=b; if f is injective, f(k)=f(0)=0 forces k=0. Both directions are explicit.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S09 · premise_audit · G1, S03, S04, S07, S08 — The equivalence agrees with both conditions failing here and adds no quotient isomorphism.
- S08 · premise_audit · G1, S02, S04, S07 — One collision suffices; being onto Q would not imply injectivity.
- S07 · inverse_equivalence · G1, S01, S04, S06 — The additive difference b-a corresponds to a inverse b in multiplicative notation, using the same source operation.
- S06 · premise_audit · G1, S01, S03, S05 — The model is a qualified homomorphism; an arbitrary map's identity preimage need not be a subgroup.
- S05 · premise_audit · G1, S01, S04 — The inverse in additive notation is negation modulo 4, not a rational reciprocal.
- S04 · premise_audit · G1, S02, S03 — Kernel elements belong to source G, not the target value set.
- S03 · premise_audit · G1, S01, S02 — This checks all pairs, not just generators, using both the formula and 16-entry table.
- S02 · premise_audit · G1, S01 — A total map is not yet a homomorphism; preservation remains to be checked.
- S01 · premise_audit · G1 — Qualify both groups before applying kernel facts to a mapping array.





## Error controls and negative controls

Target identityThe kernel is the entire preimage of target 0, not merely the source label 0.

Homomorphism firstCheck all 16 operation pairs before kernel conclusions.


- Any total map has a normal identity preimage. → reject — The map C4 to C2 with array [0,0,1,1] has identity preimage {0,1}, not closed since 1+1=2, and is not a homomorphism.
- K={0}. → reject — f(2)=0 puts 2 in the kernel too.
- f is surjective, hence injective. → reject — f(0)=f(2) is a source collision.





## Result and limitations

For f:C4 to C2, f(a)=a mod 2, the normal kernel is {0,2}; fibers are its cosets and f is not injective.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: bcd46de77dc90f619f8492cc26c9e5e506e7f2107662144b4c6d8ff101c244b0
- original source SHA-256: bcd46de77dc90f619f8492cc26c9e5e506e7f2107662144b4c6d8ff101c244b0
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-finite-group-homomorphism-kernel-01.json)