Metamath Proof Explorer

Table of Contents - 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.

  1. cgrisom
  2. cisomgr
  3. df-grisom
  4. df-isomgr
  5. isomgrrel
  6. isomgr
  7. isisomgr
  8. isomgreqve
  9. isomushgr
  10. isomuspgrlem1
  11. isomuspgrlem2a
  12. isomuspgrlem2b
  13. isomuspgrlem2c
  14. isomuspgrlem2d
  15. isomuspgrlem2e
  16. isomuspgrlem2
  17. isomuspgr
  18. isomgrref
  19. isomgrsym
  20. isomgrsymb
  21. isomgrtrlem
  22. isomgrtr
  23. strisomgrop
  24. ushrisomgr