# Metamath Proof Explorer

## Table of Contents - 20.43.15.1. Isomorphic graphs

In the following, a general definition of the isomorphy relation for graphs and specializations for simple hypergraphs (isomushgr) and simple pseudographs (isomuspgr) are provided. The latter corresponds to the definition in [Bollobas] p. 3). It is shown that the isomorphy relation for graphs is an equivalence relation (isomgrref, isomgrsym, isomgrtr). Fianlly, isomorphic graphs with different representations are studied (strisomgrop, ushrisomgr).

Maybe more important than graph isomorphy is the notion of graph isomorphism, which can be defined as in df-grisom. Then resp. . Notice that there can be multiple isomorphisms between two graphs (let and be two graphs with two vertices and one edge, then and are two different isomorphisms between these graphs).

Another approach could be to define a category of graphs (there are maybe multiple ones), where graph morphisms are couples consisting in a function on vertices and a function on edges with required compatibilities, as used in the definition of . And then, a graph isomorphism is defined as an isomorphism in the category of graphs (something like "GraphIsom = ( Iso ` GraphCat )" ). Then general category theory theorems could be used, e.g., to show that graph isomorphy is an equivalence relation.