The interchange tensorμ intertwines the braidings

In a symmetric monoidal category the interchange morphism tensorμ a b c d : (a ⊗ b) ⊗ (c ⊗ d) ⟶ (a ⊗ c) ⊗ (b ⊗ d) makes the tensor product a braided functor: braiding the two tensor pairs and then interchanging agrees with interchanging and then braiding slotwise. Mathlib records only the diagonal special case SymmetricCategory.tensorμ_braid_swap; this file proves the general four-object statement.

The proof decomposes the block braiding β_ (a ⊗ b) (c ⊗ d) into the four elementary crossings β_ b c, β_ b d, β_ a c, β_ a d via the hexagon identities; the crossing β_ d a supplied by tensorμ c d a b then cancels β_ a d by the symmetry axiom, and one exchange of the disjoint crossings β_ a c and β_ b d produces the right-hand side.

theorem RS.tensorμ_braiding {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (a b c d : D) : CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) (CategoryTheory.MonoidalCategoryStruct.tensorObj c d)).hom (CategoryTheory.MonoidalCategory.tensorμ c d a b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ a b c d) (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ a c).hom (β_ b d).hom)

In a symmetric category the interchange tensorμ makes the tensor product a braided functor: braiding the tensor pairs and then interchanging equals interchanging and then braiding slotwise.

theorem RS.tensorμ_braiding_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (a b c d : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj c a) (CategoryTheory.MonoidalCategoryStruct.tensorObj d b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj a b) (CategoryTheory.MonoidalCategoryStruct.tensorObj c d)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ c d a b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ a b c d) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (β_ a c).hom (β_ b d).hom) h)

In a symmetric category the interchange tensorμ makes the tensor product a braided functor: braiding the tensor pairs and then interchanging equals interchanging and then braiding slotwise.

theorem RS.tensor_evaluation_braiding {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y P Q : D) [CategoryTheory.ExactPairing X P] [CategoryTheory.ExactPairing Y Q] : ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ P Q).hom (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q P) (β_ Y X).hom) (ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj Q P)))

The tensor evaluation of ExactPairing.tensor is compatible with the braidings: crossing the two dual pairs converts the arc nesting of the double evaluation, inner (Q, Y)/outer (P, X) against inner (P, X)/outer (Q, Y).

theorem RS.tensor_evaluation_braiding_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y P Q : D) [CategoryTheory.ExactPairing X P] [CategoryTheory.ExactPairing Y Q] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryTheory.CategoryStruct.comp (ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ P Q).hom (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Q P) (β_ Y X).hom) (CategoryTheory.CategoryStruct.comp (ε_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj Q P)) h))

The tensor evaluation of ExactPairing.tensor is compatible with the braidings: crossing the two dual pairs converts the arc nesting of the double evaluation, inner (Q, Y)/outer (P, X) against inner (P, X)/outer (Q, Y).