lift_spec — Mathlib

English

For any φ: V ⥤q V′, the composition of of V with (lift φ).toPrefunctor equals φ.

Русский

Для любого отображения φ: V ⥤q V′, композиция of V с (lift φ).toPrefunctor равна φ.

LaTeX

$$$(\\mathrm{of}\\ V) \\; \\circ \\; (\\mathrm{lift}\\ φ).toPrefunctor = φ$$$

Lean4

theorem lift_spec (φ : V ⥤q V') : of V ⋙q (lift φ).toPrefunctor = φ :=
  by
  rw [of_eq, Prefunctor.comp_assoc, Prefunctor.comp_assoc, Functor.toPrefunctor_comp]
  dsimp [lift]
  rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]

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