Monoidal categories

Monoidal categories equip a category with a tensor product and unit object, with braided and symmetric variants governing how tensor factors may be exchanged.

TheoremTensor inverses are unique up to isomorphism in braided categories#✓fully proved

In a braided monoidal category, tensoring with the unit is cancellative up to isomorphism: if M ⊗ N ≅ 𝟙, M' ⊗ N' ≅ 𝟙, and M ≅ M', then N ≅ N'.

theorem CategoryTheory.MonoidalCategory.nonempty_iso_of_tensor_iso_tensorUnit
    {C : Type u} [Category.{v} C] [MonoidalCategory C] [BraidedCategory C]
    {M N M' N' : C} (e : M ≅ M') (h : Nonempty (M ⊗ N ≅ 𝟙_ C))
    (h' : Nonempty (M' ⊗ N' ≅ 𝟙_ C)) :
    Nonempty (N ≅ N')

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.