Johnson graphs

DefinitionGeneralized Johnson graph#✓fully proved

For natural numbers \(v\), \(k\) and \(i\), the generalized Johnson graph \(J(v,k,i)\) is the graph whose vertices are the \(k\)-element subsets of \(\{0, 1, \dots, v-1\}\), in which two distinct vertices are adjacent if and only if their intersection has exactly \(i\) elements.

The usual setting is \(v \ge k \ge i\); the definition does not require it.

def johnsonGraph (v k i : ℕ) :
    SimpleGraph {S : Finset (Fin v) // S.card = k} where
  Adj A B := A ≠ B ∧ (A.val ∩ B.val).card = i
  symm := ⟨fun {A B} ⟨hne, hcard⟩ => ⟨hne.symm, by rw [inter_comm]; exact hcard⟩⟩
  loopless := ⟨fun {A} ⟨hne, _⟩ => hne rfl⟩

Used by 2

Used byPetersen graph · Kneser graph

DefinitionJohnson graph#✓fully proved

For natural numbers \(n\) and \(k\), the Johnson graph \(J(n, k)\) has as vertices the \(k\)-element subsets of \(\{0, 1, \dots, n-1\}\), and two vertices \(s\) and \(t\) are adjacent when \(|s \cap t| + 1 = k\), that is, when \(s\) and \(t\) share exactly \(k - 1\) elements.

public def johnsonGraph (n k : ℕ) : SimpleGraph {s : Finset (Fin n) // s.card = k} where
  Adj s t := (s.val ∩ t.val).card + 1 = k
  symm.symm s t h := by simpa [Finset.inter_comm]
  loopless.irrefl := by simp +contextual

Used by 1

Used byAdjacency in the Johnson graph

TheoremAdjacency in the Johnson graph#✓fully proved

For natural numbers \(n\) and \(k\) and \(k\)-element subsets \(s\) and \(t\) of \(\{0, 1, \dots, n-1\}\), the vertices \(s\) and \(t\) of the Johnson graph \(J(n, k)\) are adjacent if and only if \(|s \cap t| + 1 = k\).

public theorem johnsonGraph_adj_iff (n k : ℕ)
    (s t : {s : Finset (Fin n) // s.card = k}) :
    (johnsonGraph n k).Adj s t ↔ (s.val ∩ t.val).card + 1 = k

Uses 1

Statement usesJohnson graph

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.