braiding_inv_apply

Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

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

English

The inverse braiding swaps back: (β_{M,N})^{-1}.hom (n ⊗ m) = m ⊗ n.

Русский

Обратный перепутыватель возвращает порядок: (β_{M,N})^{-1}.hom (n ⊗ m) = m ⊗ n.

LaTeX

$$$((\\beta_{M,N})^{-1})(n \\otimes m) = m \\otimes n$$$

Lean4

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

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

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

Разделы

Аффилиация

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