toPrefunctor — Mathlib

English

Prefunctors between two single-object quivers correspond to functions between their arrow types.

Русский

Префункторы между двумя однообъектными квиверами соответствуют функциям между их множествами стрел.

LaTeX

$$$\\text{toPrefunctor} : (\\alpha \\to \\beta) \\simeq \\mathrm{SingleObj}\\ \\alpha \\;\u2192\\q\\;\\mathrm{SingleObj}\\ \\beta.$$$

Lean4

/-- Prefunctors between two `SingleObj` quivers correspond to functions between the corresponding
arrows types.
-/
@[simps]
def toPrefunctor : (α → β) ≃ SingleObj α ⥤q SingleObj β
    where
  toFun f := ⟨id, f⟩
  invFun f a := f.map (toHom a)

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