braiding

Mathlib.CategoryTheory.GradedObject.Braiding

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GradedObject.Monoidal.braiding

Lean4

/-- The braiding `tensorObj X Y ≅ tensorObj Y X` when `X` and `Y` are graded objects
indexed by a commutative additive monoid. -/
noncomputable def braiding [HasTensor X Y] [HasTensor Y X] : tensorObj X Y ≅ tensorObj Y X
    where
  hom k := tensorObjDesc (fun i j hij => (β_ _ _).hom ≫ ιTensorObj Y X j i k (by simpa only [add_comm j i] using hij))
  inv k := tensorObjDesc (fun i j hij => (β_ _ _).inv ≫ ιTensorObj X Y j i k (by simpa only [add_comm j i] using hij))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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