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) [Category.{v, u} C] [MonoidalCategory C] :
Type

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) [Category.{v, u} C] [MonoidalCategory C] :
      Inhabited (MonoidalSingleObj C)
      Equations
        source
        instance CategoryTheory.instBicategoryMonoidalSingleObj (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
        Bicategory (MonoidalSingleObj C)
        Equations
          source
          def CategoryTheory.MonoidalSingleObj.star (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
          MonoidalSingleObj C

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

          Equations
            Instances For
              source
              def CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor (C : Type u) [Category.{v, u} 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
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_map (C : Type u) [Category.{v, u} C] [MonoidalCategory C] {X✝ Y✝ : EndMonoidal (MonoidalSingleObj.star C)} (f : X✝ ⟶ Y✝) :
                  (endMonoidalStarFunctor C).map f = f
                  source
                  @[simp]
                  theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_obj (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X : EndMonoidal (MonoidalSingleObj.star C)) :
                  (endMonoidalStarFunctor C).obj X = X
                  source
                  instance CategoryTheory.MonoidalSingleObj.instMonoidalEndMonoidalStarEndMonoidalStarFunctor (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
                  (endMonoidalStarFunctor C).Monoidal
                  Equations
                    source
                    noncomputable def CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence (C : Type u) [Category.{v, u} 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
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_map (C : Type u) [Category.{v, u} C] [MonoidalCategory C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                        (endMonoidalStarFunctorEquivalence C).inverse.map f = f
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_counitIso (C : Type u) [Category.{v, u} 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))
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_unitIso (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
                        (endMonoidalStarFunctorEquivalence C).unitIso = Iso.refl (Functor.id (EndMonoidal (MonoidalSingleObj.star C)))
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_functor (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
                        (endMonoidalStarFunctorEquivalence C).functor = endMonoidalStarFunctor C
                        source
                        @[simp]
                        theorem CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_obj (C : Type u) [Category.{v, u} C] [MonoidalCategory C] (X : C) :
                        (endMonoidalStarFunctorEquivalence C).inverse.obj X = X
                        source
                        instance CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor_isEquivalence (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :
                        (endMonoidalStarFunctor C).IsEquivalence