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
adj_matrixis the adjacency matrix of asimple_graphwith coefficients in a given semiring.
def
simple_graph.adj_matrix
{α : Type u}
[fintype α]
(R : Type v)
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj] :
matrix α α R
adj_matrix G R is the matrix A such that A i j = (1 : R) if i and j are
adjacent in the simple graph G, and otherwise A i j = 0.
Equations
- simple_graph.adj_matrix R G i j = ite (G.adj i j) 1 0
@[simp]
theorem
simple_graph.adj_matrix_apply
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(v w : α) :
simple_graph.adj_matrix R G v w = ite (G.adj v w) 1 0
@[simp]
theorem
simple_graph.transpose_adj_matrix
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj] :
(simple_graph.adj_matrix R G)ᵀ = simple_graph.adj_matrix R G
@[simp]
theorem
simple_graph.adj_matrix_dot_product
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(v : α)
(vec : α → R) :
matrix.dot_product (simple_graph.adj_matrix R G v) vec = ∑ (u : α) in G.neighbor_finset v, vec u
@[simp]
theorem
simple_graph.dot_product_adj_matrix
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(v : α)
(vec : α → R) :
matrix.dot_product vec (simple_graph.adj_matrix R G v) = ∑ (u : α) in G.neighbor_finset v, vec u
@[simp]
theorem
simple_graph.adj_matrix_mul_vec_apply
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(v : α)
(vec : α → R) :
(simple_graph.adj_matrix R G).mul_vec vec v = ∑ (u : α) in G.neighbor_finset v, vec u
@[simp]
theorem
simple_graph.adj_matrix_vec_mul_apply
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(v : α)
(vec : α → R) :
matrix.vec_mul vec (simple_graph.adj_matrix R G) v = ∑ (u : α) in G.neighbor_finset v, vec u
@[simp]
theorem
simple_graph.adj_matrix_mul_apply
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(M : matrix α α R)
(v w : α) :
(simple_graph.adj_matrix R G ⬝ M) v w = ∑ (u : α) in G.neighbor_finset v, M u w
@[simp]
theorem
simple_graph.mul_adj_matrix_apply
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(M : matrix α α R)
(v w : α) :
(M ⬝ simple_graph.adj_matrix R G) v w = ∑ (u : α) in G.neighbor_finset w, M v u
theorem
simple_graph.trace_adj_matrix
{α : Type u}
[fintype α]
(R : Type v)
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj] :
⇑(matrix.trace α R R) (simple_graph.adj_matrix R G) = 0
theorem
simple_graph.adj_matrix_mul_self_apply_self
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
(G : simple_graph α)
[decidable_rel G.adj]
(i : α) :
(simple_graph.adj_matrix R G ⬝ simple_graph.adj_matrix R G) i i = ↑(G.degree i)
@[simp]
theorem
simple_graph.adj_matrix_mul_vec_const_apply
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
{G : simple_graph α}
[decidable_rel G.adj]
{r : R}
{v : α} :
(simple_graph.adj_matrix R G).mul_vec (function.const α r) v = (↑(G.degree v)) * r
theorem
simple_graph.adj_matrix_mul_vec_const_apply_of_regular
{α : Type u}
[fintype α]
{R : Type v}
[semiring R]
{G : simple_graph α}
[decidable_rel G.adj]
{d : ℕ}
{r : R}
(hd : G.is_regular_of_degree d)
{v : α} :
(simple_graph.adj_matrix R G).mul_vec (function.const α r) v = (↑d) * r