Theorems · Definition · category theory

Prefunctor.map

{V : Type u₁} →
  [inst : Quiver V] →
    {W : Type u₂} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)

The action of a (pre)functor on edges/arrows/morphisms.

Defined in

Mathlib.Combinatorics.Quiver.Prefunctor

Cited by

952 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 5 definitions · uses no axioms

Assumes

QuiverQuiver