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.

Main results

• SchreierGraph.labelling_isCovering - The labelling prefunctor is a covering when we have a group action.

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

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 {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

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

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_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

@[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

@[implicit_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 } }

@[implicit_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_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

@[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

@[implicit_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_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

@[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✝

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_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

@[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

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.