Ends of groups: a nonstandard perspective

Isaac Goldbring

Inspired by the paper we give a definition of the Cayley graph of a group. We start from Kyle Miller's Lean 3 code at https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/graph.2C.20expander.20graph.2C.20cayley.20graph.2C.20.2E.2E.2E.html

After converting that to Lean 4, we construct the Cayley graph of ℤ and give some computations on it.

We also construct a path in this Cayley graph, using Lean's Quiver.Path.

structure digraph (V : Type) (E : Type) : Type

• edges : V → V → Set E

def symmetric_subset (G : Type) [Group G] (S : Set G) : Prop

Equations

• symmetric_subset G S = ∀ (g : G), g ∈ S → g⁻¹ ∈ S

def schreier_graph (G : Type) [Group G] (S : Set G) (X : Type) [MulAction G X] : digraph X G

Equations

• schreier_graph G S X = { edges := fun (x y : X) => {g : G | g ∈ S ∧ g • x = y} }

theorem schreier_graph.edge_mem {G : Type} [Group G] {S : Set G} {X : Type} [MulAction G X] (g : G) (x : X) (y : X) (h : g ∈ (schreier_graph G S X).edges x y) : g ∈ S

theorem schreier_graph.edge_gen {G : Type} [Group G] {S : Set G} {X : Type} [MulAction G X] (g : G) (x : X) (y : X) (h : g ∈ (schreier_graph G S X).edges x y) : g • x = y

theorem schreier_graph.edge_comm_aux {G : Type} [Group G] {S : Set G} {X : Type} [MulAction G X] {g : G} {x : X} {y : X} {sym : symmetric_subset G S} (h : g ∈ (schreier_graph G S X).edges x y) : g⁻¹ ∈ (schreier_graph G S X).edges y x

theorem schreier_graph.edge_comm {G : Type} [Group G] {S : Set G} {X : Type} [MulAction G X] (g : G) (x : X) (y : X) (sym : symmetric_subset G S) : g ∈ (schreier_graph G S X).edges x y ↔ g⁻¹ ∈ (schreier_graph G S X).edges y x

def cayley_graph (G : Type) [Group G] (S : Set G) : digraph G G

Equations

• cayley_graph G S = schreier_graph G S G

theorem cayley_graph.edge_mem {G : Type} [Group G] {S : Set G} (v : G) (w : G) (g : G) (h : g ∈ (cayley_graph G S).edges v w) : g ∈ S

theorem cayley_graph.mem_iff {G : Type} [Group G] {S : Set G} (v : G) (w : G) (g : G) : g ∈ (cayley_graph G S).edges v w ↔ g ∈ S ∧ g * v = w

theorem cayley_graph.apply {G : Type} [Group G] {S : Set G} (v : G) (g : G) (h : g ∈ S) : g ∈ (cayley_graph G S).edges v (g * v)

def IntCayley : digraph ℤ ℤ

Equations

• IntCayley = cayley_graph ℤ {1, -1}

instance instQuiverInt_marginis : Quiver ℤ

Equations

• instQuiverInt_marginis = { Hom := fun (x y : ℤ) => ↑(IntCayley.edges x y) }

def mypath : Quiver.Path 0 1

Equations

• mypath = Quiver.Path.nil.cons (let_fun this := ⟨1, mypath.proof_1⟩; this)