English
In a monoidal category, the inverse associator respects compositions with a left-tensored composite. For f: X1 → X2, g: Y1 → Y2, h: Z1 → Z2, and fg: X2 ⊗ Y2 → W, we have α_{X1,Y1,Z1}^{-1} ≫ (((f ⊗ g) ≫ fg) ⊗ h) = (f ⊗ g ⊗ h) ≫ α_{X2,Y2,Z2}^{-1} ≫ (fg ⊗ 𝟙).
Русский
В моноидальной категории обратный ассоциатор сохраняет совместимость с композициями после левого тензорирования. Для f: X1 → X2, g: Y1 → Y2, h: Z1 → Z2 и fg: X2 ⊗ Y2 → W имеем α_{X1,Y1,Z1}^{-1} ≫ (((f ⊗ g) ≫ fg) ⊗ h) = (f ⊗ g ⊗ h) ≫ α_{X2,Y2,Z2}^{-1} ≫ (fg ⊗ 𝟙).
LaTeX
$$$ \alpha_{X_1 Y_1 Z_1}^{-1} \circ (((f \otimes g) \circ fg) \otimes h) = (f \otimes g \otimes h) \circ \alpha_{X_2 Y_2 Z_2}^{-1} \circ (fg \otimes \mathrm{Id})$$$
Lean4
@[reassoc (attr := mon_tauto)]
theorem associator_inv_comp_tensorHom_tensorHom_comp (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (fg : X₂ ⊗ Y₂ ⟶ W) :
(α_ X₁ Y₁ Z₁).inv ≫ (((f ⊗ₘ g) ≫ fg) ⊗ₘ h) = (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).inv ≫ (fg ⊗ₘ 𝟙 _) := by
simp [tensorHom_def']
