The simple-graph / finite-digraph bridge (#94, shared infrastructure)

The symmetric loopless embedding of simple graphs into finite digraphs, in its own module so the foundational relational/directed carrier Graphon.InfiniteDigraph (D1) does not depend on SimpleGraph. Used by the graphon-embedding sampler law (D3c) and the directed t/t_inj/t_ind interlude (#94).

• SimpleGraph.toFiniteDigraph — the embedding, with its @[simp] coordinate lemma;
• SimpleGraph.toFiniteDigraph_injective — injectivity;
• SimpleGraph.exists_toFiniteDigraph_eq_iff — range classification: the embedded digraphs are exactly the loopless symmetric ones.

noncomputable def SimpleGraph.toFiniteDigraph {k : ℕ} (G : SimpleGraph (Fin k)) : FiniteDigraph k

The symmetric loopless embedding of a simple graph as a finite digraph.

Equations

• G.toFiniteDigraph c = decide (G.Adj (c.snd 0) (c.snd 1))

@[simp]

theorem SimpleGraph.toFiniteDigraph_coord {k : ℕ} (G : SimpleGraph (Fin k)) (a b : Fin k) : G.toFiniteDigraph (digraphCoord a b) = decide (G.Adj a b)

The ordered-pair coordinates of the embedded digraph read the (classically decided) adjacency of the simple graph.

theorem SimpleGraph.toFiniteDigraph_injective {k : ℕ} : Function.Injective toFiniteDigraph

The symmetric loopless embedding is injective.

theorem SimpleGraph.exists_toFiniteDigraph_eq_iff {k : ℕ} (D : FiniteDigraph k) : (∃ (G : SimpleGraph (Fin k)), G.toFiniteDigraph = D) ↔ (∀ (i : Fin k), D (digraphCoord i i) = false) ∧ ∀ (i j : Fin k), D (digraphCoord i j) = D (digraphCoord j i)

Classification of the range of the embedding: a finite digraph is an embedded simple graph iff its coordinates are loopless and symmetric.