Definition 20: Cayley Graph

Main Results

• cayleyGraph: The Cayley graph Cay(G, S) of a finite group G with symmetric generating set S ⊆ G \ {1}.
• cayleyGraph_isRegularOfDegree: The Cayley graph is |S|-regular.

structure CayleyGraph.SymmGenSet (G : Type u_2) [Group G] [DecidableEq G] : Type u_2

A symmetric generating set S ⊆ G \ {1}: a finite set of group elements not containing the identity, closed under inverses.

• carrier : Finset G

  The underlying finite set of generators.

• one_not_mem : 1 ∉ self.carrier

  The identity is not in S.

• inv_mem (s : G) : s ∈ self.carrier → s⁻¹ ∈ self.carrier

  S is closed under inverses: s ∈ S → s⁻¹ ∈ S.

def CayleyGraph.cayleyGraph {G : Type u_1} [Group G] [DecidableEq G] (S : SymmGenSet G) : SimpleGraph G

The (undirected) Cayley graph Cay(G, S) is the simple graph with vertex set G, where g and g' are adjacent iff there exists s ∈ S such that g' = s * g. Since S is symmetric, adjacency is symmetric; since 1 ∉ S, there are no self-loops.

Equations

• CayleyGraph.cayleyGraph S = { Adj := fun (g g' : G) => ∃ s ∈ S.carrier, g' = s * g, symm := ⋯, loopless := ⋯ }

instance CayleyGraph.cayleyGraph_decidableAdj {G : Type u_1} [Group G] [DecidableEq G] (S : SymmGenSet G) : DecidableRel (cayleyGraph S).Adj

Equations

• CayleyGraph.cayleyGraph_decidableAdj S g g' = id (decidable_of_iff (∃ s ∈ S.carrier, g' = s * g) ⋯)

theorem CayleyGraph.cayleyGraph_isRegularOfDegree {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (S : SymmGenSet G) : (cayleyGraph S).IsRegularOfDegree S.carrier.card

Each vertex g has exactly |S| neighbors {s * g : s ∈ S}, which are pairwise distinct because left multiplication by distinct group elements yields distinct results.

theorem CayleyGraph.cayleyGraph_neighborFinset {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (S : SymmGenSet G) (v : G) : (cayleyGraph S).neighborFinset v = Finset.image (fun (x : G) => x * v) S.carrier

The neighbor finset of v in the Cayley graph is {s * v | s ∈ S}.

theorem CayleyGraph.cayleyGraph_nonempty_of_nonempty {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (S : SymmGenSet G) (hS : S.carrier.Nonempty) : ∃ (g : G) (g' : G), (cayleyGraph S).Adj g g'

Witness: the Cayley graph has edges when S is nonempty.