# 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.
noncomputable def SimpleGraph.incMatrix (R : Type u_1) {α : Type u_2} (G : ) [Zero R] [One R] :
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
• = (G.incidenceSet a).indicator 1
Instances For
theorem SimpleGraph.incMatrix_apply {R : Type u_1} {α : Type u_2} (G : ) [Zero R] [One R] {a : α} {e : Sym2 α} :
= (G.incidenceSet a).indicator 1 e
theorem SimpleGraph.incMatrix_apply' {R : Type u_1} {α : Type u_2} (G : ) [Zero R] [One R] [] [DecidableRel G.Adj] {a : α} {e : Sym2 α} :
= 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 : ) [] {a : α} {b : α} {e : Sym2 α} :
* = (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 : ) [] {a : α} {b : α} {e : Sym2 α} (hab : a b) (h : ¬G.Adj a b) :
* = 0
theorem SimpleGraph.incMatrix_of_not_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} (h : eG.incidenceSet a) :
= 0
theorem SimpleGraph.incMatrix_of_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} (h : e G.incidenceSet a) :
= 1
theorem SimpleGraph.incMatrix_apply_eq_zero_iff {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} [] :
= 0 eG.incidenceSet a
theorem SimpleGraph.incMatrix_apply_eq_one_iff {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} [] :
= 1 e G.incidenceSet a
theorem SimpleGraph.sum_incMatrix_apply {R : Type u_1} {α : Type u_2} (G : ) [Fintype (Sym2 α)] [] {a : α} [Fintype (G.neighborSet a)] :
e : Sym2 α, = (G.degree a)
theorem SimpleGraph.incMatrix_mul_transpose_diag {R : Type u_1} {α : Type u_2} (G : ) [Fintype (Sym2 α)] [] {a : α} [Fintype (G.neighborSet a)] :
( * ().transpose) a a = (G.degree a)
theorem SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : ) [] {e : Sym2 α} [] :
e G.edgeSeta : α, = 2
theorem SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : ) [] {e : Sym2 α} [] (h : eG.edgeSet) :
a : α, = 0
theorem SimpleGraph.incMatrix_transpose_mul_diag {R : Type u_1} {α : Type u_2} (G : ) [] {e : Sym2 α} [] [Decidable (e G.edgeSet)] :
(().transpose * ) 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 : ) [Fintype (Sym2 α)] [] {a : α} {b : α} (h : G.Adj a b) :
( * ().transpose) a b = 1
theorem SimpleGraph.incMatrix_mul_transpose {R : Type u_1} {α : Type u_2} (G : ) [Fintype (Sym2 α)] [] [(a : α) → Fintype (G.neighborSet a)] [] [DecidableRel G.Adj] :
* ().transpose = fun (a b : α) => if a = b then (G.degree a) else if G.Adj a b then 1 else 0