English
For i, j in J and a morphism f: i ⟶ j, certain natural compatibility holds between the enriched hom components, the action of eHomEquiv, and the canonical tensor-related maps. This is a compatibility condition ensuring coherence of the enrichment with respect to morphisms in J.
Русский
Для i, j в J и морфизма f: i ⟶ j выполняется определенная естественная совместимость между компонентами обобщённых гомоморфизмов, действием eHomEquiv и каноническими тензорными отображениями. Это условие совместимости, обеспечивающее когерентность обогащения по отношению к морфизмам в J.
LaTeX
$$$\\text{enrichedHomπ } V F_1 F_2 i \\;\\circ\\; ρ^{-1} \\;\\circ\\; _ \\;\\triangleleft\\; (eHomEquiv V) (F_2.map f) \\;\\circ\\; eComp V \\_ _\\ _ =\\; \\text{enrichedHomπ } V F_1 F_2 j \\;\\circ\\; λ^{-1} \\;\\circ\\; (eHomEquiv V) (F_1.map f) \\;▷\\; _ \\circ\\; eComp V \\_ _ \\_. $$$
Lean4
@[reassoc]
theorem enrichedHom_condition' {i j : J} (f : i ⟶ j) :
enrichedHomπ V F₁ F₂ i ≫ (ρ_ _).inv ≫ _ ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V _ _ _ =
enrichedHomπ V F₁ F₂ j ≫ (λ_ _).inv ≫ (eHomEquiv V) (F₁.map f) ▷ _ ≫ eComp V _ _ _ :=
end_.condition (diagram V F₁ F₂) f
