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.22}

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

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.

@[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).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).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_toLaxMonoidalFunctor_μ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : ∀ (x x_1 : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)), (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).μ x x_1 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ({ obj := fun (X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) => X, map := fun {X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }.obj x) ({ obj := fun (X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)) => X, map := fun {X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)} (f : X ⟶ Y) => f, map_id := ⋯, map_comp := ⋯ }.obj x_1))

@[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).map f = f

noncomputable def CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.EndMonoidal (CategoryTheory.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) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