Schreier Graphs

This module defines Schreier graphs as quivers with labelled edges.

Given a monoid M acting on a type V and a map ι : S → M, the Schreier graph has vertices V and a directed edge x → ι(s) • x for each x : V and s : S.

Main definitions

• SchreierGraph V ι - The Schreier graph of an action, with vertices of type V and edges labelled by elements of S via ι : S → M.
• SchreierGraph.labelling - The prefunctor from a Schreier graph to SingleObj S that extracts edge labels.
• SchreierGraph.evalWord - Evaluation of a word in generators and their inverses as an element of the ambient group, by lifting the corresponding element of the free group along FreeGroup.lift.
• SchreierGraph.pathFromWord - The path in the symmetrified Schreier graph induced by a word of generators (forward edges) and inverses (backward edges).

Main results

• SchreierGraph.labelling_isCovering - The labelling prefunctor is a covering when we have a group action.
• SchreierGraph.evalWord_mem_closure - The evaluation of any word lies in the subgroup generated by the image of ι.
• SchreierGraph.exists_evalWord_of_mem_closure - Conversely, every element of that subgroup is the evaluation of some word.
• SchreierGraph.reachable_iff - Two vertices of a Schreier graph are connected by a path in its symmetrification iff they are related by an element of the subgroup generated by ι.

Examples

• The (left) Cayley graph of a group M with generators ι : S → M is the Schreier graph where V = M and the action is left multiplication.

Implementation notes

Although referred to informally as graphs, Schreier graphs have multiple, directed, labelled edges between nodes and so are implemented here as quivers.

References

• [Y. Vorobets, Notes on the Schreier graphs of the Grigorchuk group][Vorobets2012]

