English
If C is monoidal closed and has suitable limits, then for any functor F : J ⥤ C, the functor tensorLeft F has a right adjoint given by the enriched internal hom functor eHomFunctor C (applied to F).
Русский
Пусть C — моноидальная замкнутая категория с подходящими пределами. Тогда для любого функторa F: J ⥤ C fунктор tensorLeft F имеет правый сопряжённый, задаваемый обогащённой внутреннейHom-функцией eHomFunctor C.
LaTeX
$$$ \\text{tensorLeft } F \\dashv (eHomFunctor\\;\\_\\;\\_).\\mathrm{obj}\\;\\langle F \\rangle $$$
Lean4
/-- When `C` is monoidal closed and has suitable limits,
then for any `F : J ⥤ C`, `tensorLeft F` has a right adjoint. -/
noncomputable def adj (F : J ⥤ C) : MonoidalCategory.tensorLeft F ⊣ (eHomFunctor _ _).obj ⟨F⟩ :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun _ _ ↦ homEquiv
homEquiv_naturality_left_symm := homEquiv_naturality_two_symm
homEquiv_naturality_right := homEquiv_naturality_three }
