English
Let f: SingleObj α ⥤q SingleObj β and g: SingleObj β ⥤q SingleObj γ be prefuntors. The inverse prefunctor of the composite equals the composition of the inverse prefuntors in reverse order: toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f.
Русский
Пусть f: SingleObj α ⥤q SingleObj β и g: SingleObj β ⥤q SingleObj γ — предфункторы. Обратный префунктор к их композиции равен композицие обратных префункторов в обратном порядке: toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f.
LaTeX
$$$ \\mathrm{toPrefunctor.symm}(f \\;⋙q\\; g) = \\mathrm{toPrefunctor.symm}\, g \\circ \\mathrm{toPrefunctor.symm}\, f $$$
Lean4
@[simp]
theorem toPrefunctor_symm_comp (f : SingleObj α ⥤q SingleObj β) (g : SingleObj β ⥤q SingleObj γ) :
toPrefunctor.symm (f ⋙q g) = toPrefunctor.symm g ∘ toPrefunctor.symm f := by
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]
