tensorδ

Mathlib.CategoryTheory.Monoidal.Braided.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.tensorδ

Lean4

/-- The inverse of `tensorμ`. -/
def tensorδ (X₁ X₂ Y₁ Y₂ : C) : (X₁ ⊗ Y₁) ⊗ X₂ ⊗ Y₂ ⟶ (X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂ :=
  (α_ X₁ Y₁ (X₂ ⊗ Y₂)).hom ≫
    (X₁ ◁ (α_ Y₁ X₂ Y₂).inv) ≫ (X₁ ◁ (β_ X₂ Y₁).inv ▷ Y₂) ≫ (X₁ ◁ (α_ X₂ Y₁ Y₂).hom) ≫ (α_ X₁ X₂ (Y₁ ⊗ Y₂)).inv

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

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

Разделы

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

Аффилиация

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