Theorems · Inductive type · category theory
CategoryTheory.BraidedCategory
(C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)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.
- Cited by
- 779 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.MonoidalCategorystatement · cited by 3,095
Cited by1,087
Results whose statement or proof uses this declaration.
- CategoryTheory.BraidedCategory.braidingstatement and proof · cited by 257
- CategoryTheory.CommMonstatement · cited by 85
- CategoryTheory.CommGrpstatement · cited by 74
- CategoryTheory.MonoidalCategory.tensorμstatement and proof · cited by 71
- CategoryTheory.CommMon.Xstatement and proof · cited by 50
- CategoryTheory.CommGrp.Xstatement and proof · cited by 39
- CategoryTheory.Bimonstatement and proof · cited by 37
- CategoryTheory.IsCommMonObjstatement · cited by 37
- CategoryTheory.CommMon.toMonstatement and proof · cited by 36
- CategoryTheory.CommGrp.toGrpstatement and proof · cited by 34
- CategoryTheory.LaxBraidedFunctorstatement · cited by 33
- CategoryTheory.Functor.Braidedstatement · cited by 32
Showing the 200 most cited of 1,087.