English
For any M,N in ModuleCat and P in ModuleCat, the pre-application map (MonoidalClosed.pre f).app P is given by the composition with homLinearEquiv; explicitly, it equals ofHom (homLinearEquiv.symm.toLinearMap ∘ₗ LinearMap.lcomp _ _ f.hom ∘ₗ homLinearEquiv.toLinearMap).
Русский
Для любых M,N в ModuleCat и P в ModuleCat пред-применяющее отображение (MonoidalClosed.pre f).app P задаётся композициями через homLinearEquiv; строго: ...
LaTeX
$$$(\\mathrm{MonoidalClosed.pre}\\ f).\\mathrm{app}\\ P = \\mathrm{ofHom}(\\mathrm{homLinearEquiv.symm.toLinearMap} \\circ_ℓ \\mathrm{LinearMap.lcomp} \\_ \\_ f.hom \\circ_ℓ \\mathrm{homLinearEquiv.toLinearMap})$$$
Lean4
theorem monoidalClosed_pre_app {M N : ModuleCat.{u} R} (P : ModuleCat.{u} R) (f : N ⟶ M) :
(MonoidalClosed.pre f).app P =
ofHom (homLinearEquiv.symm.toLinearMap ∘ₗ LinearMap.lcomp _ _ f.hom ∘ₗ homLinearEquiv.toLinearMap) :=
rfl
