Theorems · Definition · combinatorics

Prefunctor.mapPath

{V : Type u₁} →
  [inst : Quiver V] →
    {W : Type u₂} → [inst_1 : Quiver W] → (F : V ⥤q W) → {a b : V} → Quiver.Path a b → Quiver.Path (F.obj a) (F.obj b)

The image of a path under a prefunctor.

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

15 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

QuiverQuiver