English
Let C be a monoidal closed category and J a small category. For any functors F1, F2, F3 : J ⥤ C, there exists a natural bijection between morphisms F1 ⊗ F2 ⟶ F3 in the functor category and morphisms F2 ⟶ functorEnrichedHom C F1 F3 in the enriched functor category.
Русский
Пусть C — моноидальная замкнутая категория и J — маленькая категория. Пусть F1, F2, F3 : J ⥤ C — произвольные_functor. Тогда существует естественная биекция между морфизмами F1 ⊗ F2 ⟶ F3 в категории функторов и морфизмами F2 ⟶ functorEnrichedHom C F1 F3 в обогащённой категории функторов.
LaTeX
$$$ (F_1 \\otimes F_2 \\to F_3) \\cong (F_2 \\to \\mathrm{functorEnrichedHom}~C~F_1~F_3) $$$
Lean4
/-- The bijection `(F₁ ⊗ F₂ ⟶ F₃) ≃ (F₂ ⟶ functorEnrichedHom C F₁ F₃)` when `F₁`, `F₂`
and `F₃` are functors `J ⥤ C`, and `C` is monoidal closed. -/
noncomputable def homEquiv : (F₁ ⊗ F₂ ⟶ F₃) ≃ (F₂ ⟶ functorEnrichedHom C F₁ F₃)
where
toFun
f :=
{
app
j :=
end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right))
(fun k₁ k₂ φ ↦ by
dsimp
simp only [enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Category.assoc,
enrichedOrdinaryCategorySelf_eHomWhiskerRight]
rw [← curry_natural_left_assoc, ← curry_natural_left_assoc, ← curry_natural_right, curry_pre_app,
Category.assoc, ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc, ← Under.w φ,
Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange_assoc]) }
invFun
g :=
{ app j := uncurry (g.app j ≫ enrichedHomπ C _ _ (Under.mk (𝟙 j)))
naturality j j'
φ := by
dsimp
rw [← uncurry_natural_right, tensorHom_def'_assoc, ← uncurry_pre_app, ← uncurry_natural_left, Category.assoc,
Category.assoc, NatTrans.naturality_assoc, functorEnrichedHom_map, end_.lift_π_assoc,
enrichedOrdinaryCategorySelf_eHomWhiskerRight]
dsimp
rw [pre_id, NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Functor.map_id, Category.comp_id,
Category.comp_id]
congr 2
dsimp
rw [← enrichedOrdinaryCategorySelf_eHomWhiskerRight, ← enrichedOrdinaryCategorySelf_eHomWhiskerLeft]
let α : Under.mk (𝟙 j) ⟶ (Under.map φ).obj (Under.mk (𝟙 j')) := Under.homMk φ
exact (enrichedHom_condition C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) α).symm }
left_inv f := by cat_disch
right_inv
g := by
ext j
dsimp
ext k
simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, enrichedCategorySelf_hom, curry_uncurry,
NatTrans.naturality_assoc, functorEnrichedHom_obj, functorEnrichedHom_map, Under.map, Comma.mapLeft,
Functor.const_obj_obj, Functor.id_obj, Discrete.natTrans_app, StructuredArrow.left_eq_id, end_.lift_π,
Under.mk_right, Under.mk_hom, Iso.refl_inv, NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerRight,
pre_id, Iso.refl_hom, enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Functor.map_id, Category.comp_id]
congr
simp
