English
The composition formula for homEquiv in the enriched functor category, expressed pointwise on j.
Русский
Формула композиции для гомэквивалентности в обогащённой категории функторов выражена по точкам j.
LaTeX
$$$\\mathrm{homEquiv}(f \\circ g) = (\\lambda_{\\mathbf{1}_V})^{-1} \\circ (\\mathrm{homEquiv} f \\otimes \\mathrm{homEquiv} g) \\circ \\mathrm{enrichedComp}(f,g)$$$
Lean4
@[reassoc]
theorem enriched_assoc [HasEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₃] [HasEnrichedHom V F₁ F₄]
[HasEnrichedHom V F₂ F₃] [HasEnrichedHom V F₂ F₄] [HasEnrichedHom V F₃ F₄] :
(α_ (enrichedHom V F₁ F₂) (enrichedHom V F₂ F₃) (enrichedHom V F₃ F₄)).inv ≫
enrichedComp V F₁ F₂ F₃ ▷ enrichedHom V F₃ F₄ ≫ enrichedComp V F₁ F₃ F₄ =
enrichedHom V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄ ≫ enrichedComp V F₁ F₂ F₄ :=
by
ext j
conv_lhs =>
rw [assoc, assoc, enrichedComp_π, tensorHom_def_assoc, ← comp_whiskerRight_assoc, enrichedComp_π,
comp_whiskerRight_assoc, ← whisker_exchange_assoc, ← whisker_exchange_assoc, ← tensorHom_def'_assoc, ←
associator_inv_naturality_assoc]
conv_rhs =>
rw [assoc, enrichedComp_π, tensorHom_def'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, enrichedComp_π,
MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange_assoc, whisker_exchange_assoc, ← tensorHom_def_assoc]
dsimp
rw [e_assoc]
