Theorems · Theorem · category theory

Prefunctor.comp_map

∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] {W : Type u_3} [inst_2 : Quiver W] (F : U ⥤q V)
  (G : V ⥤q W) {X Y : U} (f : X ⟶ Y), (F ⋙q G).map f = G.map (F.map f)

Defined in

Mathlib.Combinatorics.Quiver.Prefunctor

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

QuiverQuiverQuiver