Incidence matrix of a simple graph #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the unoriented incidence matrix of a simple graph.
Main definitions #
simple_graph.inc_matrix:G.inc_matrix Ris the incidence matrix ofGover the ringR.
Main results #
simple_graph.inc_matrix_mul_transpose_diag: The diagonal entries of the product ofG.inc_matrix Rand its transpose are the degrees of the vertices.simple_graph.inc_matrix_mul_transpose: Gives a complete description of the product ofG.inc_matrix Rand 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 ofG.inc_matrix RandG.inc_matrix Rare2or0depending on whether or not the unordered pair is an edge ofG.
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] :
G.inc_matrix R is the α × sym2 α matrix whose (a, e)-entry is 1 if e is incident to
a and 0 otherwise.
Equations
- simple_graph.inc_matrix R G = λ (a : α), (G.incidence_set a).indicator 1
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 α} :
simple_graph.inc_matrix R G a e = (G.incidence_set a).indicator 1 e
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 α} :
simple_graph.inc_matrix R G a 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 α)
[mul_zero_one_class R]
{a b : α}
{e : sym2 α} :
simple_graph.inc_matrix R G a e * simple_graph.inc_matrix R G b e = (G.incidence_set a ∩ G.incidence_set b).indicator 1 e
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) :
simple_graph.inc_matrix R G a e * simple_graph.inc_matrix R G b e = 0
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) :
simple_graph.inc_matrix R G a e = 0
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) :
simple_graph.inc_matrix R G a e = 1
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] :
simple_graph.inc_matrix R G a e = 0 ↔ e ∉ G.incidence_set a
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] :
simple_graph.inc_matrix R G a e = 1 ↔ e ∈ G.incidence_set a
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.inc_matrix_mul_transpose_diag
{R : Type u_1}
{α : Type u_2}
(G : simple_graph α)
[fintype α]
[non_assoc_semiring R]
{a : α}
[decidable_eq α]
[decidable_rel G.adj] :
(simple_graph.inc_matrix R G).mul (simple_graph.inc_matrix R G).transpose 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 α]
[non_assoc_semiring R]
{e : sym2 α} :
e ∈ ⇑simple_graph.edge_set G → 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 ∉ ⇑simple_graph.edge_set G) :
finset.univ.sum (λ (a : α), simple_graph.inc_matrix R G a e) = 0
theorem
simple_graph.inc_matrix_transpose_mul_diag
{R : Type u_1}
{α : Type u_2}
(G : simple_graph α)
[fintype α]
[non_assoc_semiring R]
{e : sym2 α}
[decidable_rel G.adj] :
(simple_graph.inc_matrix R G).transpose.mul (simple_graph.inc_matrix R G) e e = ite (e ∈ ⇑simple_graph.edge_set G) 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) :
(simple_graph.inc_matrix R G).mul (simple_graph.inc_matrix R G).transpose 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] :