Graph isomorphism: checking bijectivity and both directions of adjacency preservation from a complete mapping table

Goal and scope

G has vertices 1, 2, 3, 4 and edges {1,2}, {2,3}, {3,4}, {1,4}; H has vertices a, b, c, d and edges {a,c}, {b,c}, {b,d}, {a,d}. Prove that f: 1↦a, 2↦c, 3↦b, 4↦d is a graph isomorphism G→H; show that the bijection g: 1↦a, 2↦b, 3↦c, 4↦d is not an isomorphism; and prove that the path P (edges {1,2}, {2,3}, {3,4}) is not isomorphic to H, even though f sends every edge of P to an edge of H.

Stays inside the MKO: complete edge sets of finite undirected simple graphs and a complete mapping table (assumption a1). The guide checks both requirements of an isomorphism item by item and proves in general the lemma that an isomorphism induces a bijection between edge sets, using it as an invariant for refutation; a matching degree multiset is treated only as a necessary clue (assumption a2). The general theory of walks, paths, connected components and colouring is not treated, and the canonical MKO and its English edition are not changed.

Givens and symbols

• graph_basics
• function_def
• injective_surjective_def
• finite_counting_basics
• finite_forall

• G1 — G: V(G)={1,2,3,4}, E(G)={{1,2},{2,3},{3,4},{1,4}} (complete list).
• G2 — H: V(H)={a,b,c,d}, E(H)={{a,c},{b,c},{b,d},{a,d}} (complete list).
• G3 — Mapping table f: f(1)=a, f(2)=c, f(3)=b, f(4)=d.
• G4 — For comparison: mapping table g: g(1)=a, g(2)=b, g(3)=c, g(4)=d; path graph P: V(P)={1,2,3,4}, E(P)={{1,2},{2,3},{3,4}}.

• V(G),\ E(G) — vertex set and edge set of G
• \{u,v\} — unordered vertex pair; a possible edge when u≠v
• f,\ g — two mapping tables from V(G) to V(H)
• P — path graph on 1 to 4 with edges {1,2}, {2,3}, {3,4}
• f^{-1} — inverse of the bijection f
• \deg(v) — degree of the vertex v

Rules and sources

• graph_basics · prerequisite — (Simple undirected) graph: G=(V,E), where each edge is an unordered pair of distinct vertices; the degree of a vertex is the number of edges at it; handshake lemma Σ_v deg(v)=2|E|.
• 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.
• 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.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• 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.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mko_iso_def · cited — A graph isomorphism f:V(G)→V(H) must be bijective and, for all distinct u,v, {u,v} is an edge of G iff {f(u),f(v)} is an edge of H. Preserving edges without preserving nonedges is insufficient. · mko-graph-isomorphism
• finite_forall · prerequisite — Finite universal: for a finite set D, 'for all t∈D, Φ(t)' is equivalent to the conjunction of the instances obtained by substituting each element of D; the list must be complete.
• L_edge_bij · lemma — If φ:V(G)→V(H) is an isomorphism of finite simple graphs, then {u,v}↦{φ(u),φ(v)} is a bijection E(G)→E(H), so |E(G)|=|E(H)|.

Main derivation

f:V(G)\to V(H)\ \text{is an isomorphism}

f\ \text{bijective}\ \land\ \forall u\neq v:\ (\{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H))

f(1)=a,\ f(2)=c,\ f(3)=b,\ f(4)=d

f:V(G)\to V(H)\ \text{is a function}

f(1),f(2),f(3),f(4)=a,c,b,d

f(u)=f(v)\Rightarrow u=v

V(H)=\{a,b,c,d\}

a=f(1),\ b=f(3),\ c=f(2),\ d=f(4)

f\ \text{injective},\ f\ \text{surjective}

f\ \text{bijective};\ f^{-1}:\ a\mapsto 1,\ b\mapsto 3,\ c\mapsto 2,\ d\mapsto 4

\forall u\neq v\in V(G):\ (\{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H))

\text{the iff for each of the}\ \tbinom42=6\ \text{unordered pairs}

\{u,v\}\mapsto\{f(u),f(v)\}

