hom_inv_associator — Mathlib

English

The inverse of the associator’s hom component corresponds to the inverse associativity map: (α_M N K).inv.hom = (Algebra.TensorProduct.assoc R R M N K).symm.toAlgHom.

Русский

Обратный к гомоморфизму ассоциатора отображает обратное отображение ассоциативности.

LaTeX

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

Lean4

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

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