associator_inv_comp_tensorHom_tensorHom

English

In a monoidal category, the inverse associator is natural with respect to tensoring morphisms. Specifically, for all f: X1 → X2, g: Y1 → Y2, h: Z1 → Z2, we have α_{X1,Y1,Z1}^{-1} ∘ ((f ⊗ g) ⊗ h) = (f ⊗ g ⊗ h) ∘ α_{X2,Y2,Z2}^{-1}.

Русский

В моноидальной категории обратный ассоциатор естественен по отношению к тензорированию морфизмов: для любых f: X1 → X2, g: Y1 → Y2, h: Z1 → Z2 выполняется α_{X1,Y1,Z1}^{-1} ∘ ((f ⊗ g) ⊗ h) = (f ⊗ g ⊗ h) ∘ α_{X2,Y2,Z2}^{-1}.

LaTeX

$$$ (\alpha_{X_1 Y_1 Z_1})^{-1} \circ ((f \otimes g) \otimes h) = (f \otimes g \otimes h) \circ (\alpha_{X_2 Y_2 Z_2})^{-1} $$$

Lean4

@[reassoc (attr := mon_tauto)]
theorem associator_inv_comp_tensorHom_tensorHom (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) :
    (α_ X₁ Y₁ Z₁).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) = (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X₂ Y₂ Z₂).inv := by simp

Похожие утверждения