Mathlib Map

Structures · Category theory

CategoryTheory.BraidedCategory

A braided monoidal category is a monoidal category equipped with a braiding isomorphism β_ X Y : X ⊗ Y ≅ Y ⊗ X which is natural in both arguments, and also satisfies the two hexagon identities.

Defined in
Mathlib.CategoryTheory.Monoidal.Braided.Basic
Shape
One type argument · adds braiding, braiding_naturality_right, braiding_naturality_left, hexagon_forward, hexagon_reverse
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Concrete types that are instances27

  • CategoryTheory.Functor
  • CategoryTheory.Over
  • CategoryTheory.Discrete
  • ModuleCat
  • CategoryTheory.Grp
  • Action
  • AlgebraicGeometry.Scheme
  • AddCommGrpCat
  • CategoryTheory.ObjectProperty.FullSubcategory
  • TopCat
  • CategoryTheory.MonoidalOpposite
  • Rep
  • CommGrpCat
  • GrpCat
  • AddGrpCat
  • CategoryTheory.Skeleton
  • AlgCat
  • CategoryTheory.GradedObject
  • CategoryTheory.Center
  • CategoryTheory.AddGrp
  • QuadraticModuleCat
  • CategoryTheory.Monoidal.Transported
  • CommAlgCat
  • CategoryTheory.WideSubcategory
  • CategoryTheory.LocalizedMonoidal
  • CategoryTheory.Cat
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by1,066

Ancestors0

No ancestors.