Documentation

Mathlib.CategoryTheory.Bicategory.SingleObj

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

source
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
Instances For
    source
    instance CategoryTheory.instInhabitedMonoidalSingleObj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] :
    Inhabited (CategoryTheory.MonoidalSingleObj C)
    Equations
    source
    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.
    source
    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
    Instances For
      source
      @[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).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ({ toPrefunctor := { 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) ({ toPrefunctor := { 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 Y))
      source
      @[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
      source
      @[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
      source
      @[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)
      source
      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.
      Instances For
        source
        noncomputable def CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorIsEquivalence (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] :
        CategoryTheory.Functor.IsEquivalence (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).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.
        Instances For