Oriented incidence matrix

This file defines the oriented incidence matrix G.orientedIncMatrix R of a simple graph G over a linearly ordered vertex type, and proves the Gram factorization

G.orientedIncMatrix R * (G.orientedIncMatrix R)ᵀ = G.lapMatrix R,

the standard factorization of the graph Laplacian D - A. This complements the unoriented G.incMatrix R, whose Gram matrix is the signless Laplacian D + A (incMatrix_mul_transpose_diag ff.): the signs are what produce the Laplacian.

Main definitions

• SimpleGraph.orientedIncMatrix: the α × Sym2 α matrix with, in the column of an edge e = s(u, w) with u < w, entry +1 at row w (the larger endpoint), -1 at row u, and 0 elsewhere; columns of non-edges are zero.

Main results

• SimpleGraph.orientedIncMatrix_mul_transpose: N * Nᵀ = D - A.

Implementation notes

The orientation (each edge points from its smaller to its larger endpoint) is induced by the linear order on the vertex type. Any orientation yields the same Gram matrix, since each edge contributes (±1)² to a diagonal entry and (+1) * (-1) to an off-diagonal one.

def SimpleGraph.orientedIncMatrix (R : Type u_1) {α : Type u_2} (G : SimpleGraph α) [Zero R] [One R] [Neg R] [LinearOrder α] [DecidableRel G.Adj] : Matrix α (Sym2 α) R

The oriented incidence matrix: for an edge e incident to v, the entry is +1 if v is the larger endpoint of e and -1 if it is the smaller one; entries vanish off the incidence set.

Equations

• SimpleGraph.orientedIncMatrix R G = Matrix.of fun (v : α) (e : Sym2 α) => if e ∈ G.incidenceSet v then if v = e.sup then 1 else -1 else 0

theorem SimpleGraph.orientedIncMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Ring R] [LinearOrder α] [DecidableRel G.Adj] {v : α} {e : Sym2 α} : orientedIncMatrix R G v e = if e ∈ G.incidenceSet v then if v = e.sup then 1 else -1 else 0

theorem SimpleGraph.orientedIncMatrix_of_notMem_incidenceSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Ring R] [LinearOrder α] [DecidableRel G.Adj] {v : α} {e : Sym2 α} (h : e ∉ G.incidenceSet v) : orientedIncMatrix R G v e = 0

theorem SimpleGraph.orientedIncMatrix_mul_self {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Ring R] [LinearOrder α] [DecidableRel G.Adj] {v : α} {e : Sym2 α} : orientedIncMatrix R G v e * orientedIncMatrix R G v e = incMatrix R G v e

On its incidence set the oriented entry squares to 1, so the square of any entry is the corresponding unoriented incidence entry.

theorem SimpleGraph.orientedIncMatrix_apply_mul_apply_of_adj {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Ring R] [LinearOrder α] [DecidableRel G.Adj] {u w : α} (hadj : G.Adj u w) : orientedIncMatrix R G u s(u, w) * orientedIncMatrix R G w s(u, w) = -1

The two endpoints of an edge carry opposite signs: the product of the oriented entries of u ≠ w at their common edge s(u, w) is -1.

theorem SimpleGraph.orientedIncMatrix_apply_add_apply_of_adj {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Ring R] [LinearOrder α] [DecidableRel G.Adj] {u w : α} (hadj : G.Adj u w) : orientedIncMatrix R G u s(u, w) + orientedIncMatrix R G w s(u, w) = 0

The two endpoints of an edge carry cancelling signs: the column of an edge sums to zero over its two endpoints.

theorem SimpleGraph.orientedIncMatrix_apply_mul_apply_of_ne {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Ring R] [LinearOrder α] [DecidableRel G.Adj] {u w : α} {e : Sym2 α} (hne : u ≠ w) (he : e ≠ s(u, w)) : orientedIncMatrix R G u e * orientedIncMatrix R G w e = 0

Distinct vertices see disjoint signed columns away from their common edge: the product of oriented entries vanishes at every e ≠ s(u, w).

theorem SimpleGraph.orientedIncMatrix_mul_transpose {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Ring R] [Fintype α] [LinearOrder α] [DecidableRel G.Adj] : orientedIncMatrix R G * (orientedIncMatrix R G).transpose = lapMatrix R G

Laplacian factorization. The Gram matrix of the oriented incidence matrix is the graph Laplacian: N * Nᵀ = D - A. (The unoriented incidence matrix gives D + A instead; the signs are what make the Laplacian.)