homTo_comp — Mathlib

English

The underlying hom of a composition equals the left-unitor-adjusted tensor of the underlying hens plus the eComp correction.

Русский

Гомоморфизм подлежащий композиции равен композиции после применения левого единичного тождественного преобразования к тензору и затем корректируется через eComp.

LaTeX

$$$\\mathrm{homTo}_W(f \\circ g) = \\bigl( (\\lambda_{\\mathbf{1}_W})^{-1} \\;\\circ\\; (\\mathrm{homTo}_W f \\otimes \\mathrm{homTo}_W g) \\bigr) \\;\\circ\\; \\mathrm{eComp}_W(−,−,−)$$$

Lean4

/-- Composition in the "underlying" category of an enriched category. -/
@[simp]
theorem homTo_comp {X Y Z : ForgetEnrichment W C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    homTo W (f ≫ g) = ((λ_ (𝟙_ W)).inv ≫ (homTo W f ⊗ₘ homTo W g)) ≫ eComp W _ _ _ :=
  rfl

Похожие утверждения