mathlibdocumentation

combinatorics.simple_graph.inc_matrix

Incidence matrix of a simple graph #

This file defines the unoriented incidence matrix of a simple graph.

Main definitions #

• simple_graph.inc_matrix: G.inc_matrix R is the incidence matrix of G over the ring R.

Main results #

• simple_graph.inc_matrix_mul_transpose_diag: The diagonal entries of the product of G.inc_matrix R and its transpose are the degrees of the vertices.
• simple_graph.inc_matrix_mul_transpose: Gives a complete description of the product of G.inc_matrix 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.
• simple_graph.inc_matrix_transpose_mul_diag: The diagonal entries of the product of the transpose of G.inc_matrix 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 simple_graph α 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 simple_graph.inc_matrix (R : Type u_1) {α : Type u_2} (G : simple_graph α) [has_zero R] [has_one R] :
(sym2 α) R

G.inc_matrix R is the α × sym2 α matrix whose (a, e)-entry is 1 if e is incident to a and 0 otherwise.

Equations
theorem simple_graph.inc_matrix_apply {R : Type u_1} {α : Type u_2} (G : simple_graph α) [has_zero R] [has_one R] {a : α} {e : sym2 α} :
theorem simple_graph.inc_matrix_apply' {R : Type u_1} {α : Type u_2} (G : simple_graph α) [has_zero R] [has_one R] [decidable_eq α] [decidable_rel G.adj] {a : α} {e : sym2 α} :
e = ite (e G.incidence_set a) 1 0

Entries of the incidence matrix can be computed given additional decidable instances.

theorem simple_graph.inc_matrix_apply_mul_inc_matrix_apply {R : Type u_1} {α : Type u_2} (G : simple_graph α) {a b : α} {e : sym2 α} :
theorem simple_graph.inc_matrix_apply_mul_inc_matrix_apply_of_not_adj {R : Type u_1} {α : Type u_2} (G : simple_graph α) {a b : α} {e : sym2 α} (hab : a b) (h : ¬G.adj a b) :
e * e = 0
theorem simple_graph.inc_matrix_of_not_mem_incidence_set {R : Type u_1} {α : Type u_2} (G : simple_graph α) {a : α} {e : sym2 α} (h : e ) :
e = 0
theorem simple_graph.inc_matrix_of_mem_incidence_set {R : Type u_1} {α : Type u_2} (G : simple_graph α) {a : α} {e : sym2 α} (h : e ) :
e = 1
theorem simple_graph.inc_matrix_apply_eq_zero_iff {R : Type u_1} {α : Type u_2} (G : simple_graph α) {a : α} {e : sym2 α} [nontrivial R] :
e = 0 e
theorem simple_graph.inc_matrix_apply_eq_one_iff {R : Type u_1} {α : Type u_2} (G : simple_graph α) {a : α} {e : sym2 α} [nontrivial R] :
e = 1 e
theorem simple_graph.sum_inc_matrix_apply {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype α] {a : α} [decidable_eq α] [decidable_rel G.adj] :
finset.univ.sum (λ (e : sym2 α), e) = (G.degree a)
theorem simple_graph.inc_matrix_mul_transpose_diag {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype α] {a : α} [decidable_eq α] [decidable_rel G.adj] :
a a = (G.degree a)
theorem simple_graph.sum_inc_matrix_apply_of_mem_edge_set {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype α] {e : sym2 α} :
e G.edge_setfinset.univ.sum (λ (a : α), e) = 2
theorem simple_graph.sum_inc_matrix_apply_of_not_mem_edge_set {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype α] {e : sym2 α} (h : e G.edge_set) :
finset.univ.sum (λ (a : α), e) = 0
theorem simple_graph.inc_matrix_transpose_mul_diag {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype α] {e : sym2 α} [decidable_rel G.adj] :
e e = ite (e G.edge_set) 2 0
theorem simple_graph.inc_matrix_mul_transpose_apply_of_adj {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype (sym2 α)] [semiring R] {a b : α} (h : G.adj a b) :
a b = 1
theorem simple_graph.inc_matrix_mul_transpose {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype (sym2 α)] [semiring R] [fintype α] [decidable_eq α] [decidable_rel G.adj] :
= λ (a b : α), ite (a = b) (G.degree a) (ite (G.adj a b) 1 0)