A simple graph as a multigraph

The multigraph G.shadowGraph of a simple graph G on a finite set V, as sec:molecule-application-carrier presents it (lem:molecule-graph-carrier). The square G² and the generic rank are defined for a SimpleGraph V, and the deficiency and the molecular and panel-hinge frameworks for a multigraph Graph V β, whose edges are drawn from a type β of labels; the molecule rank formula (Application.lean) applies the latter to G.shadowGraph.

The labels of G.shadowGraph are Sym2 V. Its link between adjacent vertices u and v of G is labelled s(u, v), so it is simple, has vertex set V, and links exactly the adjacent pairs of G.

Main results

• SimpleGraph.shadowGraph: the multigraph of G.
• SimpleGraph.shadowGraph_simple: it is simple.
• SimpleGraph.shadowGraph_vertexSet: its vertex set is V.
• SimpleGraph.shadowGraph_isLink_iff: it links exactly the adjacent pairs of G.

def SimpleGraph.shadowGraph {V : Type u_1} (G : SimpleGraph V) : Graph V (Sym2 V)

The multigraph of a simple graph (lem:molecule-graph-carrier): the multigraph on V, with the labels Sym2 V, that links x and y by the label s(x, y) when G.Adj x y.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.shadowGraph_simple {V : Type u_1} (G : SimpleGraph V) : G.shadowGraph.Simple

The multigraph of a simple graph is simple (lem:molecule-graph-carrier): two links with the same ends have the same label s(x, y), and there is no loop, as G.Adj is irreflexive.

@[simp]

theorem SimpleGraph.shadowGraph_vertexSet {V : Type u_1} (G : SimpleGraph V) : G.shadowGraph.vertexSet = Set.univ

The vertex set of the multigraph of a simple graph (lem:molecule-graph-carrier): it is all of V.

theorem SimpleGraph.shadowGraph_isLink_iff {V : Type u_1} (G : SimpleGraph V) (x y : V) : (∃ (e : Sym2 V), G.shadowGraph.IsLink e x y) ↔ G.Adj x y

The links of the multigraph of a simple graph (lem:molecule-graph-carrier): G.shadowGraph links x and y iff G.Adj x y. The equivalence needs no x ≠ y: both sides fail at x = y.