braiding_hom_hom — Mathlib

English

In the Monoidal category of commutative algebras, the hom component of the braiding is exactly the canonical commutativity map of the underlying algebras.

Русский

В моноидальной категории коммутативных алгебр компонент braiding'а на гом-составляющую совпадает с каноническим отображением перестановки основанных алгебр.

LaTeX

$$$\beta_A B).hom.hom = (comm\ R\ A.carrier B.carrier).toAlgHom$$$

Lean4

@[simp]
theorem braiding_hom_hom : (β_ A B).hom.hom = (comm R A B).toAlgHom :=
  rfl

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