lift_toPath — Mathlib

English

Given a Prefunctor φ on V and a functor Φ: Paths V ⥤ C with hΦ: of V ⋙ Φ.toPrefunctor = φ, then Φ = lift φ; i.e., lift is the unique functor extending φ along paths.

Русский

Пусть φ — префунктор на V и Φ — функтор Paths V → C так, что композиция Paths.of V с Φ.toPrefunctor равна φ; тогда Φ = lift φ, то есть lift является единственным продолжением φ вдоль путей.

LaTeX

$$$\forall φ:\, V \to_q C, \; \forall Φ:\Paths\ V \to C,\; (Paths.of\ V) \circ Φ^{toPrefunctor} = φ \Rightarrow Φ = \mathrm{lift}\, φ$$$

Lean4

@[simp]
theorem lift_toPath {C} [Category C] (φ : V ⥤q C) {X Y : V} (f : X ⟶ Y) : (lift φ).map f.toPath = φ.map f :=
  by
  dsimp [Quiver.Hom.toPath, lift]
  simp

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