# mathlibdocumentation

category_theory.bicategory.single_obj

# 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.star = 𝟙 _.
@[nolint]
def category_theory.monoidal_single_obj (C : Type u_1)  :
Sort u_3

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
Instances for category_theory.monoidal_single_obj
@[protected, instance]
@[protected, instance]
Equations
@[protected, nolint]

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

Equations
@[simp]
@[simp]
@[simp]

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
@[simp]
theorem category_theory.monoidal_single_obj.End_monoidal_star_functor_to_lax_monoidal_functor_μ (C : Type u_1)  :
= 𝟙 ({obj := , map := λ (X Y : (f : X Y), f, map_id' := _, map_comp' := _}.obj X {obj := , map := λ (X Y : (f : X Y), f, map_id' := _, map_comp' := _}.obj Y)

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