Kneser graphs

DefinitionKneser graph#✓fully proved

For natural numbers \(v\) and \(k\), the Kneser graph \(K_{v:k}\) has as vertices the \(k\)-element subsets of the \(v\)-element set \(\{0, 1, \dots, v-1\}\), with two distinct vertices adjacent when they are disjoint.

By definition, \(K_{v:k}\) is the generalized Johnson graph \(J(v, k, 0)\).

def kneserGraph (v k : ℕ) :
    SimpleGraph {S : Finset (Fin v) // S.card = k} :=
  johnsonGraph v k 0

Uses 1

Statement usesGeneralized Johnson graph

TheoremAdjacency in the Kneser graph#✓fully proved

For natural numbers \(n\) and \(k\) and \(k\)-element subsets \(x\) and \(y\) of \(\{0, 1, \dots, n-1\}\), the vertices \(x\) and \(y\) of the Kneser graph \(K(n, k)\) are adjacent if and only if \(x\) and \(y\) are disjoint and \(x \ne y\).

public theorem kneserGraph_adj_iff (n k : ℕ) (x y : KneserVertex n k) :
    (kneserGraph n k).Adj x y ↔ Disjoint x.val y.val ∧ x ≠ y

TheoremKneser–Lovász theorem#✓fully proved

Let \(n\) and \(k\) be natural numbers with \(0 < k\) and \(2k \le n\). The Kneser graph \(K(n, k)\), whose vertices are the \(k\)-element subsets of \(\{0, 1, \dots, n-1\}\) and in which two such subsets are adjacent when they are disjoint and distinct, has chromatic number \(n - 2k + 2\).

public theorem kneser_lovasz {n k : ℕ} (hk : 0 < k) (h : 2 * k ≤ n) :
    (kneserGraph n k).chromaticNumber = (n - 2 * k + 2 : ℕ∞)

Sources

• L. Lovasz, JCT A 25 (1978), 319-324, DOI 10.1016/0097-3165(78)90022-5.

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.