Adjacency Matrices #

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.

source

structure Matrix.IsAdjMatrix {V : Type u_1} {α : Type u_2} [Zero α] [One α] (A : Matrix V V α) :

Prop

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.

zero_or_one : ∀ (i j : V), A i j = 0 ∨ A i j = 1
symm : Matrix.IsSymm A
apply_diag : ∀ (i : V), A i i = 0

Instances For

source

@[simp]

theorem Matrix.IsAdjMatrix.apply_diag_ne {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : Matrix.IsAdjMatrix A) (i : V) :

¬A i i = 1

source

@[simp]

theorem Matrix.IsAdjMatrix.apply_ne_one_iff {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : Matrix.IsAdjMatrix A) (i : V) (j : V) :

¬A i j = 1 ↔ A i j = 0

source

@[simp]

theorem Matrix.IsAdjMatrix.apply_ne_zero_iff {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : Matrix.IsAdjMatrix A) (i : V) (j : V) :

¬A i j = 0 ↔ A i j = 1

source

@[simp]

theorem Matrix.IsAdjMatrix.toGraph_adj {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : Matrix.IsAdjMatrix A) (i : V) (j : V) :

(Matrix.IsAdjMatrix.toGraph h).Adj i j = (A i j = 1)

source

def Matrix.IsAdjMatrix.toGraph {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : Matrix.IsAdjMatrix A) :

SimpleGraph V

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

Equations

Matrix.IsAdjMatrix.toGraph h = SimpleGraph.mk fun (i j : V) => A i j = 1

Instances For

source

instance Matrix.IsAdjMatrix.instDecidableRelAdjToGraph {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] [DecidableEq α] (h : Matrix.IsAdjMatrix A) :

DecidableRel (Matrix.IsAdjMatrix.toGraph h).Adj

Equations

Matrix.IsAdjMatrix.instDecidableRelAdjToGraph h = id inferInstance

source

