Arc-transitive graphs

Structure\(s\)-arc#✓fully proved

Let \(X\) be a finite graph and \(s\) a natural number. An \(s\)-arc in \(X\) is a sequence \((v_0, \dots, v_s)\) of vertices of \(X\) such that \(v_{i-1}\) and \(v_i\) are adjacent for \(1 \le i \le s\), and \(v_{i-1} \ne v_{i+1}\) for \(0 < i < s\).

structure _root_.SimpleGraph.SArc {V : Type*} [Fintype V] (G : SimpleGraph V) (s : ℕ) where
  vertices : Fin (s + 1) → V
  adj : ∀ i : Fin s, G.Adj (vertices i.castSucc) (vertices i.succ)
  no_backtrack : ∀ (i : Fin (s + 1)) (h : (i : ℕ) + 2 ≤ s),
    vertices i ≠ vertices ⟨(i : ℕ) + 2, by omega⟩

Used by 3

Used by\(s\)-arc digraph · \(s\)-arc regular graph · \(s\)-arc transitive graph

Definition\(s\)-arc transitive graph#✓fully proved

A finite graph \(G\) is \(s\)-arc transitive if its automorphism group acts transitively on its \(s\)-arcs: for any two \(s\)-arcs \((u_0, \dots, u_s)\) and \((v_0, \dots, v_s)\) of \(G\) there is an automorphism \(\varphi\) of \(G\) with \(\varphi(u_i) = v_i\) for every \(i \le s\).

def SimpleGraph.IsSArcTransitive {V : Type*} [Fintype V] (G : SimpleGraph V) (s : ℕ) : Prop :=
  ∀ p q : G.SArc s, ∃ φ : G ≃g G, ∀ i, φ (p.vertices i) = q.vertices i

Uses 1

Statement uses\(s\)-arc

Definition\(s\)-arc regular graph#✓fully proved

A finite graph \(G\) is \(s\)-arc regular if it has at least one \(s\)-arc and, for any two \(s\)-arcs \((u_0, \dots, u_s)\) and \((v_0, \dots, v_s)\) of \(G\), there is exactly one automorphism \(\varphi\) of \(G\) with \(\varphi(u_i) = v_i\) for every \(i \le s\).

def SimpleGraph.IsSArcRegular {V : Type*} [Fintype V] (G : SimpleGraph V) (s : ℕ) : Prop :=
  Nonempty (G.SArc s) ∧
  ∀ p q : G.SArc s, ∃! φ : G ≃g G, ∀ i : Fin (s + 1), φ (p.vertices i) = q.vertices i

Uses 1

Statement uses\(s\)-arc

Definition\(s\)-arc digraph#✓fully proved

Let \(X\) be a finite graph and \(s\) a natural number. For an \((s+1)\)-arc \(\gamma = (x_0, \dots, x_{s+1})\) of \(X\), its head is the \(s\)-arc \((x_1, \dots, x_{s+1})\) and its tail is the \(s\)-arc \((x_0, \dots, x_s)\). If \(\alpha\) and \(\beta\) are \(s\)-arcs of \(X\), then \(\beta\) follows \(\alpha\) if there is an \((s+1)\)-arc of \(X\) whose tail is \(\alpha\) and whose head is \(\beta\). The \(s\)-arc digraph \(X^{(s)}\) is the directed graph whose vertices are the \(s\)-arcs of \(X\), with an arc from \(\alpha\) to \(\beta\) if and only if \(\beta\) follows \(\alpha\).

def _root_.SimpleGraph.arcDigraph {V : Type*} [Fintype V]
    (G : SimpleGraph V) (s : ℕ) : Digraph (G.SArc s) where
  Adj a b := b.follows a

Uses 1

Statement uses\(s\)-arc

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.