Documentation

Mathlib.Combinatorics.SimpleGraph.IncMatrix

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 SimpleGraph α has the same type.

TODO #

noncomputable def SimpleGraph.incMatrix (R : Type u_1) {α : Type u_2} (G : SimpleGraph α) [Zero R] [One R] :
Matrix α (Sym2 α) R

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

Instances For
    theorem SimpleGraph.incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Zero R] [One R] {a : α} {e : Sym2 α} :
    theorem SimpleGraph.incMatrix_apply' {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e : Sym2 α} :
    SimpleGraph.incMatrix R G a e = if e SimpleGraph.incidenceSet G a then 1 else 0

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

    theorem SimpleGraph.incMatrix_apply_mul_incMatrix_apply_of_not_adj {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] {a : α} {b : α} {e : Sym2 α} (hab : a b) (h : ¬SimpleGraph.Adj G a b) :
    theorem SimpleGraph.incMatrix_of_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] {a : α} {e : Sym2 α} (h : e SimpleGraph.incidenceSet G a) :
    theorem SimpleGraph.sum_incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype α] [NonAssocSemiring R] {a : α} [DecidableEq α] [DecidableRel G.Adj] :
    (Finset.sum Finset.univ fun e => SimpleGraph.incMatrix R G a e) = ↑(SimpleGraph.degree G a)
    theorem SimpleGraph.incMatrix_mul_transpose_diag {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype α] [NonAssocSemiring R] {a : α} [DecidableEq α] [DecidableRel G.Adj] :
    (Matrix α (Sym2 α) R * Matrix (Sym2 α) α R) (Matrix α α R) Matrix.instHMulMatrixMatrixMatrix (SimpleGraph.incMatrix R G) (Matrix.transpose (SimpleGraph.incMatrix R G)) a a = ↑(SimpleGraph.degree G a)
    theorem SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype α] [NonAssocSemiring R] {e : Sym2 α} :
    e SimpleGraph.edgeSet G(Finset.sum Finset.univ fun a => SimpleGraph.incMatrix R G a e) = 2
    theorem SimpleGraph.sum_incMatrix_apply_of_not_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype α] [NonAssocSemiring R] {e : Sym2 α} (h : ¬e SimpleGraph.edgeSet G) :
    (Finset.sum Finset.univ fun a => SimpleGraph.incMatrix R G a e) = 0
    theorem SimpleGraph.incMatrix_transpose_mul_diag {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype α] [NonAssocSemiring R] {e : Sym2 α} [DecidableRel G.Adj] :
    (Matrix (Sym2 α) α R * Matrix α (Sym2 α) R) (Matrix (Sym2 α) (Sym2 α) R) Matrix.instHMulMatrixMatrixMatrix (Matrix.transpose (SimpleGraph.incMatrix R G)) (SimpleGraph.incMatrix R G) e e = if e SimpleGraph.edgeSet G then 2 else 0
    theorem SimpleGraph.incMatrix_mul_transpose_apply_of_adj {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype (Sym2 α)] [Semiring R] {a : α} {b : α} (h : SimpleGraph.Adj G a b) :
    (Matrix α (Sym2 α) R * Matrix (Sym2 α) α R) (Matrix α α R) Matrix.instHMulMatrixMatrixMatrix (SimpleGraph.incMatrix R G) (Matrix.transpose (SimpleGraph.incMatrix R G)) a b = 1
    theorem SimpleGraph.incMatrix_mul_transpose {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype (Sym2 α)] [Semiring R] [Fintype α] [DecidableEq α] [DecidableRel G.Adj] :
    SimpleGraph.incMatrix R G * Matrix.transpose (SimpleGraph.incMatrix R G) = fun a b => if a = b then ↑(SimpleGraph.degree G a) else if SimpleGraph.Adj G a b then 1 else 0