English
The action of whiskering on the right by an identity morphism yields an identity in the enriched Hom.
Русский
Действие взятия за whisker справа от тождественного морфизма даёт тождественный элемент в обогащённой Hom.
LaTeX
$$$eHomWhiskerRight\,V\,(\mathbf{1}X)\,Y = \mathbf{1}.$$$
Lean4
/-- When composing a tensor product of morphisms with the `V`-composition morphism in `Cᵒᵖ`,
this re-writes the `V`-composition to be in `C` and moves the braiding to the left. -/
@[reassoc]
theorem tensorHom_eComp_op_eq {C : Type u} [EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V}
(f : v ⟶ EnrichedCategory.Hom z y) (g : w ⟶ EnrichedCategory.Hom y x) :
(f ⊗ₘ g) ≫ eComp V z y x = (β_ v w).hom ≫ (g ⊗ₘ f) ≫ eComp V x.unop y.unop z.unop :=
by
rw [eComp_op_eq]
exact
braiding_naturality_assoc f g
_
-- This section establishes the equivalence on underlying categories
