# Documentation

Mathlib.Combinatorics.SimpleGraph.IncMatrix

# 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.

Instances For
theorem SimpleGraph.incMatrix_apply {R : Type u_1} {α : Type u_2} (G : ) [Zero R] [One R] {a : α} {e : Sym2 α} :
=
theorem SimpleGraph.incMatrix_apply' {R : Type u_1} {α : Type u_2} (G : ) [Zero R] [One R] [] [DecidableRel G.Adj] {a : α} {e : Sym2 α} :
= if 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 α} :
* =
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 : ¬) :
* = 0
theorem SimpleGraph.incMatrix_of_not_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} (h : ¬) :
= 0
theorem SimpleGraph.incMatrix_of_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} (h : ) :
= 1
theorem SimpleGraph.incMatrix_apply_eq_zero_iff {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} [] :
= 0 ¬
theorem SimpleGraph.incMatrix_apply_eq_one_iff {R : Type u_1} {α : Type u_2} (G : ) [] {a : α} {e : Sym2 α} [] :
= 1
theorem SimpleGraph.sum_incMatrix_apply {R : Type u_1} {α : Type u_2} (G : ) [] [] {a : α} [] [DecidableRel G.Adj] :
(Finset.sum Finset.univ fun e => ) = ↑()
theorem SimpleGraph.incMatrix_mul_transpose_diag {R : Type u_1} {α : Type u_2} (G : ) [] [] {a : α} [] [DecidableRel G.Adj] :
(Matrix α (Sym2 α) R * Matrix (Sym2 α) α R) (Matrix α α R) Matrix.instHMulMatrixMatrixMatrix () () a a = ↑()
theorem SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : ) [] [] {e : Sym2 α} :
(Finset.sum Finset.univ fun a => ) = 2
theorem SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : ) [] [] {e : Sym2 α} (h : ) :
(Finset.sum Finset.univ fun a => ) = 0
theorem SimpleGraph.incMatrix_transpose_mul_diag {R : Type u_1} {α : Type u_2} (G : ) [] [] {e : Sym2 α} [DecidableRel G.Adj] :
(Matrix (Sym2 α) α R * Matrix α (Sym2 α) R) (Matrix (Sym2 α) (Sym2 α) R) Matrix.instHMulMatrixMatrixMatrix () () e e = if 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 : ) :
(Matrix α (Sym2 α) R * Matrix (Sym2 α) α R) (Matrix α α R) Matrix.instHMulMatrixMatrixMatrix () () a b = 1
theorem SimpleGraph.incMatrix_mul_transpose {R : Type u_1} {α : Type u_2} (G : ) [Fintype (Sym2 α)] [] [] [] [DecidableRel G.Adj] :
= fun a b => if a = b then ↑() else if then 1 else 0