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) [Category.{u_3, u_2} C] [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.22}

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

Equations

• CategoryTheory.instInhabitedMonoidalSingleObj C = id inferInstance

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

Equations

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

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

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

Equations

• CategoryTheory.MonoidalSingleObj.star C = PUnit.unit

def CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : Functor (EndMonoidal (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.

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X✝ Y✝ : EndMonoidal (MonoidalSingleObj.star C)} (f : X✝ ⟶ Y✝) : (endMonoidalStarFunctor C).map f = f

@[simp]

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

instance CategoryTheory.MonoidalSingleObj.instMonoidalEndMonoidalStarEndMonoidalStarFunctor (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : (endMonoidalStarFunctor C).Monoidal

Equations

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

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

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.

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_unitIso (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : (endMonoidalStarFunctorEquivalence C).unitIso = Iso.refl (Functor.id (EndMonoidal (MonoidalSingleObj.star C)))

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_counitIso (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : (endMonoidalStarFunctorEquivalence C).counitIso = Iso.refl ({ obj := fun (X : C) => X, map := fun {X Y : C} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }.comp (endMonoidalStarFunctor C))

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (endMonoidalStarFunctorEquivalence C).inverse.map f = f

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (X : C) : (endMonoidalStarFunctorEquivalence C).inverse.obj X = X

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_functor (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : (endMonoidalStarFunctorEquivalence C).functor = endMonoidalStarFunctor C

instance CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_isEquivalence (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] : (endMonoidalStarFunctor C).IsEquivalence