braiding_hom_apply

Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

URI: https://scilib.ai/kg/mathlib#ModuleCat.MonoidalCategory.braiding_hom_apply

English

The braiding isomorphism swaps tensor factors: (β_{M,N}).hom (m ⊗ n) = n ⊗ m.

Русский

Схема перепутывания фактора в тензорном произведении: (β_{M,N}).hom (m ⊗ n) = n ⊗ m.

LaTeX

$$$((\\beta_{M,N})^{\\mathrm{hom}})(m \\otimes n) = n \\otimes m$$$

Lean4

@[simp]
theorem braiding_hom_apply {M N : ModuleCat.{u} R} (m : M) (n : N) : ((β_ M N).hom : M ⊗ N ⟶ N ⊗ M) (m ⊗ₜ n) = n ⊗ₜ m :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru