English
Let V be a monoidal category enriching C, and F1, F2 be functors J ⥤ C. Then there exists a natural bijection between morphisms F1 ⟶ F2 in the functor category and enriched natural transformations 𝟙_{J ⥤ V} ⟶ functorEnrichedHom V F1 F2.
Русский
Пусть V — моноидальная категория, обогащающая C, и пусть F1, F2 — функторы J ⥤ C. Существет биекция между мороморфизмами F1 → F2 в категории функторов и обогащёнными естественными преобразованиями 𝟙_{J ⥤ V} ⟶ functorEnrichedHom V F1 F2.
LaTeX
$$$\operatorname{Nat}(F_1,F_2) \cong \operatorname{Hom}_{J\to V}( \mathbf{1}_{J\to V}, \mathrm{functorEnrichedHom}(V,F_1,F_2) ).$$$
Lean4
/-- Given functors `F₁` and `F₂` in `J ⥤ C`, where `C` is a `V`-enriched ordinary category,
this is the bijection `(F₁ ⟶ F₂) ≃ (𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂)`. -/
@[simps! apply_app]
noncomputable def functorHomEquiv [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] :
(F₁ ⟶ F₂) ≃ (𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂) :=
(homEquiv V).trans (isLimitConeFunctorEnrichedHom V F₁ F₂).homEquiv