\{1,2\}\mapsto\{a,c\},\ \{1,3\}\mapsto\{a,b\},\ \{1,4\}\mapsto\{a,d\},\ \{2,3\}\mapsto\{b,c\},\ \{2,4\}\mapsto\{c,d\},\ \{3,4\}\mapsto\{b,d\}

\{u,v\}\in E(G)\ ?

\{1,2\},\{2,3\},\{3,4\},\{1,4\}\in E(G);\ \{1,3\},\{2,4\}\notin E(G)

\{f(u),f(v)\}\in E(H)\ ?

\{a,c\},\{b,c\},\{b,d\},\{a,d\}\in E(H);\ \{a,b\},\{c,d\}\notin E(H)

\text{edge status of}\ \{u,v\}\ \text{in}\ G\ \text{and of its image in}\ H

\{u,v\}\in E(G)\Leftrightarrow\{f(u),f(v)\}\in E(H)\ \text{for all 6 pairs}

f\ \text{bijective},\ \text{iff on all 6 pairs}

f:G\to H\ \text{is an isomorphism},\ G\cong H

g(1)=a,\ g(2)=b,\ \{1,2\}\in E(G)

\{g(1),g(2)\}=\{a,b\}\notin E(H)\Rightarrow g\ \text{not an isomorphism}

f\ \text{on}\ P:\ \{1,2\},\{2,3\},\{3,4\}\mapsto\{a,c\},\{b,c\},\{b,d\}

\text{every edge of}\ P\ \text{goes to an edge of}\ H

\{1,4\}\notin E(P)

\{f(1),f(4)\}=\{a,d\}\in E(H)\Rightarrow f\ \text{is not an isomorphism}\ P\to H

|E(P)|=3,\ |E(H)|=4

\text{no isomorphism}\ P\to H\ \text{exists}

\deg\ \text{in}\ G\ \text{and}\ H

\{2,2,2,2\}=\{2,2,2,2\}

Substeps and lemmas

\{u,v\}\in E(G)

\{\varphi(u),\varphi(v)\}\in E(H)

\{\varphi(u),\varphi(v)\}=\{\varphi(u'),\varphi(v')\}

\{u,v\}=\{u',v'\}

\{p,q\}\in E(H)

\{\varphi^{-1}(p),\varphi^{-1}(q)\}\in E(G)\ \Rightarrow\ |E(G)|=|E(H)|

Reverse audits

• S16 · premise_audit · G1, G2, graph_basics — This guide records the step as a consistency check of an invariant; the direct map proof of S11 does not depend on it. Adding the classification that a four-vertex simple 2-regular graph is C4 would provide another proof route.
• S15.3 · premise_audit · mko_iso_def, finite_counting_basics — Surjectivity is exactly where the 'nonedges to nonedges' half of the iff is used; an edge-preserving map does not guarantee it. This sub-step does not use L_edge_bij.
• S15.2 · premise_audit · injective_surjective_def — It needs φ⁻¹ to exist, that is, φ bijective; this sub-step does not use L_edge_bij.
• S15.1 · premise_audit · mko_iso_def, injective_surjective_def — Only one direction of the iff and injectivity are used; this sub-step does not use L_edge_bij.
• S15 · premise_audit · L_edge_bij, contrapositive — It uses the contrapositive of 'isomorphic ⇒ equal edge counts'; the converse 'equal edge counts ⇒ isomorphic' is false and not claimed.
• S14 · premise_audit · G4, G2, contradiction — This refutes only the table f; whether P and H are non-isomorphic altogether needs the invariant argument of S15.
• S13 · premise_audit · G4, G3, G2 — Only the '⇒' direction is checked; it does not claim that nonedges are preserved (S14 shows they are not).
• S12 · premise_audit · G1, G2, G4, contradiction — Refutation needs one failing pair; the step does not claim G and H are non-isomorphic (S11 proves they are), only that the table g is not an isomorphism.
• S11 · sufficient_goal_reduction · S01, S05, S06, S10 — Goal G: f is an isomorphism. Sufficient condition H: f is bijective and the iff holds on all 6 pairs; H⇒G by S01 and S06. H is proved forwards in S02 to S10; G is never used as a premise.
• S10 · premise_audit · S08, S09, iff_intro, case_analysis — The edge case gives the '⇒' direction and the nonedge case gives '⇐' (in contrapositive form: nonedges of G match nonedges of H). Missing either class would not give the iff.
• S09 · premise_audit · G2, S07, graph_basics — It needs only table lookups; deciding nonedges relies on the complete list of E(H) (assumption a1).
• S08 · premise_audit · G1, case_analysis — The two classes cover all 6 pairs and are disjoint; the complete list of E(G) is needed, otherwise 'not listed' would not mean nonedge.
• S07 · inverse_equivalence · function_def, S05 — Looking up values replaces equals; f⁻¹ maps each image back to its pair, so the step is two-way.
• S06 · inverse_equivalence · finite_forall, set_extensionality — The universal gives each instance (∀-elimination); with the complete list of 6 instances, all of them together give the universal. Both directions hold.
• S05 · premise_audit · S03, S04, injective_surjective_def — Bijectivity is only the first requirement; on its own it does not give an isomorphism (g in S12 is also a bijection).
• S04 · premise_audit · S02, G2, injective_surjective_def — Each element of V(H) needs only one preimage, and all four are listed.
• S03 · premise_audit · S02, injective_surjective_def — All six comparisons are made; only injectivity is claimed, nothing about adjacency.
• S02 · premise_audit · G3, function_def — It needs exactly one row per vertex with a value in V(H); both are read directly from the table.
• S01 · premise_audit · mko_iso_def — This step only unfolds the definition; bijectivity is checked first (S02 to S05), then the adjacency condition (S06 to S10).

