Path lifting with a fixed endpoint

Mathlib's quiver-covering API supplies path-star lifting, with the initial vertex fixed. The categorical covering theorem also needs the dual statement with the terminal vertex fixed. This file proves it directly from the costar bijections.

@[reducible, inline]

abbrev Quiver.PathCostar {U : Type u_1} [Quiver U] (v : U) : Type (max u_1 u_1 u)

The path costar at v: all paths ending at v.

def Prefunctor.pathCostar {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (v : U) : Quiver.PathCostar v → Quiver.PathCostar (φ.obj v)

A prefunctor maps the path costar at a vertex into the path costar at its image.

@[simp]

theorem Prefunctor.pathCostar_apply {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) {u v : U} (p : Quiver.Path u v) : φ.pathCostar v ⟨u, p⟩ = ⟨φ.obj u, φ.mapPath p⟩

theorem Quiver.Path.length_cast_eq {U : Type u_1} [Quiver U] {a b a' b' : U} (p : Path a b) (ha : a = a') (hb : b = b') : (cast ha hb p).length = p.length

theorem Prefunctor.pathCostar_surjective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (v : U), Function.Surjective (φ.costar v)) (v : U) : Function.Surjective (φ.pathCostar v)

theorem Prefunctor.pathCostar_injective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (v : U), Function.Injective (φ.costar v)) (v : U) : Function.Injective (φ.pathCostar v)

theorem Prefunctor.pathCostar_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] (φ : U ⥤q V) (hφ : ∀ (v : U), Function.Bijective (φ.costar v)) (v : U) : Function.Bijective (φ.pathCostar v)

theorem Prefunctor.IsCovering.pathCostar_bijective {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {φ : U ⥤q V} (hφ : φ.IsCovering) (v : U) : Function.Bijective (φ.pathCostar v)

A quiver covering gives unique path lifting with the terminal vertex fixed.