The adjacency array of a graph and the graph of an array

The adjacency array SimpleGraph.adjArray G of a graph on ℕ is symmetric with false diagonal. An array is read back as a graph by graphOfArray, the SimpleGraph.fromRel of the array: i and j are adjacent when they are distinct and the array is true at (i, j) or at (j, i). The two are mutually inverse on the symmetric arrays with false diagonal and intertwine relabelling of the graph with the diagonal relabelling of the array. The adjacency array itself, its measurability and its injectivity are in SimpleGraph/Maps.lean and SimpleGraph/Measurable.lean.

Main results

• SimpleGraph.adjArray_mem_symmetricArraysWithDiag, SimpleGraph.adjArray_comap — the adjacency array of a graph on ℕ lies in the carrier and intertwines relabelling.
• TauCeti.DenseGraphLimits.graphOfArray, graphOfArray_adj, measurable_graphOfArray, graphOfArray_pairReindex.
• SimpleGraph.graphOfArray_adjArray, TauCeti.DenseGraphLimits.adjArray_graphOfArray — the two round trips.

References

• P. Diaconis, S. Janson, Graph limits and exchangeable random graphs, Rend. Mat. Appl. (7) 28 (2008), 33–61, Section 5: exchangeable random graphs as symmetric zero-diagonal arrays.

No material is adapted from cameronfreer/graphon; the adjacency array is read directly from Mathlib's adjacency relation, and the relabelling square is SimpleGraph.comap_adj.

theorem SimpleGraph.adjArray_mem_symmetricArraysWithDiag (G : SimpleGraph ℕ) : G.adjArray ∈ TauCeti.Probability.symmetricArraysWithDiag Bool false

The adjacency array of a graph is symmetric with false diagonal.

theorem SimpleGraph.adjArray_comap (σ : Equiv.Perm ℕ) (G : SimpleGraph ℕ) : (SimpleGraph.comap (⇑σ) G).adjArray = TauCeti.Probability.pairReindex σ σ G.adjArray

Relabelling the graph is relabelling both axes of its adjacency array.

def TauCeti.DenseGraphLimits.graphOfArray (x : ℕ × ℕ → Bool) : SimpleGraph ℕ

The graph of an array: i and j are adjacent when they are distinct and the array is true at (i, j) or at (j, i), so on a symmetric array at either.

Equations

• TauCeti.DenseGraphLimits.graphOfArray x = SimpleGraph.fromRel fun (i j : ℕ) => x (i, j) = true

@[simp]

theorem TauCeti.DenseGraphLimits.graphOfArray_adj (x : ℕ × ℕ → Bool) (i j : ℕ) : (graphOfArray x).Adj i j ↔ i ≠ j ∧ (x (i, j) = true ∨ x (j, i) = true)

Adjacency in the graph of an array.

theorem TauCeti.DenseGraphLimits.measurable_graphOfArray : Measurable graphOfArray

Reading an array as a graph is measurable.

@[simp]

theorem SimpleGraph.graphOfArray_adjArray (G : SimpleGraph ℕ) : TauCeti.DenseGraphLimits.graphOfArray G.adjArray = G

The graph of the adjacency array of a graph is the graph.

@[simp]

theorem TauCeti.DenseGraphLimits.adjArray_graphOfArray {x : ℕ × ℕ → Bool} (hx : x ∈ Probability.symmetricArraysWithDiag Bool false) : (graphOfArray x).adjArray = x

The adjacency array of the graph of a symmetric false-diagonal array is the array.

theorem TauCeti.DenseGraphLimits.graphOfArray_pairReindex (σ : Equiv.Perm ℕ) (x : ℕ × ℕ → Bool) : graphOfArray (Probability.pairReindex σ σ x) = SimpleGraph.comap (⇑σ) (graphOfArray x)

The graph of a relabelled array is the relabelling of its graph.