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
.
Equations
- symmetric_subset G S = ∀ g ∈ S, g⁻¹ ∈ S
Instances For
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_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
Equations
- cayley_graph G S = schreier_graph G S G
Instances For
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.apply
{G : Type}
[Group G]
{S : Set G}
(v : G)
(g : G)
(h : g ∈ S)
:
g ∈ (cayley_graph G S).edges v (g * v)
Equations
- instQuiverInt_marginis = { Hom := fun (x y : ℤ) => ↑(IntCayley.edges x y) }
Equations
- mypath = Quiver.Path.nil.cons (let_fun this := ⟨1, mypath.proof_1⟩; this)