(Local) Isomorphisms of graphs

[avekens]

In MathOverflow (https://mathoverflow.net/questions/491133/locally-isomorphic-graphs), the following question was posted (and answered):

If G=(V,E) is a simple undirected graph and v∈V we let the "pointed neighborhood" (or "closed neighborhood") of v be defined by N*(G,v)={w∈V:{v,w}∈E}∪{v}.

If Gi=(Vi,Ei) are graphs for i=0,1 then they are said to be locally isomorphic if there is a bijection φ:V0→V1 such that for all v∈V0 we have that N*(G0,v) and N*(G1, φ(v)) are isomorphic induced subgraphs of G0 and G1, respectively.

Question: Are there connected locally isomorphic graphs G0,G1 with G0≆G1?

Answers:

1. Yes, since it is easy to construct triangle-free cubic graphs which are not isomorphic. For example, the Petersen graph and the 5-prism are not isomorphic, but are locally isomorphic, since every pointed neighbourhood in either graph is isomorphic to K1,3.
2. Let G0 be two pentagons (5-cycles) connected by an edge: say V0=(Z/5Z)×{0,1} with (i,p) connected to (i−1,p) and (i+1,p) except that (0,p) is also connected to (0,1−p). Let G1 be a decagon (10-cycle) with an extra diameter: say V1=Z/10Z with i connected to i−1 and i+1 except that 0 and 5 are also connected.
3. Let G0 be two triangles (3-cycles) connected by an edge: say V0=(Z/3Z)×{0,1} with (i,p) connected to (i−1,p) and (i+1,p) except that (0,p) is also connected to (0,1−p). Let G1 be a hexagon (6-cycle) with an extra diameter: say V1=Z/6Z with i connected to i−1 and i+1 except that 0 and 3 are also connected.

To prove the (third) answer formally with Metamath, the required definitions (and related theorems) have to be provided first:

• Definition of graph isomorphisms (and isomorphic graphs) and related basic theorems
• Definition of closed neighborhoods of vertices in a graph and related basic theorems
• Definition of induced subgraphs and related basic theorems
• Definition of locally isomorphic graphs and related basic theorems
• Provision of a criterion for two graphs not being isomorphic (one graph contains a triangle and the other is tringle-free)
• Provision of G0 and G1 formally (as ordered pairs of vertices and edges)
• Proof that G0 and G1 are connected graphs
• Proof that G0 and G1 are locally isomorphic
• Proof that G0 and G1 are not isomorphic

[avekens]

I almost finished the first item "Definition of graph isomorphisms (and isomorphic graphs) and related basic theorems" and will provide the material soon.

[avekens]

next 2 items done with PR #4828