Theorems · Inductive type · category theory

CategoryTheory.MonoidalCategory

(C : Type u) → [𝒞 : CategoryTheory.Category.{v, u} C] → Type (max u v)

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

Cited by

3,095 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category