# Documentation

This module defines the adjacency matrix of a graph, and provides theorems connecting graph properties to computational properties of the matrix.

## Main definitions #

• Matrix.IsAdjMatrix: A : Matrix V V α is qualified as an "adjacency matrix" if (1) every entry of A is 0 or 1, (2) A is symmetric, (3) every diagonal entry of A is 0.

• Matrix.IsAdjMatrix.to_graph: for A : Matrix V V α and h : A.IsAdjMatrix, h.to_graph is the simple graph induced by A.

• Matrix.compl: for A : Matrix V V α, A.compl is supposed to be the adjacency matrix of the complement graph of the graph induced by A.

• SimpleGraph.adjMatrix: the adjacency matrix of a SimpleGraph.

• SimpleGraph.adjMatrix_pow_apply_eq_card_walk: each entry of the nth power of a graph's adjacency matrix counts the number of length-n walks between the corresponding pair of vertices.

structure Matrix.IsAdjMatrix {V : Type u_1} {α : Type u_2} [Zero α] [One α] (A : Matrix V V α) :
• zero_or_one : ∀ (i j : V), A i j = 0 A i j = 1
• symm :
• apply_diag : ∀ (i : V), A i i = 0

A : Matrix V V α is qualified as an "adjacency matrix" if (1) every entry of A is 0 or 1, (2) A is symmetric, (3) every diagonal entry of A is 0.

