English
The functorHomEquiv respects composition: the image of a composite f ≫ g is obtained by composing the images of f and g via the tensor product and the enriched composition, up to the left unitor.
Русский
Функторактивная биекция сохраняет композицию: образ композиции f ∘ g получаем как композицию образов f и g через тензор и обогащённую композицию, с учётом левого унитора.
LaTeX
$$$\mathrm{functorHomEquiv}(V)(f \circ g) = (\lambda_{(\mathbf{1}_{J\to V})})^{-1} \circ (\mathrm{functorHomEquiv}(V)f \otimes \mathrm{functorHomEquiv}(V)g) \circ \mathrm{functorEnrichedComp}(V,F_1,F_2,F_3).$$$
Lean4
theorem functorHomEquiv_comp [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃]
[HasEnrichedHom V F₂ F₃] [HasFunctorEnrichedHom V F₁ F₃] [HasEnrichedHom V F₁ F₃] (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) :
(functorHomEquiv V) (f ≫ g) =
(λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ₘ (functorHomEquiv V) g) ≫ functorEnrichedComp V F₁ F₂ F₃ :=
by
ext j
dsimp
ext k
rw [homEquiv_comp, assoc, assoc, assoc, assoc, assoc, end_.lift_π, enrichedComp_π]
simp [tensorHom_comp_tensorHom_assoc]
