The tensorμ interchange associativity #
The mixed associativity of the middle-four interchange: shuffling
first and regrouping equals regrouping blockwise and shuffling
twice. This is the symmetric-category companion of Mathlib's
tensor_associativity, with the shuffle on the other side; one
adjacent symmetry cancellation dissolves the doubled crossing.
Mixed associativity of the interchange: shuffling the first two
pairs and regrouping against Z₁ ⊗ Z₂ agrees with regrouping
blockwise and shuffling twice. The two block braidings on the right
decompose into four elementary crossings, of which the adjacent pair
β_ X₂ Z₁ ≫ β_ Z₁ X₂ cancels by the symmetry axiom; one exchange of
the disjoint surviving crossings then matches the left-hand side.
Mixed associativity of the interchange: shuffling the first two
pairs and regrouping against Z₁ ⊗ Z₂ agrees with regrouping
blockwise and shuffling twice. The two block braidings on the right
decompose into four elementary crossings, of which the adjacent pair
β_ X₂ Z₁ ≫ β_ Z₁ X₂ cancels by the symmetry axiom; one exchange of
the disjoint surviving crossings then matches the left-hand side.
The inverse-associator companion of tensorMu_assoc_swap:
shuffling the last two pairs and regrouping against Z₁ ⊗ Z₂ agrees
with regrouping blockwise and shuffling twice. The two block
braidings on the right decompose into four elementary crossings, of
which the adjacent pair β_ Z₂ Y₁ ≫ β_ Y₁ Z₂ cancels by the symmetry
axiom; one exchange of the disjoint surviving crossings then matches
the left-hand side.
The inverse-associator companion of tensorMu_assoc_swap:
shuffling the last two pairs and regrouping against Z₁ ⊗ Z₂ agrees
with regrouping blockwise and shuffling twice. The two block
braidings on the right decompose into four elementary crossings, of
which the adjacent pair β_ Z₂ Y₁ ≫ β_ Y₁ Z₂ cancels by the symmetry
axiom; one exchange of the disjoint surviving crossings then matches
the left-hand side.