The Schreier graph of a free-group action. Its vertices are action points, and a generator-labelled edge follows the corresponding left action. The subgroup application uses the action on cosets.

Adapted for Lean Pool from Arthur742Ramos/KuroshSubgroupTheorem, commit 911707126c8b9bb0c764bf853008fe1053c0aad9: imports, API compatibility, and proof organization were revised.

@[reducible, inline]

abbrev GraphCoveringTheory.CoverVertex (α A : Type u) [MulAction (FreeGroup α) A] : Type u

The Schreier vertices, represented as objects of the action groupoid.

Equations

• GraphCoveringTheory.CoverVertex α A = CategoryTheory.ActionCategory (FreeGroup α) A

@[instance_reducible]

instance GraphCoveringTheory.coverQuiver (α A : Type u) [MulAction (FreeGroup α) A] : Quiver (CoverVertex α A)

Equations

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

inductive GraphCoveringTheory.Rose (α : Type u) : Type u

The one-vertex quiver whose loops will be labeled by the generator type.

• point {α : Type u} : Rose α

@[instance_reducible]

instance GraphCoveringTheory.roseQuiver (α : Type u) : Quiver (Rose α)

Equations

• GraphCoveringTheory.roseQuiver α = { Hom := fun (x x_1 : GraphCoveringTheory.Rose α) => α }

def GraphCoveringTheory.coverProjection (α A : Type u) [MulAction (FreeGroup α) A] : CoverVertex α A ⥤q Rose α

Project the Schreier quiver to the rose by retaining each edge's generator label.

Equations

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

def GraphCoveringTheory.coverStarEquiv (α A : Type u) [MulAction (FreeGroup α) A] (x : CoverVertex α A) : Quiver.Star x ≃ Quiver.Star Rose.point

Outgoing Schreier edges are in bijection with the generator loops of the rose.

Equations

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

def GraphCoveringTheory.coverCostarEquiv (α A : Type u) [MulAction (FreeGroup α) A] (x : CoverVertex α A) : Quiver.Costar x ≃ Quiver.Costar Rose.point

Incoming Schreier edges are in bijection with the generator loops of the rose.

Equations

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

theorem GraphCoveringTheory.coverProjection_isCovering (α A : Type u) [MulAction (FreeGroup α) A] : (coverProjection α A).IsCovering

The action groupoid admits a smaller, explicit generating quiver when the acting free group is presented as FreeGroup α. Mathlib's general Nielsen--Schreier instance uses an abstract chosen basis; this version keeps the original generator type visible for the cardinality computation.

@[reducible]

def GraphCoveringTheory.freeActionGroupoidIsFree (α A : Type u) [MulAction (FreeGroup α) A] : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup α) A)

Present the free-group action groupoid by its Schreier quiver of generator edges.

Equations

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