The path-lifting graph cover

This module constructs the standard combinatorial unfolding of a rooted quiver.

The path-lifting cover

For a root r, a vertex of the cover remembers both a graph vertex v and a morphism from r to v in the free groupoid. An edge is a base edge whose lift has exactly the prescribed endpoint. This is the standard combinatorial unfolding construction; the covering proof below is independent of the rank calculation.

@[reducible, inline]

abbrev FiniteGraphFreeGroup.graphCoverVertex {V : Type u} [Quiver V] (root : V) : Type u

Vertices of the path-lifting cover over a chosen root.

Equations

• FiniteGraphFreeGroup.graphCoverVertex root = ((v : V) × ((Quiver.FreeGroupoid.of V).obj root ⟶ (Quiver.FreeGroupoid.of V).obj v))

@[instance_reducible]

instance FiniteGraphFreeGroup.graphCoverQuiver {V : Type u} [Quiver V] (root : V) : Quiver (graphCoverVertex root)

The lifted edges whose endpoint is prescribed by composition in the free groupoid.

Equations

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

def FiniteGraphFreeGroup.graphCoverProjection {V : Type u} [Quiver V] (root : V) : graphCoverVertex root ⥤q V

The projection from the path-lifting cover to the original quiver.

Equations

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

theorem FiniteGraphFreeGroup.graphCoverStar_ext {V : Type u} [Quiver V] {root : V} {x z y : graphCoverVertex root} (hy : z = y) {f : x ⟶ z} {e : x ⟶ y} (h : ↑f ≍ ↑e) : ⟨z, f⟩ = ⟨y, e⟩

theorem FiniteGraphFreeGroup.graphCoverCostar_ext {V : Type u} [Quiver V] {root : V} {x z y : graphCoverVertex root} (hy : z = y) {f : z ⟶ x} {e : y ⟶ x} (h : ↑f ≍ ↑e) : ⟨z, f⟩ = ⟨y, e⟩

def FiniteGraphFreeGroup.graphCoverStarEquiv {V : Type u} [Quiver V] (root : V) (x : graphCoverVertex root) : Quiver.Star x ≃ Quiver.Star x.fst

Explicit lifting of a star at a cover vertex.

Equations

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

def FiniteGraphFreeGroup.graphCoverCostarEquiv {V : Type u} [Quiver V] (root : V) (x : graphCoverVertex root) : Quiver.Costar x ≃ Quiver.Costar x.fst

Explicit lifting of a costar at a cover vertex.

Equations

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

theorem FiniteGraphFreeGroup.graphCoverProjection_isCovering {V : Type u} [Quiver V] (root : V) : (graphCoverProjection root).IsCovering

The path-lifting projection is a covering of quivers.