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.

Equations
Instances For
    theorem SimpleGraph.incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Zero R] [One R] {a : α} {e : Sym2 α} :
    SimpleGraph.incMatrix R G a e = (G.incidenceSet a).indicator 1 e
    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 G.incidenceSet a then 1 else 0

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

    theorem SimpleGraph.incMatrix_apply_mul_incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] {a : α} {b : α} {e : Sym2 α} :
    SimpleGraph.incMatrix R G a e * SimpleGraph.incMatrix R G b e = (G.incidenceSet a G.incidenceSet b).indicator 1 e
    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 : ¬G.Adj a b) :
    theorem SimpleGraph.incMatrix_of_not_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] {a : α} {e : Sym2 α} (h : eG.incidenceSet a) :
    theorem SimpleGraph.incMatrix_of_mem_incidenceSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] {a : α} {e : Sym2 α} (h : e G.incidenceSet a) :
    theorem SimpleGraph.incMatrix_apply_eq_zero_iff {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] {a : α} {e : Sym2 α} [Nontrivial R] :
    SimpleGraph.incMatrix R G a e = 0 eG.incidenceSet a
    theorem SimpleGraph.incMatrix_apply_eq_one_iff {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [MulZeroOneClass R] {a : α} {e : Sym2 α} [Nontrivial R] :
    SimpleGraph.incMatrix R G a e = 1 e G.incidenceSet a
    theorem SimpleGraph.sum_incMatrix_apply {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] {a : α} [Fintype (Sym2 α)] [Fintype (G.neighborSet a)] :
    e : Sym2 α, SimpleGraph.incMatrix R G a e = (G.degree a)
    theorem SimpleGraph.incMatrix_mul_transpose_diag {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] {a : α} [Fintype (Sym2 α)] [Fintype (G.neighborSet a)] :
    (SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G).transpose) a a = (G.degree a)
    theorem SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] {e : Sym2 α} [Fintype α] :
    e G.edgeSeta : α, 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 α) [NonAssocSemiring R] {e : Sym2 α} [Fintype α] (h : eG.edgeSet) :
    a : α, SimpleGraph.incMatrix R G a e = 0
    theorem SimpleGraph.incMatrix_transpose_mul_diag {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [NonAssocSemiring R] {e : Sym2 α} [Fintype α] [Decidable (e G.edgeSet)] :
    ((SimpleGraph.incMatrix R G).transpose * SimpleGraph.incMatrix R G) e e = if e G.edgeSet 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 : G.Adj a b) :
    (SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G).transpose) a b = 1
    theorem SimpleGraph.incMatrix_mul_transpose {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [Fintype (Sym2 α)] [Semiring R] [(a : α) → Fintype (G.neighborSet a)] [DecidableEq α] [DecidableRel G.Adj] :
    SimpleGraph.incMatrix R G * (SimpleGraph.incMatrix R G).transpose = fun (a b : α) => if a = b then (G.degree a) else if G.Adj a b then 1 else 0