Signed adjacency matrices

A weight function w : V → V → ℝ defines the signed adjacency matrix of G, equal to w i j on edges and to 0 elsewhere. With w taking values ±1 this is the adjacency matrix of a signing of G, whose characteristic polynomials average to the matching polynomial (GodsilGutman).

Main definitions

• SimpleGraph.signedAdjMatrix G w: the signed adjacency matrix.

Main results

• SimpleGraph.signedAdjMatrix_eq_zero_of_not_adj, SimpleGraph.signedAdjMatrix_diag: it vanishes off the edges and on the diagonal.

noncomputable def SimpleGraph.signedAdjMatrix {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (w : V → V → ℝ) : Matrix V V ℝ

The signed adjacency matrix A_w: entry (i, j) is the signing w i j when i ~ j, else 0. For the MSS argument the signing is symmetric on edges (w i j = w j i) and takes values in {−1, +1}; those constraints enter as hypotheses where needed.

Equations

• G.signedAdjMatrix w i j = if G.Adj i j then w i j else 0

theorem SimpleGraph.signedAdjMatrix_eq_zero_of_not_adj {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (w : V → V → ℝ) {i j : V} (h : ¬G.Adj i j) : G.signedAdjMatrix w i j = 0

Off the edge set, the signed adjacency matrix vanishes.

theorem SimpleGraph.signedAdjMatrix_diag {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (w : V → V → ℝ) (i : V) : G.signedAdjMatrix w i i = 0

The diagonal of the signed adjacency matrix is zero (no self-loops in a SimpleGraph).