English
The composition formula for functorHomEquiv is compatible with left unitor and enriched composition; it expresses how the image of a composite is built from images of the factors.
Русский
Формула композиции для functorHomEquiv совместима с левым унитором и обогащённой композицией; выражает, как образ композиции строится из образов факторов.
LaTeX
$$$\text{(functorHomEquiv } V)\ (f \gg g) = (\lambda_{(\mathbf{1}_{J\to V})})^{-1} \gg ((\text{functorHomEquiv } V)f \otimes_{\mathsf{t}} (\text{functorHomEquiv } V)g) \gg \text{functorEnrichedComp } V F_1 F_2 F_3.$$$
Lean4
/-- `eHomCongr` respects composition of morphisms. Recall that for any
composable pair of arrows `f : X ⟶ Y` and `g : Y ⟶ Z` in `C`, the composite
`f ≫ g` in `C` defines a morphism `𝟙_ V ⟶ (X ⟶[V] Z)` in `V`. Composing with
the isomorphism `eHomCongr V α γ` yields a morphism in `V` that can be factored
through the enriched composition map as shown:
`𝟙_ V ⟶ 𝟙_ V ⊗ 𝟙_ V ⟶ (X₁ ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z₁) ⟶ (X₁ ⟶[V] Z₁)`. -/
@[reassoc]
theorem eHomCongr_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) :
eHomEquiv V (f ≫ g) ≫ (eHomCongr V α γ).hom =
(λ_ _).inv ≫
(eHomEquiv V f ≫ (eHomCongr V α β).hom) ▷ _ ≫ _ ◁ (eHomEquiv V g ≫ (eHomCongr V β γ).hom) ≫ eComp V X₁ Y₁ Z₁ :=
by
simp only [eHomCongr, MonoidalCategory.whiskerRight_id, assoc, MonoidalCategory.whiskerLeft_comp]
rw [rightUnitor_inv_naturality_assoc, rightUnitor_inv_naturality_assoc, rightUnitor_inv_naturality_assoc,
hom_inv_id_assoc, ← whisker_exchange_assoc, ← whisker_exchange_assoc, ← eComp_eHomWhiskerLeft,
eHom_whisker_cancel_assoc, ← eComp_eHomWhiskerRight_assoc, ← tensorHom_def_assoc, ← eHomEquiv_comp_assoc]
