Theorems · Definition · category theory

CategoryTheory.reverseBraiding

(C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory C

The braided monoidal category obtained from C by replacing its braiding β_ X Y : X ⊗ Y ≅ Y ⊗ X with the inverse (β_ Y X)⁻¹ : X ⊗ Y ≅ Y ⊗ X. This corresponds to the automorphism of the braid group swapping over-crossings and under-crossings.

Defined in

Mathlib.CategoryTheory.Monoidal.Braided.Basic

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategory