36 Def 20: Cayley Graph
A symmetric generating set for a group \(G\) is a structure consisting of:
A finite set of generators \(S \subseteq G\) (the carrier),
A proof that the identity \(1 \notin S\),
A proof that \(S\) is closed under inverses: for all \(s \in S\), \(s^{-1} \in S\).
Let \(G\) be a finite group with decidable equality, and let \(S\) be a symmetric generating set for \(G\). The Cayley graph \(\operatorname {Cay}(G, S)\) is the simple graph with vertex set \(G\), where two vertices \(g, g' \in G\) are adjacent if and only if there exists \(s \in S\) such that \(g' = s \cdot g\).
Well-definedness as a simple graph follows from:
Symmetry: If \(g' = s \cdot g\) for some \(s \in S\), then \(g = s^{-1} \cdot g'\) and \(s^{-1} \in S\) by the inverse-closure of \(S\).
Looplessness: If \(g = s \cdot g\) for some \(s \in S\), then \(s = 1\), contradicting \(1 \notin S\).
The Cayley graph \(\operatorname {Cay}(G, S)\) is \(|S|\)-regular: every vertex has degree exactly \(|S|\).
Let \(v \in G\) be an arbitrary vertex. We show that the neighbor set of \(v\) equals the image \(\{ s \cdot v \mid s \in S\} \). By extensionality, a vertex \(w\) belongs to the neighbor finset of \(v\) if and only if there exists \(s \in S\) with \(w = s \cdot v\), which holds if and only if \(w \in S.\operatorname {image}(\cdot \times v)\). This establishes the equality of neighbor finsets.
It then follows that
where the last equality holds because the map \(s \mapsto s \cdot v\) is injective: if \(s \cdot v = s' \cdot v\), then right-cancellation gives \(s = s'\). Since \(v\) was arbitrary, the graph is \(|S|\)-regular.
For any vertex \(v \in G\), the neighbor finset of \(v\) in \(\operatorname {Cay}(G, S)\) equals the image of the carrier under left-multiplication by \(v\):
By extensionality, a vertex \(w\) is in the neighbor finset of \(v\) if and only if \(w\) and \(v\) are adjacent in \(\operatorname {Cay}(G, S)\), i.e., there exists \(s \in S\) with \(w = s \cdot v\). This is precisely the condition for \(w \in \{ s \cdot v \mid s \in S\} \). Both directions follow immediately by unfolding the definitions.
If the carrier \(S\) is nonempty, then the Cayley graph \(\operatorname {Cay}(G, S)\) has at least one edge: there exist \(g, g' \in G\) such that \(g\) and \(g'\) are adjacent.
Since \(S\) is nonempty, we obtain some \(s \in S\). We then exhibit the adjacency \(1 \sim s \cdot 1\) in \(\operatorname {Cay}(G, S)\), witnessed by \(s \in S\) and the equality \(s \cdot 1 = s \cdot 1\) (by reflexivity). Hence there exist vertices \(g = 1\) and \(g' = s \cdot 1\) that are adjacent.