Documentation

Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Adjacency Matrices #

This module defines the adjacency matrix of a graph, and provides theorems connecting graph properties to computational properties of the matrix.

Main definitions #

structure Matrix.IsAdjMatrix {V : Type u_1} {α : Type u_2} [Zero α] [One α] (A : Matrix V V α) :

A : Matrix V V α is qualified as an "adjacency matrix" if (1) every entry of A is 0 or 1, (2) A is symmetric, (3) every diagonal entry of A is 0.

  • zero_or_one : ∀ (i j : V), A i j = 0 A i j = 1
  • symm : A.IsSymm
  • apply_diag : ∀ (i : V), A i i = 0
Instances For
    theorem Matrix.IsAdjMatrix.zero_or_one {V : Type u_1} {α : Type u_2} [Zero α] [One α] {A : Matrix V V α} (self : A.IsAdjMatrix) (i : V) (j : V) :
    A i j = 0 A i j = 1
    theorem Matrix.IsAdjMatrix.symm {V : Type u_1} {α : Type u_2} [Zero α] [One α] {A : Matrix V V α} (self : A.IsAdjMatrix) :
    A.IsSymm
    theorem Matrix.IsAdjMatrix.apply_diag {V : Type u_1} {α : Type u_2} [Zero α] [One α] {A : Matrix V V α} (self : A.IsAdjMatrix) (i : V) :
    A i i = 0
    @[simp]
    theorem Matrix.IsAdjMatrix.apply_diag_ne {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : A.IsAdjMatrix) (i : V) :
    ¬A i i = 1
    @[simp]
    theorem Matrix.IsAdjMatrix.apply_ne_one_iff {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : A.IsAdjMatrix) (i : V) (j : V) :
    ¬A i j = 1 A i j = 0
    @[simp]
    theorem Matrix.IsAdjMatrix.apply_ne_zero_iff {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : A.IsAdjMatrix) (i : V) (j : V) :
    ¬A i j = 0 A i j = 1
    @[simp]
    theorem Matrix.IsAdjMatrix.toGraph_adj {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : A.IsAdjMatrix) (i : V) (j : V) :
    h.toGraph.Adj i j = (A i j = 1)
    def Matrix.IsAdjMatrix.toGraph {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : A.IsAdjMatrix) :

    For A : Matrix V V α and h : IsAdjMatrix A, h.toGraph is the simple graph whose adjacency matrix is A.

    Equations
    • h.toGraph = { Adj := fun (i j : V) => A i j = 1, symm := , loopless := }
    Instances For
      instance Matrix.IsAdjMatrix.instDecidableRelAdjToGraphOfDecidableEq {V : Type u_1} {α : Type u_2} {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] [DecidableEq α] (h : A.IsAdjMatrix) :
      DecidableRel h.toGraph.Adj
      Equations
      • h.instDecidableRelAdjToGraphOfDecidableEq = id inferInstance
      def Matrix.compl {V : Type u_1} {α : Type u_2} [Zero α] [One α] [DecidableEq α] [DecidableEq V] (A : Matrix V V α) :
      Matrix V V α

      For A : Matrix V V α, A.compl is supposed to be the adjacency matrix of the complement graph of the graph induced by A.adjMatrix.

      Equations
      • A.compl i j = if i = j then 0 else if A i j = 0 then 1 else 0
      Instances For
        @[simp]
        theorem Matrix.compl_apply_diag {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (i : V) :
        A.compl i i = 0
        @[simp]
        theorem Matrix.compl_apply {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (i : V) (j : V) :
        A.compl i j = 0 A.compl i j = 1
        @[simp]
        theorem Matrix.isSymm_compl {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (h : A.IsSymm) :
        A.compl.IsSymm
        @[simp]
        theorem Matrix.isAdjMatrix_compl {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] (A : Matrix V V α) [Zero α] [One α] (h : A.IsSymm) :
        A.compl.IsAdjMatrix
        @[simp]
        theorem Matrix.IsAdjMatrix.compl {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] {A : Matrix V V α} [Zero α] [One α] (h : A.IsAdjMatrix) :
        A.compl.IsAdjMatrix
        theorem Matrix.IsAdjMatrix.toGraph_compl_eq {V : Type u_1} {α : Type u_2} [DecidableEq α] [DecidableEq V] {A : Matrix V V α} [MulZeroOneClass α] [Nontrivial α] (h : A.IsAdjMatrix) :
        .toGraph = h.toGraph
        def SimpleGraph.adjMatrix {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [DecidableRel G.Adj] [Zero α] [One α] :
        Matrix V V α

        adjMatrix G α is the matrix A such that A i j = (1 : α) if i and j are adjacent in the simple graph G, and otherwise A i j = 0.

        Equations
        Instances For
          @[simp]
          theorem SimpleGraph.adjMatrix_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (w : V) [Zero α] [One α] :
          SimpleGraph.adjMatrix α G v w = if G.Adj v w then 1 else 0
          @[simp]
          theorem SimpleGraph.transpose_adjMatrix {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Zero α] [One α] :
          @[simp]
          theorem SimpleGraph.isSymm_adjMatrix {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Zero α] [One α] :
          (SimpleGraph.adjMatrix α G).IsSymm
          @[simp]
          theorem SimpleGraph.isAdjMatrix_adjMatrix {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [DecidableRel G.Adj] [Zero α] [One α] :
          (SimpleGraph.adjMatrix α G).IsAdjMatrix

          The adjacency matrix of G is an adjacency matrix.

          theorem SimpleGraph.toGraph_adjMatrix_eq {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [DecidableRel G.Adj] [MulZeroOneClass α] [Nontrivial α] :
          .toGraph = G

          The graph induced by the adjacency matrix of G is G itself.

          theorem SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [DecidableEq α] [NonAssocSemiring α] :
          1 + SimpleGraph.adjMatrix α G + (SimpleGraph.adjMatrix α G).compl = Matrix.of fun (x x : V) => 1

          The sum of the identity, the adjacency matrix, and its complement is the all-ones matrix.

          @[simp]
          theorem SimpleGraph.adjMatrix_dotProduct {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : Vα) :
          Matrix.dotProduct (SimpleGraph.adjMatrix α G v) vec = uG.neighborFinset v, vec u
          @[simp]
          theorem SimpleGraph.dotProduct_adjMatrix {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : Vα) :
          Matrix.dotProduct vec (SimpleGraph.adjMatrix α G v) = uG.neighborFinset v, vec u
          @[simp]
          theorem SimpleGraph.adjMatrix_mulVec_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : Vα) :
          (SimpleGraph.adjMatrix α G).mulVec vec v = uG.neighborFinset v, vec u
          @[simp]
          theorem SimpleGraph.adjMatrix_vecMul_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (v : V) (vec : Vα) :
          Matrix.vecMul vec (SimpleGraph.adjMatrix α G) v = uG.neighborFinset v, vec u
          @[simp]
          theorem SimpleGraph.adjMatrix_mul_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (M : Matrix V V α) (v : V) (w : V) :
          (SimpleGraph.adjMatrix α G * M) v w = uG.neighborFinset v, M u w
          @[simp]
          theorem SimpleGraph.mul_adjMatrix_apply {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (M : Matrix V V α) (v : V) (w : V) :
          (M * SimpleGraph.adjMatrix α G) v w = uG.neighborFinset w, M v u
          @[simp]
          theorem SimpleGraph.trace_adjMatrix {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [AddCommMonoid α] [One α] :
          (SimpleGraph.adjMatrix α G).trace = 0
          theorem SimpleGraph.adjMatrix_mul_self_apply_self {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (i : V) :
          (SimpleGraph.adjMatrix α G * SimpleGraph.adjMatrix α G) i i = (G.degree i)
          theorem SimpleGraph.adjMatrix_mulVec_const_apply {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] {a : α} {v : V} :
          (SimpleGraph.adjMatrix α G).mulVec (Function.const V a) v = (G.degree v) * a
          theorem SimpleGraph.adjMatrix_mulVec_const_apply_of_regular {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] {d : } {a : α} (hd : G.IsRegularOfDegree d) {v : V} :
          (SimpleGraph.adjMatrix α G).mulVec (Function.const V a) v = d * a
          theorem SimpleGraph.adjMatrix_pow_apply_eq_card_walk {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] [DecidableEq V] [Semiring α] (n : ) (u : V) (v : V) :
          (SimpleGraph.adjMatrix α G ^ n) u v = (Fintype.card {p : G.Walk u v | p.length = n})
          theorem SimpleGraph.dotProduct_mulVec_adjMatrix {V : Type u_1} {α : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype V] [NonAssocSemiring α] (x : Vα) (y : Vα) :
          Matrix.dotProduct x ((SimpleGraph.adjMatrix α G).mulVec y) = i : V, j : V, if G.Adj i j then x i * y j else 0
          theorem Matrix.IsAdjMatrix.adjMatrix_toGraph_eq {V : Type u_1} {α : Type u_2} [MulZeroOneClass α] [Nontrivial α] {A : Matrix V V α} (h : A.IsAdjMatrix) [DecidableEq α] :
          SimpleGraph.adjMatrix α h.toGraph = A

          If A is qualified as an adjacency matrix, then the adjacency matrix of the graph induced by A is itself.