hom_hom_associator — Mathlib

English

The associator morphism’s hom component corresponds to the associativity map on tensor products: (α_M N K).hom.hom = (Algebra.TensorProduct.assoc R R M N K).toAlgHom.

Русский

Гомоморфизм ассоциатора соответствует отображению ассоциативности на тензорных произведениях.

LaTeX

$$$$ (\alpha_{M N K}).hom.hom = (\operatorname{Algebra.TensorProduct.assoc} R R M N K).toAlgHom. $$$$

Lean4

theorem hom_hom_associator {M N K : AlgCat.{u} R} :
    (α_ M N K).hom.hom = (Algebra.TensorProduct.assoc R R M N K).toAlgHom :=
  rfl

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