Mathlib Map

Structures · Category theory

CategoryTheory.MonoidalCategory

In a monoidal category, we can take the tensor product of objects, X ⊗ Y and of morphisms f ⊗ₘ g. Tensor product does not need to be strictly associative on objects, but there is a specified associator, α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z). There is a tensor unit 𝟙_ C, with specified left and right unitor isomorphisms λ_ X : 𝟙_ C ⊗ X ≅ X and ρ_ X : X ⊗ 𝟙_ C ≅ X. These associators and unitors satisfy the pentagon and triangle equations.

Defined in
Mathlib.CategoryTheory.Monoidal.Category
Shape
One type argument · adds tensorHom_def, id_tensorHom_id, tensorHom_comp_tensorHom, whiskerLeft_id, id_whiskerRight, associator_naturality, leftUnitor_naturality, rightUnitor_naturality, pentagon, triangle
Open in Mathlib docs

Extends1

Extended by1

Concrete types that are instances37

  • Quiver.Hom
  • CategoryTheory.Functor
  • CategoryTheory.Discrete
  • ModuleCat
  • CategoryTheory.Grp
  • HomologicalComplex
  • Action
  • CategoryTheory.Mon
  • CategoryTheory.ObjectProperty.FullSubcategory
  • CategoryTheory.MonoidalOpposite
  • Rep
  • CategoryTheory.Skeleton
  • PresheafOfModules
  • CategoryTheory.Sheaf
  • AlgCat
  • CategoryTheory.GradedObject
  • CategoryTheory.Center
  • CategoryTheory.AddGrp
  • CategoryTheory.AddMon
  • QuadraticModuleCat
  • SemimoduleCat
  • CategoryTheory.Monoidal.Transported
  • CommAlgCat
  • HopfAlgCat
  • CategoryTheory.Comon
  • BialgCat
  • CategoryTheory.WideSubcategory
  • CategoryTheory.FreeMonoidalCategory
  • CoalgCat
  • CategoryTheory.Dial
  • CategoryTheory.LocalizedMonoidal
  • CategoryTheory.MonoidalCategory.DayFunctor
  • LightCondMod
  • SFinKer
  • AugmentedSimplexCategory
  • Prod
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by4,013

Ancestors1