mathlib documentation

combinatorics.simple_graph.inc_matrix

Incidence matrix of a simple graph #

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

Main definitions #

Main results #

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 #

noncomputable def simple_graph.inc_matrix (R : Type u_1) {α : Type u_2} (G : simple_graph α) [has_zero R] [has_one R] :
matrix α (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 α} :

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

theorem simple_graph.inc_matrix_apply_mul_inc_matrix_apply_of_not_adj {R : Type u_1} {α : Type u_2} (G : simple_graph α) [mul_zero_one_class R] {a b : α} {e : sym2 α} (hab : a b) (h : ¬G.adj a b) :
theorem simple_graph.inc_matrix_of_not_mem_incidence_set {R : Type u_1} {α : Type u_2} (G : simple_graph α) [mul_zero_one_class R] {a : α} {e : sym2 α} (h : e G.incidence_set a) :
theorem simple_graph.inc_matrix_of_mem_incidence_set {R : Type u_1} {α : Type u_2} (G : simple_graph α) [mul_zero_one_class R] {a : α} {e : sym2 α} (h : e G.incidence_set a) :
theorem simple_graph.inc_matrix_apply_eq_zero_iff {R : Type u_1} {α : Type u_2} (G : simple_graph α) [mul_zero_one_class R] {a : α} {e : sym2 α} [nontrivial R] :
theorem simple_graph.inc_matrix_apply_eq_one_iff {R : Type u_1} {α : Type u_2} (G : simple_graph α) [mul_zero_one_class R] {a : α} {e : sym2 α} [nontrivial R] :
theorem simple_graph.sum_inc_matrix_apply {R : Type u_1} {α : Type u_2} (G : simple_graph α) [fintype α] [non_assoc_semiring R] {a : α} [decidable_eq α] [decidable_rel G.adj] :
finset.univ.sum (λ (e : sym2 α), simple_graph.inc_matrix R G a e) = (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 α] [non_assoc_semiring R] {e : sym2 α} :
e G.edge_set finset.univ.sum (λ (a : α), simple_graph.inc_matrix R G 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 α] [non_assoc_semiring R] {e : sym2 α} (h : e G.edge_set) :
finset.univ.sum (λ (a : α), simple_graph.inc_matrix R G a e) = 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) :
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] :
(simple_graph.inc_matrix R G).mul (simple_graph.inc_matrix R G).transpose = λ (a b : α), ite (a = b) (G.degree a) (ite (G.adj a b) 1 0)