Incidence matrix of a simple graph

This file defines the unoriented incidence matrix of a simple graph.

Main definitions

• SimpleGraph.incMatrix: G.incMatrix R is the incidence matrix of G over the ring R.

Main results

• SimpleGraph.incMatrix_mul_transpose_diag: The diagonal entries of the product of G.incMatrix R and its transpose are the degrees of the vertices.
• SimpleGraph.incMatrix_mul_transpose: Gives a complete description of the product of G.incMatrix R and its transpose; the diagonal is the degrees of each vertex, and the off-diagonals are 1 or 0 depending on whether or not the vertices are adjacent.
• SimpleGraph.incMatrix_transpose_mul_diag: The diagonal entries of the product of the transpose of G.incMatrix R and G.inc_matrix R are 2 or 0 depending on whether or not the unordered pair is an edge of G.

Implementation notes

The usual definition of an incidence matrix has one row per vertex and one column per edge. However, this definition has columns indexed by all of Sym2 α, where α is the vertex type. This appears not to change the theory, and for simple graphs it has the nice effect that every incidence matrix for each SimpleGraph α has the same type.

TODO

• Define the oriented incidence matrices for oriented graphs.
• Define the graph Laplacian of a simple graph using the oriented incidence matrix from an arbitrary orientation of a simple graph.

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

G.incMatrix R is the α × Sym2 α matrix whose (a, e)-entry is 1 if e is incident to a and 0 otherwise.

Equations

• SimpleGraph.incMatrix R G = Matrix.of fun (a : α) (e : Sym2 α) => if e ∈ G.incidenceSet a then 1 else 0

theorem SimpleGraph.incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} : incMatrix R G a e = (G.incidenceSet a).indicator 1 e

theorem SimpleGraph.incMatrix_apply' {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} : incMatrix R G a e = if e ∈ G.incidenceSet a then 1 else 0

Entries of the incidence matrix can be computed given additional decidable instances.

theorem SimpleGraph.incMatrix_apply_mul_incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] [DecidableEq α] [DecidableRel G.Adj] {a b : α} {e : Sym2 α} : incMatrix R G a e * incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e

theorem SimpleGraph.incMatrix_apply_mul_incMatrix_apply_of_not_adj {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] [DecidableEq α] [DecidableRel G.Adj] {a b : α} {e : Sym2 α} (hab : a ≠ b) (h : ¬G.Adj a b) : incMatrix R G a e * incMatrix R G b e = 0

theorem SimpleGraph.incMatrix_of_notMem_incidenceSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} (h : e ∉ G.incidenceSet a) : incMatrix R G a e = 0

theorem SimpleGraph.incMatrix_of_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} (h : e ∈ G.incidenceSet a) : incMatrix R G a e = 1

theorem SimpleGraph.incMatrix_apply_eq_zero_iff {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} [Nontrivial R] : incMatrix R G a e = 0 ↔ e ∉ G.incidenceSet a

theorem SimpleGraph.incMatrix_apply_eq_one_iff {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} [Nontrivial R] : incMatrix R G a e = 1 ↔ e ∈ G.incidenceSet a

theorem SimpleGraph.sum_incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {a : α} [Fintype (Sym2 α)] [Fintype ↑(G.neighborSet a)] : ∑ e : Sym2 α, incMatrix R G a e = ↑(G.degree a)

theorem SimpleGraph.incMatrix_mul_transpose_diag {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {a : α} [Fintype (Sym2 α)] [Fintype ↑(G.neighborSet a)] : (incMatrix R G * (incMatrix R G).transpose) a a = ↑(G.degree a)

theorem SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {e : Sym2 α} [Fintype α] : e ∈ G.edgeSet → ∑ a : α, incMatrix R G a e = 2

theorem SimpleGraph.sum_incMatrix_apply_of_notMem_edgeSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {e : Sym2 α} [Fintype α] (h : e ∉ G.edgeSet) : ∑ a : α, incMatrix R G a e = 0

theorem SimpleGraph.incMatrix_transpose_mul_diag {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {e : Sym2 α} [Fintype α] [Decidable (e ∈ G.edgeSet)] : ((incMatrix R G).transpose * incMatrix R G) e e = if e ∈ G.edgeSet then 2 else 0

theorem SimpleGraph.incMatrix_mul_transpose_apply_of_adj {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype (Sym2 α)] [DecidableEq α] [DecidableRel G.Adj] [Semiring R] {a b : α} (h : G.Adj a b) : (incMatrix R G * (incMatrix R G).transpose) a b = 1

theorem SimpleGraph.incMatrix_mul_transpose {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype (Sym2 α)] [DecidableEq α] [DecidableRel G.Adj] [Semiring R] [G.LocallyFinite] : incMatrix R G * (incMatrix R G).transpose = Matrix.of fun (a b : α) => if a = b then ↑(G.degree a) else if G.Adj a b then 1 else 0