English
Same content as Lift Uniqueness: the lift φ is the unique prefunctor extending φ and preserving reverses.
Русский
То же самое, что и Уникальность лифтинга: единственный префунктор, расширяющий φ и сохраняющий развороты.
LaTeX
$$$ (\\forall X Y, f, \\, Φ.map(\\mathrm{reverse} f) = \\mathrm{reverse}(\\Phi.map f)) \\wedge (of \\;⋙q\\; Φ) = φ \\Rightarrow Φ = \\mathrm{Symmetrify.lift} φ $$$
Lean4
/-- `lift φ` is the only prefunctor extending `φ` and preserving reverses. -/
theorem lift_unique [HasReverse V'] (φ : V ⥤q V') (Φ : Symmetrify V ⥤q V') (hΦ : (of ⋙q Φ) = φ)
(hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) :
Φ = Symmetrify.lift φ := by
subst_vars
fapply Prefunctor.ext
· rintro X
rfl
· rintro X Y f
cases f
· rfl
· exact hΦinv (Sum.inl _)