def Matrix.compl {V : Type u_1} {α : Type u_2} [Zero α] [One α] [DecidableEq α] [DecidableEq V] (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.

Equations

Matrix.compl A i j = if i = j then 0 else if A i j = 0 then 1 else 0

Instances For

source

@[simp]

theorem Matrix.compl_apply_diag {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (i : V) :

Matrix.compl A i i = 0

source

@[simp]

theorem Matrix.compl_apply {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (i : V) (j : V) :

Matrix.compl A i j = 0 ∨ Matrix.compl A i j = 1

source

@[simp]

theorem Matrix.isSymm_compl {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (h : Matrix.IsSymm A) :

Matrix.IsSymm (Matrix.compl A)

source

@[simp]

theorem Matrix.isAdjMatrix_compl {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (h : Matrix.IsSymm A) :

Matrix.IsAdjMatrix (Matrix.compl A)

source

@[simp]

theorem Matrix.IsAdjMatrix.compl {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] {A : Matrix V V α} [Zero α] [One α] (h : Matrix.IsAdjMatrix A) :

Matrix.IsAdjMatrix (Matrix.compl A)

source

theorem Matrix.IsAdjMatrix.toGraph_compl_eq {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : Matrix.IsAdjMatrix A) :

Matrix.IsAdjMatrix.toGraph (_ : Matrix.IsAdjMatrix (Matrix.compl A)) = (Matrix.IsAdjMatrix.toGraph h)ᶜ

source

def SimpleGraph.adjMatrix {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [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.

Equations

SimpleGraph.adjMatrix α G = Matrix.of fun (i j : V) => if G.Adj i j then 1 else 0

Instances For

source

@[simp]

theorem SimpleGraph.adjMatrix_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (w : V) [Zero α] [One α] :

SimpleGraph.adjMatrix α G v w = if G.Adj v w then 1 else 0

source

@[simp]

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

Matrix.transpose (SimpleGraph.adjMatrix α G) = SimpleGraph.adjMatrix α G

source

@[simp]

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

Matrix.IsSymm (SimpleGraph.adjMatrix α G)

source

@[simp]

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

Matrix.IsAdjMatrix (SimpleGraph.adjMatrix α G)

The adjacency matrix of G is an adjacency matrix.

source

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

Matrix.IsAdjMatrix.toGraph (_ : Matrix.IsAdjMatrix (SimpleGraph.adjMatrix α G)) = G

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

source

@[simp]

theorem SimpleGraph.adjMatrix_dotProduct {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : V → α) :

Matrix.dotProduct (SimpleGraph.adjMatrix α G v) vec = Finset.sum (SimpleGraph.neighborFinset G v) fun (u : V) => vec u

source

@[simp]

theorem SimpleGraph.dotProduct_adjMatrix {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : V → α) :

Matrix.dotProduct vec (SimpleGraph.adjMatrix α G v) = Finset.sum (SimpleGraph.neighborFinset G v) fun (u : V) => vec u

source

@[simp]

theorem SimpleGraph.adjMatrix_mulVec_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : V → α) :

Matrix.mulVec (SimpleGraph.adjMatrix α G) vec v = Finset.sum (SimpleGraph.neighborFinset G v) fun (u : V) => vec u

source

@[simp]

theorem SimpleGraph.adjMatrix_vecMul_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : V → α) :

Matrix.vecMul vec (SimpleGraph.adjMatrix α G) v = Finset.sum (SimpleGraph.neighborFinset G v) fun (u : V) => vec u

source

@[simp]

theorem SimpleGraph.adjMatrix_mul_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (M : Matrix V V α) (v : V) (w : V) :

(SimpleGraph.adjMatrix α G * M) v w = Finset.sum (SimpleGraph.neighborFinset G v) fun (u : V) => M u w

source

@[simp]

theorem SimpleGraph.mul_adjMatrix_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (M : Matrix V V α) (v : V) (w : V) :

(M * SimpleGraph.adjMatrix α G) v w = Finset.sum (SimpleGraph.neighborFinset G w) fun (u : V) => M v u

source

@[simp]

theorem SimpleGraph.trace_adjMatrix {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [AddCommMonoid α] [One α] :

Matrix.trace (SimpleGraph.adjMatrix α G) = 0

source

theorem SimpleGraph.adjMatrix_mul_self_apply_self {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (i : V) :

(SimpleGraph.adjMatrix α G * SimpleGraph.adjMatrix α G) i i = ↑(SimpleGraph.degree G i)

source

theorem SimpleGraph.adjMatrix_mulVec_const_apply {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] [Semiring α] {a : α} {v : V} :

Matrix.mulVec (SimpleGraph.adjMatrix α G) (Function.const V a) v = ↑(SimpleGraph.degree G v) * a

source

theorem SimpleGraph.adjMatrix_mulVec_const_apply_of_regular {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] [Semiring α] {d : ℕ} {a : α} (hd : SimpleGraph.IsRegularOfDegree G d) {v : V} :

Matrix.mulVec (SimpleGraph.adjMatrix α G) (Function.const V a) v = ↑d * a

source

theorem SimpleGraph.adjMatrix_pow_apply_eq_card_walk {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] [DecidableEq V] [Semiring α] (n : ℕ) (u : V) (v : V) :

(SimpleGraph.adjMatrix α G ^ n) u v = ↑(Fintype.card ↑{p : SimpleGraph.Walk G u v | SimpleGraph.Walk.length p = n})

source

theorem Matrix.IsAdjMatrix.adjMatrix_toGraph_eq {V : Type u_1} {α : Type u_2} [MulZeroOneClass α] [Nontrivial α] {A : Matrix V V α} (h : Matrix.IsAdjMatrix A) [DecidableEq α] :

SimpleGraph.adjMatrix α (Matrix.IsAdjMatrix.toGraph h) = A

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

Documentation

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Adjacency Matrices #

Main definitions #