Promoting a monoidal category to a single object bicategory. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 = 𝟙 _.

source

@[nolint]

def category_theory.monoidal_single_obj (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] :

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

category_theory.monoidal_single_obj C = punit

Instances for category_theory.monoidal_single_obj

source

@[protected, instance]

def category_theory.monoidal_single_obj.inhabited (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] :

inhabited (category_theory.monoidal_single_obj C)

source

@[protected, instance]

def category_theory.monoidal_single_obj.bicategory (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.bicategory (category_theory.monoidal_single_obj C)

Equations

category_theory.monoidal_single_obj.bicategory C = {to_category_struct := {to_quiver := {hom := λ (_x _x : category_theory.monoidal_single_obj C), C}, id := λ (_x : category_theory.monoidal_single_obj C), 𝟙_ C, comp := λ (_x _x_1 _x_2 : category_theory.monoidal_single_obj C) (X : _x ⟶ _x_1) (Y : _x_1 ⟶ _x_2), X ⊗ Y}, hom_category := λ (_x _x : category_theory.monoidal_single_obj C), _inst_1, whisker_left := λ (_x _x_1 _x_2 : category_theory.monoidal_single_obj C) (X : _x ⟶ _x_1) (Y Z : _x_1 ⟶ _x_2) (f : Y ⟶ Z), 𝟙 X ⊗ f, whisker_right := λ (_x _x_1 _x_2 : category_theory.monoidal_single_obj C) (X Y : _x ⟶ _x_1) (f : X ⟶ Y) (Z : _x_1 ⟶ _x_2), f ⊗ 𝟙 Z, associator := λ (_x _x_1 _x_2 _x_3 : category_theory.monoidal_single_obj C) (X : _x ⟶ _x_1) (Y : _x_1 ⟶ _x_2) (Z : _x_2 ⟶ _x_3), α_ X Y Z, left_unitor := λ (_x _x_1 : category_theory.monoidal_single_obj C) (X : _x ⟶ _x_1), λ_ X, right_unitor := λ (_x _x_1 : category_theory.monoidal_single_obj C) (X : _x ⟶ _x_1), ρ_ X, whisker_left_id' := _, whisker_left_comp' := _, id_whisker_left' := _, comp_whisker_left' := _, id_whisker_right' := _, comp_whisker_right' := _, whisker_right_id' := _, whisker_right_comp' := _, whisker_assoc' := _, whisker_exchange' := _, pentagon' := _, triangle' := _}

source

@[protected, nolint]

def category_theory.monoidal_single_obj.star (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_single_obj C

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

Equations

category_theory.monoidal_single_obj.star C = punit.star

source

@[simp]

theorem category_theory.monoidal_single_obj.End_monoidal_star_functor_to_lax_monoidal_functor_ε (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_single_obj.End_monoidal_star_functor C).to_lax_monoidal_functor.ε = 𝟙 (𝟙_ C)

source

@[simp]

theorem category_theory.monoidal_single_obj.End_monoidal_star_functor_to_lax_monoidal_functor_to_functor_obj (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) :

(category_theory.monoidal_single_obj.End_monoidal_star_functor C).to_lax_monoidal_functor.to_functor.obj X = X

source

@[simp]

theorem category_theory.monoidal_single_obj.End_monoidal_star_functor_to_lax_monoidal_functor_to_functor_map (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) (f : X ⟶ Y) :

(category_theory.monoidal_single_obj.End_monoidal_star_functor C).to_lax_monoidal_functor.to_functor.map f = f

source

def category_theory.monoidal_single_obj.End_monoidal_star_functor (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_functor (category_theory.End_monoidal (category_theory.monoidal_single_obj.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

category_theory.monoidal_single_obj.End_monoidal_star_functor C = {to_lax_monoidal_functor := {to_functor := {obj := λ (X : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)), X, map := λ (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)), 𝟙 ({obj := λ (X : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)), X, map := λ (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}.obj X ⊗ {obj := λ (X : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)), X, map := λ (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

source

@[simp]

theorem category_theory.monoidal_single_obj.End_monoidal_star_functor_to_lax_monoidal_functor_μ (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) :

(category_theory.monoidal_single_obj.End_monoidal_star_functor C).to_lax_monoidal_functor.μ X Y = 𝟙 ({obj := λ (X : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)), X, map := λ (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}.obj X ⊗ {obj := λ (X : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)), X, map := λ (X Y : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}.obj Y)

source

noncomputable def category_theory.monoidal_single_obj.End_monoidal_star_functor_is_equivalence (C : Type u_1) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.is_equivalence (category_theory.monoidal_single_obj.End_monoidal_star_functor C).to_lax_monoidal_functor.to_functor

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

category_theory.monoidal_single_obj.End_monoidal_star_functor_is_equivalence C = {inverse := {obj := λ (X : C), X, map := λ (X Y : C) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}, unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.End_monoidal (category_theory.monoidal_single_obj.star C)), category_theory.as_iso (𝟙 ((𝟭 (category_theory.End_monoidal (category_theory.monoidal_single_obj.star C))).obj X))) _, counit_iso := category_theory.nat_iso.of_components (λ (X : C), category_theory.as_iso (𝟙 (({obj := λ (X : C), X, map := λ (X Y : C) (f : X ⟶ Y), f, map_id' := _, map_comp' := _} ⋙ (category_theory.monoidal_single_obj.End_monoidal_star_functor C).to_lax_monoidal_functor.to_functor).obj X))) _, functor_unit_iso_comp' := _}