# The correct image isomorphism for a nonsurjection

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-first-isomorphism-theorem-finite-groups/)

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-first-isomorphism-theorem-finite-groups-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For f:C4 to C4,f(a)=2a mod 4, C4/{0,2} is isomorphic to {0,2}, not the full codomain C4.

Complete finite homomorphism, kernel, image, quotient and induced map with every representative checked.





## Givens and symbols


- calc


- G1 — G=Q=C4, both using the full addition-modulo-4 table below; f(0)=0,f(1)=2,f(2)=0,f(3)=2.


- K,I — source kernel and target image
- \bar f — map from cosets to the image





## Rules and sources


- calc · prerequisite — Assume exact modulo-4 arithmetic and definitions of groups, homomorphisms, quotient cosets and isomorphism, in additive notation.
- mko_definition · cited — Qualify both complete Cayley tables and the complete total homomorphism f first. Construct the full kernel, image and kernel-coset quotient. The induced map bar_f(g*kernel)=f(g) must agree on every representative of every coset, preserve every product and be injective and surjective onto the image. Equal cardinalities alone do not prove an isomorphism. If f is not surjective, do not replace the image by the entire codomain. Finite enumeration certifies the specified model, not the general abstract theorem; a nonhomomorphism cannot invoke the theorem. · mko-first-isomorphism-theorem-finite-groups





## Main derivation

S01 · impliesBefore

G=Q=C_4

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}

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Source and target are the same complete four-element group model, each with this 16-entry table; associativity descends from integers, identity is 0 and inverse list 0,3,2,1 is complete.



S02 · impliesBefore

f:G\to Q

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

All four values of the complete total map lie in Q.



S03 · impliesBefore

f((a+b)\bmod4)\equiv2(a+b)\pmod4

After

\begin{array}{c|cccc}f(a+b)&0&1&2&3\\\hline 0&0&2&0&2\\1&2&0&2&0\\2&0&2&0&2\\3&2&0&2&0\\\end{array}\quad=f(a)+f(b)\ (\bmod4)

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Distributivity and reduction give equality for all 16 pairs, fully verifying the homomorphism.



S04 · impliesBefore

K=f^{-1}(0),\quad I=f(G)

After

K=\{0,2\},\quad I=\{0,2\};\quad0+0=0,0+2=2,2+0=2,2+2=0\ (\bmod4)

Conditions: none

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

Leaf basis: calc

The full preimage and image are explicit; four products and inverses 0,2 qualify subgroups, and g+k-g=k for all g proves K normal.



S05 · impliesBefore

A=0+K=2+K,\quad B=1+K=3+K

After

A=\{0,2\},\quad B=\{1,3\},\quad A\sqcup B=G

Conditions: none

Rule: calc · Uses: G1, S01, S04

Leaf basis: calc

All four cosets deduplicate to a complete two-class partition.



S06 · impliesBefore

a,b=0,1,2,3

After

\begin{array}{c|cccc}(a+b)+K&0&1&2&3\\\hline 0&A&B&A&B\\1&B&A&B&A\\2&A&B&A&B\\3&B&A&B&A\\\end{array}\qquad\begin{array}{c|cc}+&A&B\\\hline A&A&B\\B&B&A\\\end{array}

Conditions: none

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

Leaf basis: calc

All 16 representative-pair class indices are constant on each 2-by-2 block, proving well-defined quotient addition and yielding its full four-entry table.



S07 · impliesBefore

\bar f(a+K)=f(a)

After

f(0)=f(2)=0\Rightarrow\bar f(A)=0;\quad f(1)=f(3)=2\Rightarrow\bar f(B)=2

Conditions: none

Rule: calc · Uses: G1, S02, S05, S06

Leaf basis: calc

Every representative within each coset has the same value, first proving representative independence of the induced map.



S08 · impliesBefore

A+A=A,A+B=B,B+A=B,B+B=A

After

0+0=0,0+2=2,2+0=2,2+2=0\ (\bmod4)

Conditions: none

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

Leaf basis: calc

The images of all four quotient products match products in I, so bar f is a homomorphism.



S09 · impliesBefore

\bar f(A)=0\ne2=\bar f(B)

After

\bar f\text{ injective and onto }I=\{0,2\}

Conditions: none

Rule: calc · Uses: G1, S04, S07

Leaf basis: calc

Distinct images prove injectivity, and both I elements are hit, proving surjectivity onto the image.



S10 · impliesBefore

\bar f:G/K\to I\text{ well-defined bijective homomorphism}

After

G/K\cong I\subsetneq Q

Conditions: none

Rule: mko_definition · Uses: G1, S06, S07, S08, S09

Leaf basis: mko_definition

Well-definedness, operation preservation and bijectivity establish the first-isomorphism conclusion for this model.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S10 · premise_audit · G1, S06, S07, S08, S09 — This finite certificate does not replace the general abstract proof or substitute Q for the proper image.
- S09 · premise_audit · G1, S04, S07 — Codomain values 1,3 are missed, so onto Q cannot be claimed.
- S08 · premise_audit · G1, S04, S06, S07 — The carriers differ but all four products correspond; size two alone is not an isomorphism proof.
- S07 · premise_audit · G1, S02, S05, S06 — One cannot check only 0,1 and ignore 2,3; all four representatives are checked.
- S06 · premise_audit · G1, S01, S04, S05 — Associativity descends, identity is A, and A,B are each self-inverse, fully qualifying the quotient.
- S05 · premise_audit · G1, S01, S04 — Quotient elements are sets A,B rather than unique representatives 0,1.
- S04 · premise_audit · G1, S01, S02, S03 — K belongs to the source and I to the target, with distinct roles despite identical numeral sets.
- S03 · premise_audit · G1, S01, S02 — Neither cardinality nor f(0)=0 alone qualifies a homomorphism.
- S02 · premise_audit · G1, S01 — Q contains 1,3, which f need not hit; retain the image/codomain distinction.
- S01 · premise_audit · G1 — Identical group models do not make f the identity; the map still needs checking.





## Error controls and negative controls

Image boundaryThe conclusion targets I={0,2}; without surjectivity it cannot be replaced by Q.

Representatives firstCheck A's representatives 0,2 and B's 1,3 before the induced map.


- G/K is isomorphic to Q because f is a homomorphism. → reject — G/K has 2 elements but Q has 4, and f is not onto.
- Equal sizes |G/K|=|I| prove isomorphism. → reject — An actual induced map must respect all products and representatives; sizes give no operation certificate.
- bar f(B) may differ for representatives 1 and 3. → reject — f(1)=f(3)=2, and well-definedness requires agreement.





## Result and limitations

For f:C4 to C4,f(a)=2a mod 4, C4/{0,2} is isomorphic to {0,2}, not the full codomain C4.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 9360cc100c3545402543cbff3455c309c354f0877cbee06c221b8fcf66c7282a
- original source SHA-256: 9360cc100c3545402543cbff3455c309c354f0877cbee06c221b8fcf66c7282a
- 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-first-isomorphism-theorem-finite-groups-01.json)