Prefunctors on paths and on vertices

Elementary facts about a prefunctor φ : Q ⥤q R which Prefunctor.mapPath and Prefunctor.comp leave unrecorded: pushing a path along φ preserves its length, a prefunctor with a two-sided inverse is bijective on vertices, and a pair of composable one-sided inverse pairs composes to a one-sided inverse pair.

Main results

• Prefunctor.length_mapPath: pushing a path along a prefunctor preserves its length.
• Prefunctor.obj_bijective_of_comp_eq_id: mutually inverse prefunctors are bijective on vertices.
• Prefunctor.comp_comp_comp_eq_id: composing two one-sided inverse pairs of prefunctors gives a one-sided inverse pair.

References

They all feed TauCeti.PathAlgebra.mapAlgHom in TauCeti/RepresentationTheory/Quiver/PathAlgebra/Map.lean, whose uniform hypothesis is bijectivity on vertices, and the transport of the zigzag relations in TauCeti/RepresentationTheory/Quiver/Zigzag/Isomorphism.lean, which is stated in terms of path lengths.

@[simp]

theorem Prefunctor.length_mapPath {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (φ : Q ⥤q R) {a b : Q} (p : Quiver.Path a b) : (φ.mapPath p).length = p.length

Pushing a path along a prefunctor preserves its length: the image path traverses the image of each arrow of the original, in order.

theorem Prefunctor.obj_bijective_of_comp_eq_id {Q : Type u} {R : Type u'} [Quiver Q] [Quiver R] (φ : Q ⥤q R) (ψ : R ⥤q Q) (hφψ : φ ⋙q ψ = 𝟭q Q) (hψφ : ψ ⋙q φ = 𝟭q R) : Function.Bijective φ.obj

Mutually inverse prefunctors are bijective on vertices.

theorem Prefunctor.comp_comp_comp_eq_id {Q : Type u} {R : Type u'} {S : Type u''} [Quiver Q] [Quiver R] [Quiver S] (φ : Q ⥤q R) (ψ : R ⥤q Q) (φ' : R ⥤q S) (ψ' : S ⥤q R) (hφψ : φ ⋙q ψ = 𝟭q Q) (hφψ' : φ' ⋙q ψ' = 𝟭q R) : φ ⋙q φ' ⋙q (ψ' ⋙q ψ) = 𝟭q Q

One-sided inverse pairs of prefunctors compose: if ψ is a right inverse of φ and ψ' one of φ', then ψ' ⋙q ψ is a right inverse of φ ⋙q φ'. Applying this to a mutually inverse pair in each order gives both inverse laws for the composite pair.