eHomEquiv_comp — Mathlib

English

The image of a composite under eHomEquiv is the composite of images under eHomEquiv, up to the left unitor and enriched tensor product.

Русский

Образ композиции f∘g под eHomEquiv равен композиции образов f и g с учётом левого унитора и обогащённого тензорного произведения.

LaTeX

$$$eHomEquiv\,V\,(f \circ g) = (\lambda_{ }^{-1}) \circ (eHomEquiv\,V\,f \otimes\, eHomEquiv\,V\,g) \circ eComp\,V\,X\,Y\,Z.$$$

Lean4

@[reassoc]
theorem eHomEquiv_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    eHomEquiv V (f ≫ g) = (λ_ _).inv ≫ (eHomEquiv V f ⊗ₘ eHomEquiv V g) ≫ eComp V X Y Z :=
  EnrichedOrdinaryCategory.homEquiv_comp _ _

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