hom_hom_associator — Mathlib

English

The hom component of the associator is the canonical linear map for the tensor associativity: (α_M N K).hom = (TensorProduct.assoc _ _ _ _).toLinearMap.

Русский

Гом-компонента ассоциатора является канонической линейной картой ассоциативности тензора.

LaTeX

$$$ (\\alpha_{M,N,K}).hom = (\\text{TensorProduct}.assoc \\; R \\; M \\; N \\; K)^{\\toLinearMap} $$$

Lean4

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

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