Instances For
@[simp]
theorem Matrix.IsAdjMatrix.apply_diag_ne {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [] [] (h : ) (i : V) :
¬A i i = 1
@[simp]
theorem Matrix.IsAdjMatrix.apply_ne_one_iff {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [] [] (h : ) (i : V) (j : V) :
¬A i j = 1 A i j = 0
@[simp]
theorem Matrix.IsAdjMatrix.apply_ne_zero_iff {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [] [] (h : ) (i : V) (j : V) :
¬A i j = 0 A i j = 1
@[simp]
theorem Matrix.IsAdjMatrix.toGraph_Adj {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [] [] (h : ) (i : V) (j : V) :
= (A i j = 1)
def Matrix.IsAdjMatrix.toGraph {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [] [] (h : ) :

For A : Matrix V V α and h : IsAdjMatrix A, h.toGraph is the simple graph whose adjacency matrix is A.

Instances For
instance Matrix.IsAdjMatrix.instDecidableRelAdjToGraph {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [] [] [] (h : ) :
def Matrix.compl {V : Type u_1} {α : Type u_2} [Zero α] [One α] [] [] (A : Matrix V V α) :
Matrix V V α

For A : Matrix V V α, A.compl is supposed to be the adjacency matrix of the complement graph of the graph induced by A.adjMatrix.

Instances For
@[simp]
theorem Matrix.compl_apply_diag {V : Type u_1} {α : Type u_2} [] [] (A : Matrix V V α) [Zero α] [One α] (i : V) :
Matrix.compl A i i = 0
@[simp]
theorem Matrix.compl_apply {V : Type u_1} {α : Type u_2} [] [] (A : Matrix V V α) [Zero α] [One α] (i : V) (j : V) :
Matrix.compl A i j = 0 Matrix.compl A i j = 1
@[simp]
theorem Matrix.isSymm_compl {V : Type u_1} {α : Type u_2} [] [] (A : Matrix V V α) [Zero α] [One α] (h : ) :
@[simp]
theorem Matrix.isAdjMatrix_compl {V : Type u_1} {α : Type u_2} [] [] (A : Matrix V V α) [Zero α] [One α] (h : ) :
@[simp]
theorem Matrix.IsAdjMatrix.compl {V : Type u_1} {α : Type u_2} [] [] {A : Matrix V V α} [Zero α] [One α] (h : ) :
theorem Matrix.IsAdjMatrix.toGraph_compl_eq {V : Type u_1} {α : Type u_2} [] [] {A : Matrix V V α} [] [] (h : ) :
def SimpleGraph.adjMatrix {V : Type u_1} (α : Type u_2) (G : ) [DecidableRel G.Adj] [Zero α] [One α] :
Matrix V V α

adjMatrix G α is the matrix A such that A i j = (1 : α) if i and j are adjacent in the simple graph G, and otherwise A i j = 0.

Instances For
@[simp]
theorem SimpleGraph.adjMatrix_apply {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] (v : V) (w : V) [Zero α] [One α] :
= if then 1 else 0
@[simp]
theorem SimpleGraph.transpose_adjMatrix {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [Zero α] [One α] :
@[simp]
theorem SimpleGraph.isSymm_adjMatrix {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [Zero α] [One α] :
@[simp]
theorem SimpleGraph.isAdjMatrix_adjMatrix {V : Type u_1} (α : Type u_2) (G : ) [DecidableRel G.Adj] [Zero α] [One α] :

The adjacency matrix of G is an adjacency matrix.

theorem SimpleGraph.toGraph_adjMatrix_eq {V : Type u_1} (α : Type u_2) (G : ) [DecidableRel G.Adj] [] [] :

The graph induced by the adjacency matrix of G is G itself.

@[simp]
theorem SimpleGraph.adjMatrix_dotProduct {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [] [] (v : V) (vec : Vα) :
Matrix.dotProduct () vec = Finset.sum () fun u => vec u
@[simp]
theorem SimpleGraph.dotProduct_adjMatrix {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [] [] (v : V) (vec : Vα) :
Matrix.dotProduct vec () = Finset.sum () fun u => vec u
@[simp]
theorem SimpleGraph.adjMatrix_mulVec_apply {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [] [] (v : V) (vec : Vα) :
Matrix.mulVec () vec v = Finset.sum () fun u => vec u
@[simp]
theorem SimpleGraph.adjMatrix_vecMul_apply {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [] [] (v : V) (vec : Vα) :
Matrix.vecMul vec () v = Finset.sum () fun u => vec u
@[simp]
theorem SimpleGraph.adjMatrix_mul_apply {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [] [] (M : Matrix V V α) (v : V) (w : V) :
(Matrix V V α * Matrix V V α) (Matrix V V α) Matrix.instHMulMatrixMatrixMatrix () M v w = Finset.sum () fun u => M u w
@[simp]
theorem SimpleGraph.mul_adjMatrix_apply {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [] [] (M : Matrix V V α) (v : V) (w : V) :
(Matrix V V α * Matrix V V α) (Matrix V V α) Matrix.instHMulMatrixMatrixMatrix M () v w = Finset.sum () fun u => M v u
@[simp]
theorem SimpleGraph.trace_adjMatrix {V : Type u_1} (α : Type u_2) (G : ) [DecidableRel G.Adj] [] [] [One α] :
theorem SimpleGraph.adjMatrix_mul_self_apply_self {V : Type u_1} {α : Type u_2} (G : ) [DecidableRel G.Adj] [] [] (i : V) :
(Matrix V V α * Matrix V V α) (Matrix V V α) Matrix.instHMulMatrixMatrixMatrix () () i i = ↑()
theorem SimpleGraph.adjMatrix_mulVec_const_apply {V : Type u_1} {α : Type u_2} {G : } [DecidableRel G.Adj] [] [] {a : α} {v : V} :
Matrix.mulVec () () v = ↑() * a
theorem SimpleGraph.adjMatrix_mulVec_const_apply_of_regular {V : Type u_1} {α : Type u_2} {G : } [DecidableRel G.Adj] [] [] {d : } {a : α} (hd : ) {v : V} :
Matrix.mulVec () () v = d * a
theorem SimpleGraph.adjMatrix_pow_apply_eq_card_walk {V : Type u_1} {α : Type u_2} {G : } [DecidableRel G.Adj] [] [] [] (n : ) (u : V) (v : V) :
(Matrix V V α ^ ) (Matrix V V α) instHPow () n u v = ↑(Fintype.card {p | })
theorem Matrix.IsAdjMatrix.adjMatrix_toGraph_eq {V : Type u_1} {α : Type u_2} [] [] {A : Matrix V V α} (h : ) [] :

If A is qualified as an adjacency matrix, then the adjacency matrix of the graph induced by A is itself.