Adjacency Matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

matrix.is_adj_matrix: 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.is_adj_matrix.to_graph: for A : matrix V V α and h : A.is_adj_matrix, 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.
simple_graph.adj_matrix: the adjacency matrix of a simple_graph.
simple_graph.adj_matrix_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.is_adj_matrix {V : Type u_1} {α : Type u_2} [has_zero α] [has_one α] (A : matrix V V α) :

Prop

zero_or_one : (∀ (i j : V), A i j = 0 ∨ A i j = 1) . "obviously"
symm : A.is_symm . "obviously"
apply_diag : (∀ (i : V), A i i = 0) . "obviously"

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.

source

@[simp]

theorem matrix.is_adj_matrix.apply_diag_ne {V : Type u_1} {α : Type u_2} {A : matrix V V α} [mul_zero_one_class α] [nontrivial α] (h : A.is_adj_matrix) (i : V) :

¬A i i = 1

source

@[simp]

theorem matrix.is_adj_matrix.apply_ne_one_iff {V : Type u_1} {α : Type u_2} {A : matrix V V α} [mul_zero_one_class α] [nontrivial α] (h : A.is_adj_matrix) (i j : V) :

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

source

@[simp]

theorem matrix.is_adj_matrix.apply_ne_zero_iff {V : Type u_1} {α : Type u_2} {A : matrix V V α} [mul_zero_one_class α] [nontrivial α] (h : A.is_adj_matrix) (i j : V) :

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

source

@[simp]

theorem matrix.is_adj_matrix.to_graph_adj {V : Type u_1} {α : Type u_2} {A : matrix V V α} [mul_zero_one_class α] [nontrivial α] (h : A.is_adj_matrix) (i j : V) :

h.to_graph.adj i j = (A i j = 1)

source

def matrix.is_adj_matrix.to_graph {V : Type u_1} {α : Type u_2} {A : matrix V V α} [mul_zero_one_class α] [nontrivial α] (h : A.is_adj_matrix) :

simple_graph V

For A : matrix V V α and h : is_adj_matrix A, h.to_graph is the simple graph whose adjacency matrix is A.

Equations

h.to_graph = {adj := λ (i j : V), A i j = 1, symm := _, loopless := _}

source

@[protected, instance]

def matrix.is_adj_matrix.adj.decidable_rel {V : Type u_1} {α : Type u_2} {A : matrix V V α} [mul_zero_one_class α] [nontrivial α] [decidable_eq α] (h : A.is_adj_matrix) :

decidable_rel h.to_graph.adj

Equations

matrix.is_adj_matrix.adj.decidable_rel h = _.mpr (λ (a b : V), _inst_3 (A a b) 1)

source