structure Quiver.SchreierGraph (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (_ι : S → M) : Type u_1

A Schreier graph for a monoid M acting on V with generators ι : S → M. Vertices are elements of V, and there is an edge from x to y for each s : S such that ι s • x = y.

• ofVertex :: (
• toVertex : V

  The underlying vertex.

• )

theorem Quiver.SchreierGraph.ext_iff {V : Type u_1} {M : Type u_2} {inst✝ : SMul M V} {S : Type u_3} {_ι : S → M} {x y : SchreierGraph V _ι} : x = y ↔ x.toVertex = y.toVertex

theorem Quiver.SchreierGraph.ext {V : Type u_1} {M : Type u_2} {inst✝ : SMul M V} {S : Type u_3} {_ι : S → M} {x y : SchreierGraph V _ι} (toVertex : x.toVertex = y.toVertex) : x = y

def Quiver.SchreierGraph.equiv (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) : V ≃ SchreierGraph V ι

Equivalence between the original vertex type and the Schreier graph type.

Equations

• Quiver.SchreierGraph.equiv V ι = { toFun := Quiver.SchreierGraph.ofVertex, invFun := Quiver.SchreierGraph.toVertex, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Quiver.SchreierGraph.equiv_symm_apply (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) (self : SchreierGraph V ι) : (equiv V ι).symm self = self.toVertex

@[simp]

theorem Quiver.SchreierGraph.equiv_apply_toVertex (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) (toVertex : V) : ((equiv V ι) toVertex).toVertex = toVertex

@[instance_reducible]

instance Quiver.SchreierGraph.schreierGraphSMul (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) : SMul M (SchreierGraph V ι)

Transport the scalar multiplication to the Schreier graph vertices.

Equations

• Quiver.SchreierGraph.schreierGraphSMul V ι = { smul := fun (x : M) (y : Quiver.SchreierGraph V ι) => { toVertex := x • y.toVertex } }

@[instance_reducible]

instance Quiver.SchreierGraph.schreierGraphQuiver (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) : Quiver (SchreierGraph V ι)

The quiver structure on a Schreier graph. An arrow from x to y exists when there is an s : S such that (ι s) • x = y.

Equations

• Quiver.SchreierGraph.schreierGraphQuiver V ι = { Hom := fun (x y : Quiver.SchreierGraph V ι) => { s : S // ι s • x = y } }

def Quiver.SchreierGraph.labelling (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) : SchreierGraph V ι ⥤q SingleObj S

The labelling of arrows in a Schreier graph by elements of S. This is encoded as a prefunctor to SingleObj S.

Equations

• Quiver.SchreierGraph.labelling V ι = { obj := fun (x : Quiver.SchreierGraph V ι) => Quiver.SingleObj.star S, map := fun {X Y : Quiver.SchreierGraph V ι} (e : X ⟶ Y) => ↑e }

@[simp]

theorem Quiver.SchreierGraph.labelling_obj (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) (x✝ : SchreierGraph V ι) : (labelling V ι).obj x✝ = SingleObj.star S

@[simp]

theorem Quiver.SchreierGraph.labelling_map (V : Type u_1) {M : Type u_2} [SMul M V] {S : Type u_3} (ι : S → M) {X✝ Y✝ : SchreierGraph V ι} (e : X✝ ⟶ Y✝) : (labelling V ι).map e = ↑e

@[instance_reducible]

instance Quiver.SchreierGraph.instMulAction (V : Type u_1) {M : Type u_2} [Monoid M] [MulAction M V] {S : Type u_3} (ι : S → M) : MulAction M (SchreierGraph V ι)

The monoid acts on the vertices of the Schreier graph.

Equations

• Quiver.SchreierGraph.instMulAction V ι = { toSMul := Quiver.SchreierGraph.schreierGraphSMul V ι, mul_smul := ⋯, one_smul := ⋯ }

Schreier graphs for group actions

When we have a group action, the labelling becomes a covering.

def Quiver.SchreierGraph.labellingStarEquiv {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) : Star x ≃ Star (SingleObj.star S)

The star map of the labelling prefunctor as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Quiver.SchreierGraph.labellingStarEquiv_symm_apply_fst {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) (x✝ : Star (SingleObj.star S)) : ((labellingStarEquiv ι x).symm x✝).fst = ι x✝.snd • x

@[simp]

theorem Quiver.SchreierGraph.labellingStarEquiv_apply {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) (a✝ : Star x) : (labellingStarEquiv ι x) a✝ = (labelling V ι).star x a✝

@[simp]

theorem Quiver.SchreierGraph.labellingStarEquiv_symm_apply_snd_coe {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) (x✝ : Star (SingleObj.star S)) : ↑((labellingStarEquiv ι x).symm x✝).snd = x✝.snd

def Quiver.SchreierGraph.labellingCostarEquiv {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) : Costar x ≃ Costar (SingleObj.star S)

The costar map of the labelling prefunctor as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Quiver.SchreierGraph.labellingCostarEquiv_apply {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) (a✝ : Costar x) : (labellingCostarEquiv ι x) a✝ = (labelling V ι).costar x a✝

@[simp]

theorem Quiver.SchreierGraph.labellingCostarEquiv_symm_apply_fst {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) (x✝ : Costar (SingleObj.star S)) : ((labellingCostarEquiv ι x).symm x✝).fst = (ι x✝.snd)⁻¹ • x

@[simp]

theorem Quiver.SchreierGraph.labellingCostarEquiv_symm_apply_snd_coe {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) (x✝ : Costar (SingleObj.star S)) : ↑((labellingCostarEquiv ι x).symm x✝).snd = x✝.snd

theorem Quiver.SchreierGraph.labelling_isCovering {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) : (labelling V ι).IsCovering

The labelling prefunctor is a covering for Schreier graphs with group actions.

theorem Quiver.SchreierGraph.map_smul_of_comp_labelling_eq {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) {W : Type u_4} [MulAction M W] (φ : SchreierGraph V ι ⥤q SchreierGraph W ι) (φm : φ ⋙q labelling W ι = labelling V ι) (v : SchreierGraph V ι) (s : S) : φ.obj (ι s • v) = ι s • φ.obj v

If a prefunctor between Schreier graphs commutes with the labelling (i.e., labels are preserved), then it commutes with the group action. In other words, morphisms that preserve edge labels also preserve the group structure.

Word evaluation

Evaluating a word (list of generators tagged with a boolean for forward/inverse direction) as an element of the ambient group, by lifting it through the free group. Words are kept in list form because pathFromWord recurses on the list: distinct words give distinct paths, even when they evaluate to the same group element.

def Quiver.SchreierGraph.evalWord {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) (w : List (S × Bool)) : M

Evaluate a word List (S × Bool) as an element of the group M. A pair (s, true) contributes ι s; a pair (s, false) contributes (ι s)⁻¹.

Equations

• Quiver.SchreierGraph.evalWord ι w = (FreeGroup.lift ι) (FreeGroup.mk w)

@[simp]

theorem Quiver.SchreierGraph.evalWord_nil {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) : evalWord ι [] = 1

@[simp]

theorem Quiver.SchreierGraph.evalWord_cons_true {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) (s : S) (w : List (S × Bool)) : evalWord ι ((s, true) :: w) = ι s * evalWord ι w

@[simp]

theorem Quiver.SchreierGraph.evalWord_cons_false {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) (s : S) (w : List (S × Bool)) : evalWord ι ((s, false) :: w) = (ι s)⁻¹ * evalWord ι w

theorem Quiver.SchreierGraph.evalWord_append {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) (w₁ w₂ : List (S × Bool)) : evalWord ι (w₁ ++ w₂) = evalWord ι w₁ * evalWord ι w₂

theorem Quiver.SchreierGraph.evalWord_mem_closure {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) (w : List (S × Bool)) : evalWord ι w ∈ Subgroup.closure (Set.range ι)

The evaluation of any word lies in the subgroup generated by the image of ι.

theorem Quiver.SchreierGraph.exists_evalWord_of_mem_closure {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) {g : M} (hg : g ∈ Subgroup.closure (Set.range ι)) : ∃ (w : List (S × Bool)), evalWord ι w = g

Every element of the subgroup generated by the image of ι is the evaluation of a word.

Reachability in symmetrified Schreier graphs

Reachability in the symmetrified Schreier graph characterises the orbit of the subgroup generated by ι.

def Quiver.SchreierGraph.pathFromWord {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x : SchreierGraph V ι) (w : List (S × Bool)) : Path (Symmetrify.of.obj x) (Symmetrify.of.obj (evalWord ι w • x))

Construct a path in the symmetrified Schreier graph from a Bool-tagged word. A pair (s, true) contributes a forward edge for ι s; (s, false) contributes a backward edge, representing motion along (ι s)⁻¹.

Equations

• Quiver.SchreierGraph.pathFromWord ι x [] = Quiver.Path.cast ⋯ ⋯ Quiver.Path.nil
• Quiver.SchreierGraph.pathFromWord ι x ((s, true) :: w) = Quiver.Path.cast ⋯ ⋯ ((Quiver.SchreierGraph.pathFromWord ι x w).cons (Sum.inl ⟨s, ⋯⟩))
• Quiver.SchreierGraph.pathFromWord ι x ((s, false) :: w) = Quiver.Path.cast ⋯ ⋯ ((Quiver.SchreierGraph.pathFromWord ι x w).cons (Sum.inr ⟨s, ⋯⟩))

theorem Quiver.SchreierGraph.reachable_of_mem_closure {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) {g : M} (hg : g ∈ Subgroup.closure (Set.range ι)) (y : SchreierGraph V ι) : Reachable (Symmetrify.of.obj y) (Symmetrify.of.obj (g • y))

If g lies in the subgroup generated by the image of ι, then g • y is reachable from y in the symmetrification, for every vertex y of the Schreier graph.

theorem Quiver.SchreierGraph.exists_mem_closure_of_path {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) {x : SchreierGraph V ι} {y : Symmetrify (SchreierGraph V ι)} (p : Path (Symmetrify.of.obj x) y) : ∃ g ∈ Subgroup.closure (Set.range ι), g • x = y

A path in the symmetrified Schreier graph exhibits an element of the subgroup generated by ι that carries the source to the target.

theorem Quiver.SchreierGraph.reachable_iff {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x y : SchreierGraph V ι) : Reachable (Symmetrify.of.obj x) (Symmetrify.of.obj y) ↔ ∃ g ∈ Subgroup.closure (Set.range ι), g • x = y

Two vertices of a Schreier graph are connected by a path in the symmetrified quiver iff some element of the subgroup generated by ι carries one to the other.