English
For f: F1 ⊗ F2 ⟶ F3 and f3: F3 ⟶ F3', the naturality of the homEquiv with respect to f3 expresses as an equality between the image of f ≫ f3 under homEquiv and a certain composed expression involving f, f3 and the enriched hom functor.
Русский
Для f: F1 ⊗ F2 ⟶ F3 и f3: F3 ⟶ F3' естественность гом-эквивариантности по отношению к f3 даёт равенство между образом f ≫ f3 и соответствующим композиционным выражением, включающим f, f3 и обогащённую Hom-функцию.
LaTeX
$$$ \\mathrm{homEquiv}(f \\;\\circ\\; f_3) = \\mathrm{homEquiv}(f) \\;\\circ\\; \\rho^{-1} \\;\\triangleleft\\; \\mathrm{functorHomEquiv}~f_3 \\;\\circ\\; \\mathrm{functorEnrichedComp}~C~F_1~F_3~F_3' $$$
Lean4
theorem homEquiv_naturality_three [∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂] (f : F₁ ⊗ F₂ ⟶ F₃) (f₃ : F₃ ⟶ F₃') :
homEquiv (f ≫ f₃) = homEquiv f ≫ (ρ_ _).inv ≫ _ ◁ functorHomEquiv _ f₃ ≫ functorEnrichedComp C F₁ F₃ F₃' :=
by
dsimp [homEquiv]
ext j
dsimp
ext k
rw [Category.assoc, Category.assoc, Category.assoc, end_.lift_π, enrichedComp_π, tensorHom_def, Category.assoc,
whisker_exchange_assoc, whiskerRight_id_assoc, Iso.inv_hom_id_assoc, end_.lift_π_assoc, Category.assoc, ←
MonoidalCategory.whiskerLeft_comp_assoc, Category.assoc, end_.lift_π, enrichedOrdinaryCategorySelf_eHomWhiskerRight,
enrichedOrdinaryCategorySelf_eHomWhiskerLeft]
dsimp
rw [pre_id, NatTrans.id_app, Functor.map_id, Category.comp_id, Category.comp_id, homEquiv_apply_π,
curry_natural_right]
congr 2
symm
apply enrichedOrdinaryCategorySelf_eHomWhiskerLeft