def matrix.compl {V : Type u_1} {α : Type u_2} [has_zero α] [has_one α] [decidable_eq α] [decidable_eq 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.adj_matrix.

Equations

A.compl = λ (i j : V), ite (i = j) 0 (ite (A i j = 0) 1 0)

source

@[simp]

theorem matrix.compl_apply_diag {V : Type u_1} {α : Type u_2} [decidable_eq α] [decidable_eq V] (A : matrix V V α) [has_zero α] [has_one α] (i : V) :

A.compl i i = 0

source

@[simp]

theorem matrix.compl_apply {V : Type u_1} {α : Type u_2} [decidable_eq α] [decidable_eq V] (A : matrix V V α) [has_zero α] [has_one α] (i j : V) :

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

source

@[simp]

theorem matrix.is_symm_compl {V : Type u_1} {α : Type u_2} [decidable_eq α] [decidable_eq V] (A : matrix V V α) [has_zero α] [has_one α] (h : A.is_symm) :

A.compl.is_symm

source

@[simp]

theorem matrix.is_adj_matrix_compl {V : Type u_1} {α : Type u_2} [decidable_eq α] [decidable_eq V] (A : matrix V V α) [has_zero α] [has_one α] (h : A.is_symm) :

A.compl.is_adj_matrix

source

@[simp]

theorem matrix.is_adj_matrix.compl {V : Type u_1} {α : Type u_2} [decidable_eq α] [decidable_eq V] {A : matrix V V α} [has_zero α] [has_one α] (h : A.is_adj_matrix) :

A.compl.is_adj_matrix

source

theorem matrix.is_adj_matrix.to_graph_compl_eq {V : Type u_1} {α : Type u_2} [decidable_eq α] [decidable_eq V] {A : matrix V V α} [mul_zero_one_class α] [nontrivial α] (h : A.is_adj_matrix) :

_.to_graph = h.to_graph ᶜ

source

def simple_graph.adj_matrix {V : Type u_1} (α : Type u_2) (G : simple_graph V) [decidable_rel G.adj] [has_zero α] [has_one α] :

matrix V V α

adj_matrix 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

simple_graph.adj_matrix α G = ⇑matrix.of (λ (i j : V), ite (G.adj i j) 1 0)

source

@[simp]

theorem simple_graph.adj_matrix_apply {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] (v w : V) [has_zero α] [has_one α] :

simple_graph.adj_matrix α G v w = ite (G.adj v w) 1 0

source

@[simp]

theorem simple_graph.transpose_adj_matrix {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [has_zero α] [has_one α] :

(simple_graph.adj_matrix α G).transpose = simple_graph.adj_matrix α G

source

@[simp]

theorem simple_graph.is_symm_adj_matrix {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [has_zero α] [has_one α] :

(simple_graph.adj_matrix α G).is_symm

source

@[simp]

theorem simple_graph.is_adj_matrix_adj_matrix {V : Type u_1} (α : Type u_2) (G : simple_graph V) [decidable_rel G.adj] [has_zero α] [has_one α] :

(simple_graph.adj_matrix α G).is_adj_matrix

The adjacency matrix of G is an adjacency matrix.

source

theorem simple_graph.to_graph_adj_matrix_eq {V : Type u_1} (α : Type u_2) (G : simple_graph V) [decidable_rel G.adj] [mul_zero_one_class α] [nontrivial α] :

_.to_graph = G

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

source

@[simp]

theorem simple_graph.adj_matrix_dot_product {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [non_assoc_semiring α] (v : V) (vec : V → α) :

matrix.dot_product (simple_graph.adj_matrix α G v) vec = (G.neighbor_finset v).sum (λ (u : V), vec u)

source

@[simp]

theorem simple_graph.dot_product_adj_matrix {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [non_assoc_semiring α] (v : V) (vec : V → α) :

matrix.dot_product vec (simple_graph.adj_matrix α G v) = (G.neighbor_finset v).sum (λ (u : V), vec u)

source

@[simp]

theorem simple_graph.adj_matrix_mul_vec_apply {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [non_assoc_semiring α] (v : V) (vec : V → α) :

(simple_graph.adj_matrix α G).mul_vec vec v = (G.neighbor_finset v).sum (λ (u : V), vec u)

source

@[simp]

theorem simple_graph.adj_matrix_vec_mul_apply {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [non_assoc_semiring α] (v : V) (vec : V → α) :

matrix.vec_mul vec (simple_graph.adj_matrix α G) v = (G.neighbor_finset v).sum (λ (u : V), vec u)

source

@[simp]

theorem simple_graph.adj_matrix_mul_apply {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [non_assoc_semiring α] (M : matrix V V α) (v w : V) :

(simple_graph.adj_matrix α G).mul M v w = (G.neighbor_finset v).sum (λ (u : V), M u w)

source

@[simp]

theorem simple_graph.mul_adj_matrix_apply {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [non_assoc_semiring α] (M : matrix V V α) (v w : V) :

M.mul (simple_graph.adj_matrix α G) v w = (G.neighbor_finset w).sum (λ (u : V), M v u)

source

@[simp]

theorem simple_graph.trace_adj_matrix {V : Type u_1} (α : Type u_2) (G : simple_graph V) [decidable_rel G.adj] [fintype V] [add_comm_monoid α] [has_one α] :

(simple_graph.adj_matrix α G).trace = 0

source

theorem simple_graph.adj_matrix_mul_self_apply_self {V : Type u_1} {α : Type u_2} (G : simple_graph V) [decidable_rel G.adj] [fintype V] [non_assoc_semiring α] (i : V) :

(simple_graph.adj_matrix α G).mul (simple_graph.adj_matrix α G) i i = ↑(G.degree i)

source

@[simp]

theorem simple_graph.adj_matrix_mul_vec_const_apply {V : Type u_1} {α : Type u_2} {G : simple_graph V} [decidable_rel G.adj] [fintype V] [semiring α] {a : α} {v : V} :

(simple_graph.adj_matrix α G).mul_vec (function.const V a) v = ↑(G.degree v) * a

source

theorem simple_graph.adj_matrix_mul_vec_const_apply_of_regular {V : Type u_1} {α : Type u_2} {G : simple_graph V} [decidable_rel G.adj] [fintype V] [semiring α] {d : ℕ} {a : α} (hd : G.is_regular_of_degree d) {v : V} :

(simple_graph.adj_matrix α G).mul_vec (function.const V a) v = ↑d * a

source

theorem simple_graph.adj_matrix_pow_apply_eq_card_walk {V : Type u_1} {α : Type u_2} {G : simple_graph V} [decidable_rel G.adj] [fintype V] [decidable_eq V] [semiring α] (n : ℕ) (u v : V) :

(simple_graph.adj_matrix α G ^ n) u v = ↑(fintype.card ↥{p : G.walk u v | p.length = n})

source

theorem matrix.is_adj_matrix.adj_matrix_to_graph_eq {V : Type u_1} {α : Type u_2} [mul_zero_one_class α] [nontrivial α] {A : matrix V V α} (h : A.is_adj_matrix) [decidable_eq α] :

simple_graph.adj_matrix α h.to_graph = A

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