The labelled Schreier graph and its spanning-tree basis

The action groupoid is equipped with the smaller generating quiver whose edges are labelled by the original free generators. This is the finite graph that the core construction uses; the generic Nielsen--Schreier instance instead uses the whole free group as a generator synonym.

@[reducible, inline]

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

The objects of the action groupoid serving as vertices of the covering graph.

Equations

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

@[instance_reducible]

def MarshallHall.coverQuiver (α A : Type u) [MulAction (FreeGroup α) A] : Quiver (CoverVertex α A)

The generator-labelled covering quiver, supplied explicitly to preserve categorical arrows.

Equations

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

The action groupoid is free for this explicit labelled generating quiver.

@[reducible]

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

The free-group action groupoid is free on its generator-labelled covering quiver.

Equations

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

The basis is indexed by the actual labelled edges outside the chosen tree. The proof is the same unique-lift argument as Mathlib's spanning-tree theorem, but keeps the edge type explicit for later core-support statements.

def MarshallHall.spanningTreeRoot {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] : G

The root of a spanning tree, viewed as an object of the underlying groupoid.

Equations

• MarshallHall.spanningTreeRoot T = Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)

noncomputable def MarshallHall.spanningTreeBasis {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] : FreeGroupBasis (↑(Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify T))ᶜ) (CategoryTheory.End (spanningTreeRoot T))

The free basis of the root endomorphism group indexed by generator edges outside the spanning tree.

Equations

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

theorem MarshallHall.spanningTreeBasis_apply {G : Type u} [CategoryTheory.Groupoid G] [IsFreeGroupoid G] (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G))) [Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] (e : ↑(Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify T))ᶜ) : (spanningTreeBasis T) e = IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of (↑e).hom)