English
Let φ: V → V' be a prefunctor and Φ: Symmetrify V → V' a prefunctor. If (of ⋙q Φ) = φ and Φ preserves reverses, then Φ is the unique lift of φ, i.e., Φ = Symmetrify.lift φ.
Русский
Пусть φ: V → V' — префунктор, а Φ: Symmetrify V → V' — префунктор. Если (of ⋙q Φ) = φ и Φ сохраняет развороты, то Φ является единственным лифтингом φ, то есть Φ = Symmetrify.lift φ.
LaTeX
$$$ (\\forall X Y, f, \\, \\Phi.map(\\mathrm{reverse} f) = \\mathrm{reverse}(\\Phi.map f)) \\wedge (of \\;⋙q\\; Φ) = φ \\Rightarrow Φ = \\mathrm{Symmetrify.lift} φ $$$
Lean4
theorem lift_reverse [h : HasInvolutiveReverse V'] (φ : Prefunctor V V') {X Y : Symmetrify V} (f : X ⟶ Y) :
(Symmetrify.lift φ).map (Quiver.reverse f) = Quiver.reverse ((Symmetrify.lift φ).map f) :=
by
dsimp [Symmetrify.lift]; cases f
· simp only
rfl
· simp only [reverse_reverse]
rfl
