English
Given V and a V-enriched ordinary category C with functors F1,F2: J ⥤ C, there is a bijection between morphisms F1 ⟶ F2 and morphisms from the tensor unit to enrichedHom V F1 F2, capturing the universal property of enriched homs.
Русский
Для данных V и обогащённой V-обычной категории C с функторaми F1,F2: J ⥤ C существует биекция между морфизмами F1 ⟶ F2 и морфизмами от тензорной единицы к enrichedHom V F1 F2, выражающая универсальную свойствo обогащённой гом.
LaTeX
$$$ (F_1 \\to F_2) \\cong (\\mathbf{1}_V \\to \\mathrm{enrichedHom} 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₂) ≃ (𝟙_ V ⟶ enrichedHom V F₁ F₂)`. -/
noncomputable def homEquiv : (F₁ ⟶ F₂) ≃ (𝟙_ V ⟶ enrichedHom V F₁ F₂)
where
toFun
τ :=
end_.lift (fun j ↦ eHomEquiv V (τ.app j))
(fun i j f ↦ by
trans eHomEquiv V (τ.app i ≫ F₂.map f)
· dsimp
simp only [eHomEquiv_comp, tensorHom_def_assoc, MonoidalCategory.whiskerRight_id, ← unitors_equal, assoc,
Iso.inv_hom_id_assoc, eHomWhiskerLeft]
· dsimp
simp only [← NatTrans.naturality, eHomEquiv_comp, tensorHom_def', id_whiskerLeft, assoc, Iso.inv_hom_id_assoc,
eHomWhiskerRight])
invFun
g :=
{ app := fun j ↦ (eHomEquiv V).symm (g ≫ end_.π _ j)
naturality := fun i j f ↦
(eHomEquiv V).injective
(by
simp only [eHomEquiv_comp, Equiv.apply_symm_apply, Iso.cancel_iso_inv_left]
conv_rhs =>
rw [tensorHom_def_assoc, MonoidalCategory.whiskerRight_id_assoc, assoc, enrichedHom_condition' V F₁ F₂ f]
conv_lhs =>
rw [tensorHom_def'_assoc, MonoidalCategory.whiskerLeft_comp_assoc, id_whiskerLeft_assoc,
id_whiskerLeft_assoc, Iso.inv_hom_id_assoc, unitors_equal]) }
left_inv τ := by aesop
right_inv g := by aesop
