associator_hom_comp_tensorHom_tensorHom

English

Duplicate naturality statement for associator with triple tensoring.

Русский

Дублирующее утверждение естественности ассоциатора по тройному тензорированию.

LaTeX

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

Lean4

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

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