pathsOf_freeMap_toPrefunctor — Mathlib

English

Let F: V ⥤q W be a Prefunctor between quivers. Then the path construction is compatible with the free quiver functor: the composition Paths.of V with (Cat.freeMap F).toPrefunctor equals the composition F with Paths.of W.

Русский

Пусть F : V ⥤q W — префунктор между кварьерами. Тогда построение путей совместимо с свободной реконструкцией квар: композиция Paths.of V с (Cat.freeMap F).toPrefunctor равна композиции F с Paths.of W.

LaTeX

$$$Paths.of V \;⋙q\; (Cat.freeMap F).toPrefunctor = F \;⋙q\; Paths.of W$$$

Lean4

/-- Naturality of `Paths.of`, which defines a natural transformation
` 𝟭 _⟶ Cat.free ⋙ Quiv.forget`. -/
theorem pathsOf_freeMap_toPrefunctor {V : Type u} {W : Type u₁} [Quiver.{v + 1} V] [Quiver.{v₁ + 1} W] (F : V ⥤q W) :
    Paths.of V ⋙q (Cat.freeMap F).toPrefunctor = F ⋙q Paths.of W :=
  rfl

Похожие утверждения