Promoting a monoidal category to a single object bicategory.

A monoidal category can be thought of as a bicategory with a single object.

The objects of the monoidal category become the 1-morphisms, with composition given by tensor product, and the morphisms of the monoidal category become the 2-morphisms.

We verify that the endomorphisms of that single object recovers the original monoidal category.

One could go much further: the bicategory of monoidal categories (equipped with monoidal functors and monoidal natural transformations) is equivalent to the bicategory consisting of

• single object bicategories,
• pseudofunctors, and
• (oplax) natural transformations η such that η.app PUnit.unit = 𝟙 _.

def CategoryTheory.MonoidalSingleObj (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] : Sort u_4

Promote a monoidal category to a bicategory with a single object. (The objects of the monoidal category become the 1-morphisms, with composition given by tensor product, and the morphisms of the monoidal category become the 2-morphisms.)

Equations

• CategoryTheory.MonoidalSingleObj C = PUnit.{u_4}

instance CategoryTheory.instInhabitedMonoidalSingleObj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Inhabited (CategoryTheory.MonoidalSingleObj C)

Equations

• CategoryTheory.instInhabitedMonoidalSingleObj C = id inferInstance

instance CategoryTheory.instBicategoryMonoidalSingleObj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Bicategory (CategoryTheory.MonoidalSingleObj C)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.MonoidalSingleObj.star (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalSingleObj C

The unique object in the bicategory obtained by "promoting" a monoidal category.

Equations

• CategoryTheory.MonoidalSingleObj.star C = PUnit.unit

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_toLaxMonoidalFunctor_μ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) (Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) : (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).toLaxMonoidalFunctor.μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) => X, map := fun {X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)} (f : X ⟶ Y) => f }).toPrefunctor.obj X) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) => X, map := fun {X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)} (f : X ⟶ Y) => f }).toPrefunctor.obj Y))

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_toLaxMonoidalFunctor_toFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : ∀ {X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)} (f : X ⟶ Y), (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).toLaxMonoidalFunctor.toFunctor.toPrefunctor.map f = f

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_toLaxMonoidalFunctor_toFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) : (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X = X

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_toLaxMonoidalFunctor_ε (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

def CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalFunctor (CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) C

The monoidal functor from the endomorphisms of the single object when we promote a monoidal category to a single object bicategory, to the original monoidal category.

We subsequently show this is an equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorIsEquivalence (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.IsEquivalence (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).toLaxMonoidalFunctor.toFunctor

The equivalence between the endomorphisms of the single object when we promote a monoidal category to a single object bicategory, and the original monoidal category.

Equations

• One or more equations did not get rendered due to their size.