Part 1 of 2

DefinitionAndrásfai graph#✓fully proved

For a natural number \(k\), the Andrásfai graph is the Cayley graph of the cyclic group \(\mathbb{Z}/(3k+2)\mathbb{Z}\) whose connection set \(C\) consists of the residues whose representative in \(\{0, 1, \dots, 3k+1\}\) is congruent to \(1\) modulo \(3\): two distinct residues \(x\) and \(y\) are adjacent when \(y - x \in C\) or \(x - y \in C\).

def andrasfaiGraph (k : ℕ) : SimpleGraph (ZMod (3 * k + 2)) :=
  SimpleGraph.addCayley (andrasfaiConnectionSet k)

DefinitionCayley digraph#✓fully proved

Let \(G\) be a set with a binary operation written as multiplication, and let \(C \subseteq G\). The Cayley digraph \(X(G, C)\) is the directed graph whose vertices are the elements of \(G\), with an arc \(u \to v\) exactly when \(v = uc\) for some \(c \in C\).

Usually \(G\) is a group and \(C\) does not contain the identity, so that \(X(G, C)\) has no loops; neither condition is imposed here.

def directedCayleyGraph {G : Type*} [Mul G] (S : Set G) : Digraph G where
  Adj := cayleyArc S

TheoremCayley's formula#✓fully proved

For every natural number \(n \ge 2\), the complete graph on \(n\) vertices has exactly \(n^{n-2}\) spanning trees.

theorem cayley_formula :
    ∀ {n : ℕ}, 2 ≤ n → numSpanningTrees (⊤ : _root_.SimpleGraph (Fin n)) = n ^ (n - 2)
Sources
  • A. Cayley, "A theorem on trees", Quarterly Journal of Pure and Applied Mathematics 23 (1889), 376-378.
Uses 2
Statement usesNumber of spanning trees
Proof usesSpanning tree

DefinitionCoxeter graph#✓fully proved

The Coxeter graph is the simple graph whose \(28\) vertices are the pairs \((i, j)\) with \(i \in \{0, 1, 2, 3\}\) and \(j \in \mathbb{Z}/7\mathbb{Z}\), and whose edges are the following: for each \(i \in \{1, 2, 3\}\), the vertices \((i, j)\) and \((i, j')\) are adjacent when \(j - j' = i\) or \(j' - j = i\) in \(\mathbb{Z}/7\mathbb{Z}\), and for each \(j\) the vertex \((0, j)\) is adjacent to \((1, j)\), \((2, j)\) and \((3, j)\). There are no other edges.

def coxeterGraph : SimpleGraph (Fin 4 × ZMod 7) :=
  SimpleGraph.fromRel fun a b =>
    (a.1 = b.1 ∧ a.1 ≠ 0 ∧ a.2 - b.2 = fin4ToZMod7 a.1)
    ∨
    (a.1 = 0 ∧ b.1 ≠ 0 ∧ a.2 = b.2)

DefinitionEdge-transposition graph#✓fully proved

Let \(n\) be a natural number and let \(T\) be a set of permutations of \(\{0, 1, \dots, n - 1\}\), typically a set of transpositions in the symmetric group \(S_n\). The edge-transposition graph of \(T\) is the simple graph with vertex set \(\{0, 1, \dots, n - 1\}\) in which two distinct vertices \(i\) and \(j\) are adjacent if and only if the transposition swapping \(i\) and \(j\) belongs to \(T\).

def edgeTranspositionGraph {n : ℕ} (T : Set (Equiv.Perm (Fin n))) :
    SimpleGraph (Fin n) :=
  SimpleGraph.fromRel (fun i j => Equiv.swap i j ∈ T)

TheoremFrucht's theorem#✓fully proved

Every finite group is isomorphic to the automorphism group of a finite simple graph.

theorem frucht
    {G : Type*} [Group G] [Fintype G] [DecidableEq G] :
    ∃ (n : ℕ) (Γ : SimpleGraph (Fin n)), Nonempty (G ≃* (Γ ≃g Γ))
Sources
  • R. Frucht, Compositio Math. 6 (1939), 239-250.

DefinitionMoore graph#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(d\) be a natural number. Then \(G\) is a Moore graph of diameter \(d\) when \(G\) has diameter \(d\) and girth \(2d + 1\).

def IsMooreGraph {V : Type*} [Fintype V] (G : SimpleGraph V) (d : ℕ) : Prop :=
  G.diam = d ∧ G.girth = 2 * d + 1

DefinitionPetersen graph#✓fully proved

The Petersen graph is the generalized Johnson graph \(J(5,2,0)\): its vertices are the \(2\)-element subsets of \(\{0, 1, 2, 3, 4\}\), and two of them are adjacent exactly when they are disjoint.

def petersenGraph : SimpleGraph {S : Finset (Fin 5) // S.card = 2} :=
  johnsonGraph 5 2 0
Uses 1
Statement usesGeneralized Johnson graph

TheoremPowers of a weighted adjacency matrix sum the weights of walks#✓fully proved

Let \(R\) be a commutative semiring, let \(k\) and \(n\) be natural numbers, and let \(A\) be a \(k \times k\) matrix over \(R\) with rows and columns indexed by \(\{0, \dots, k-1\}\), viewed as the weighted adjacency matrix of a weighted digraph on these \(k\) vertices. Then for all vertices \(i\) and \(j\),

\[(A^n)_{ij} = \sum_{p} \prod_{t=0}^{n-1} A_{p_t p_{t+1}},\]

where the sum runs over all sequences \(p = (p_0, \dots, p_n)\) of vertices with \(p_0 = i\) and \(p_n = j\), that is, over all walks of length \(n\) from \(i\) to \(j\), each weighted by the product of the entries of \(A\) along its edges.

The source states \(n \ge 1\); the case \(n = 0\) is included, where both sides equal \(1\) if \(i = j\) and \(0\) otherwise.

theorem adjMatrix_pow_weighted_walk_sum
    {k : ℕ} {R : Type*} [CommSemiring R]
    (A : Matrix (Fin k) (Fin k) R) (n : ℕ) (i j : Fin k) :
    (A ^ n) i j =
      ∑ p ∈ (Fintype.piFinset (fun _ : Fin (n + 1) => (Finset.univ : Finset (Fin k)))).filter
        (fun p => p 0 = i ∧ p (Fin.last n) = j),
        ∏ t : Fin n, A (p t.castSucc) (p t.succ)
Sources
  • Thomas Koshy, "A Graph-Theoretic Model for a Generalized Fibonacci Gem," Journal of Integer Sequences 22 (2019), Article 19.4.1, Theorem, lines 128–130, https://cs.uwaterloo.ca/journals/JIS/VOL22/Koshy/koshy7.tex
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.