Error controls and negative controls

Preserving edges is not enough

The common mistake named by the MKO is to declare an isomorphism after checking only that edges go to edges. f sends all three edges of P to edges of H (S13), but the nonedge {1,4} goes to the edge {a,d} (S14). Both directions of the iff must be checked: edges to edges and nonedges to nonedges.

Matching degree sequences is not a proof

The six-cycle C6 and two disjoint triangles both have six vertices, six edges and every degree equal to 2, but they are not isomorphic: two triangles contain three pairwise adjacent vertices, C6 does not, and an isomorphism sends three pairwise adjacent vertices to three pairwise adjacent vertices. So matching invariants are only necessary; the isomorphism here comes from the pair-by-pair check of S11.

Check bijectivity and adjacency separately

g is a bijection but not an isomorphism (S12); separately, if a table sent two vertices to the same point, some {u,v} would have a one-point image that is not even a candidate edge. The MKO's order is to check bijectivity first, then all unordered vertex pairs.

• For any two finite undirected simple graphs, equality of their degree multisets is sufficient to imply that the graphs are isomorphic → reject — C6 and two disjoint triangles have the same degree multiset but are not isomorphic, refuting the general claim. Four vertices all of degree 2 form a special case that does force both graphs to be C4; this guide nevertheless proves G≅H directly using the map in S11.
• f sends every edge of P to an edge of H, so f is an isomorphism P→H → reject — The nonedge {1,4} is sent to the edge {a,d} of H.
• g is a bijection V(G)→V(H), so g is an isomorphism → reject — {1,2}∈E(G) but {g(1),g(2)}={a,b}∉E(H).
• P and H both have four vertices, so a suitable mapping table makes them isomorphic → reject — By L_edge_bij an isomorphism needs equal edge counts, but |E(P)|=3≠4=|E(H)|.

Result and limitations

f: 1↦a, 2↦c, 3↦b, 4↦d is a bijection and the adjacency iff holds on all 6 unordered vertex pairs, so f is an isomorphism and G≅H. The bijection g fails at {1,2}↦{a,b} and is not an isomorphism. f sends every edge of the path P to an edge of H but sends the nonedge {1,4} to the edge {a,d}; and by Lemma L_edge_bij, |E(P)|=3≠4=|E(H)|, so P and H are not isomorphic.

• The remark in the error controls that an isomorphism preserves three pairwise adjacent vertices is explanatory; it follows directly from the iff condition and is not a numbered step.
• finite_forall is a premise of this guide and is not derived here from more basic logical rules.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: a7cc7455e8b911e77e5121725e1be4abeed121e79d85845f5c53dcd1836af658
• original source SHA-256: 9d22ff5f2bd20224ad3785c20866dd5d700d99fedad9037b43fd496881eceb3e
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)