Metamath Proof Explorer


Table of Contents - 21.51.15.4. Isomorphisms of graphs

This section is about isomorphisms of graphs, whereby the term "isomorphism" is used in both of its meanings (according to the Meriam-Webster dictionary, see https://www.merriam-webster.com/dictionary/isomorphism): "1: the quality or state of being isomorphic." and "2: a one-to-one correspondence between two mathematical sets".

At first, an operation is defined (see df-grim) which provides the graph isomorphisms (as "one-to-one correspondence") between two given graphs. This definition, however, is applicable for any two sets, but is meaningful only if these sets have "vertices" and "edges".

Afterwards, a binary relation is defined (see df-gric) which is true for two graphs iff there is a graph isomorphisms between these graphs. Then these graphs are called "isomorphic". Therefore, this relation is also called "is isomorphic to" relation. More formally, resp. . Notice that there can be multiple isomorphisms between two graphs. For example, let and be two graphs with two vertices and one edge, then and are two different isomorphisms between these graphs.

The names and symbols are chosen analogously to group isomorphisms (see df-gim) resp. isomorphism between groups (see df-gic).

The general definition of graph isomorphisms and the relation "is isomorphic to" for graphs is specialized for simple hypergraphs (gricushgr) and simple pseudographs (gricuspgr). The latter corresponds to the definition in [Bollobas] p. 3. It is shown that the relation "is isomorphic to" for graphs is an equivalence relation, see gricer. Finally, isomorphic graphs with different representations are studied (opstrgric, ushggricedg).

Another approach could be to define a category of graphs (there are maybe multiple ones), where graph morphisms are couples consisting of 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 isomorphism is an equivalence relation.

  1. cgrisom
  2. cgrim
  3. cgric
  4. df-grisom
  5. df-grim
  6. grimfn
  7. grimdmrel
  8. df-gric
  9. isgrim
  10. grimprop
  11. grimf1o
  12. grimidvtxedg
  13. grimid
  14. grimuhgr
  15. grimcnv
  16. grimco
  17. uhgrimedgi
  18. uhgrimedg
  19. uhgrimprop
  20. isuspgrim0lem
  21. isuspgrim0
  22. isuspgrimlem
  23. isuspgrim
  24. upgrimwlklem1
  25. upgrimwlklem2
  26. upgrimwlklem3
  27. upgrimwlklem4
  28. upgrimwlklem5
  29. upgrimwlk
  30. upgrimwlklen
  31. upgrimtrlslem1
  32. upgrimtrlslem2
  33. upgrimtrls
  34. upgrimpthslem1
  35. upgrimpthslem2
  36. upgrimpths
  37. upgrimspths
  38. upgrimcycls
  39. brgric
  40. brgrici
  41. gricrcl
  42. dfgric2
  43. gricbri
  44. gricushgr
  45. gricuspgr
  46. gricrel
  47. gricref
  48. gricsym
  49. gricsymb
  50. grictr
  51. gricer
  52. gricen
  53. opstrgric
  54. ushggricedg
  55. cycldlenngric
  56. isubgrgrim
  57. uhgrimisgrgriclem
  58. uhgrimisgrgric
  59. clnbgrisubgrgrim
  60. clnbgrgrimlem
  61. clnbgrgrim
  62. grimedg
  63. grimedgi