Theorems · Theorem · category theory

CategoryTheory.tensorHom_eComp_op_eq

∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] {C : Type u} [inst_3 : CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ}
  {v w : V} (f : v ⟶ z ⟶[V] y) (g : w ⟶ y ⟶[V] x),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.eComp V z y x) =
    CategoryTheory.CategoryStruct.comp (β_ v w).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
        (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)))

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.

Defined in

Mathlib.CategoryTheory.Enriched.Opposite

Cited by

1 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategoryCategoryTheory.EnrichedCategory