From 6abb6de90754c5613a3aab6261eea9e5c72d539d Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Sat, 9 Apr 2022 17:28:05 +0000
Subject: [PATCH] feat(category_theory/bicategory): monoidal categories are
 single object bicategories (#13157)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 src/category_theory/bicategory/End.lean       |  41 +++++++
 src/category_theory/bicategory/basic.lean     |   2 +-
 .../bicategory/single_obj.lean                | 104 ++++++++++++++++++
 3 files changed, 146 insertions(+), 1 deletion(-)
 create mode 100644 src/category_theory/bicategory/End.lean
 create mode 100644 src/category_theory/bicategory/single_obj.lean

diff --git a/src/category_theory/bicategory/End.lean b/src/category_theory/bicategory/End.lean
new file mode 100644
index 0000000000000..f677e134b87f8
--- /dev/null
+++ b/src/category_theory/bicategory/End.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.bicategory.basic
+import category_theory.monoidal.category
+
+/-!
+# Endomorphisms of an object in a bicategory, as a monoidal category.
+-/
+
+namespace category_theory
+
+variables {C : Type*} [bicategory C]
+
+/-- The endomorphisms of an object in a bicategory can be considered as a monoidal category. -/
+@[derive category]
+def End_monoidal (X : C) := X ⟶ X
+
+instance (X : C) : inhabited (End_monoidal X) := ⟨𝟙 X⟩
+
+open_locale bicategory
+
+open monoidal_category
+open bicategory
+
+instance (X : C) : monoidal_category (End_monoidal X) :=
+{ tensor_obj := λ f g, f ≫ g,
+  tensor_hom := λ f g h i η θ, (η ▷ h) ≫ (g ◁ θ),
+  tensor_unit := 𝟙 _,
+  associator := λ f g h, α_ f g h,
+  left_unitor := λ f, λ_ f,
+  right_unitor := λ f, ρ_ f,
+  tensor_comp' := begin
+    intros,
+    rw [bicategory.whisker_left_comp, bicategory.comp_whisker_right, category.assoc, category.assoc,
+      bicategory.whisker_exchange_assoc],
+  end }
+
+end category_theory
diff --git a/src/category_theory/bicategory/basic.lean b/src/category_theory/bicategory/basic.lean
index 3ab618c76cae9..ae6620c0000f1 100644
--- a/src/category_theory/bicategory/basic.lean
+++ b/src/category_theory/bicategory/basic.lean
@@ -68,7 +68,7 @@ class bicategory (B : Type u) extends category_struct.{v} B :=
 (associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
   (f ≫ g) ≫ h ≅ f ≫ (g ≫ h))
 (notation `α_` := associator)
---left unitor:
+-- left unitor:
 (left_unitor {a b : B} (f : a ⟶ b) : 𝟙 a ≫ f ≅ f)
 (notation `λ_` := left_unitor)
 -- right unitor:
diff --git a/src/category_theory/bicategory/single_obj.lean b/src/category_theory/bicategory/single_obj.lean
new file mode 100644
index 0000000000000..47022b6ab0912
--- /dev/null
+++ b/src/category_theory/bicategory/single_obj.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.bicategory.End
+import category_theory.monoidal.functorial
+
+/-!
+# 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 = 𝟙 _`.
+-/
+
+namespace category_theory
+
+variables (C : Type*) [category C] [monoidal_category C]
+
+/--
+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.)
+-/
+@[nolint unused_arguments, derive inhabited]
+def monoidal_single_obj (C : Type*) [category C] [monoidal_category C] := punit
+
+open monoidal_category
+
+instance : bicategory (monoidal_single_obj C) :=
+{ hom := λ _ _, C,
+  id := λ _, 𝟙_ C,
+  comp := λ _ _ _ X Y, X ⊗ Y,
+  whisker_left := λ _ _ _ X Y Z f, 𝟙 X ⊗ f,
+  whisker_right := λ _ _ _ X Y f Z, f ⊗ 𝟙 Z,
+  associator := λ _ _ _ _ X Y Z, α_ X Y Z,
+  left_unitor := λ _ _ X, λ_ X,
+  right_unitor := λ _ _ X, ρ_ X,
+  comp_whisker_left' :=
+    by { intros, rw [associator_inv_naturality, iso.hom_inv_id_assoc, tensor_id], },
+  whisker_assoc' := by { intros, rw [associator_inv_naturality, iso.hom_inv_id_assoc], },
+  whisker_right_comp' :=
+    by { intros, rw [←tensor_id, associator_naturality, iso.inv_hom_id_assoc], },
+  id_whisker_left' := by { intros, rw [left_unitor_inv_naturality, iso.hom_inv_id_assoc], },
+  whisker_right_id' := by { intros, rw [right_unitor_inv_naturality, iso.hom_inv_id_assoc], },
+  pentagon' := by { intros, rw [pentagon], }, }
+
+namespace monoidal_single_obj
+
+/-- The unique object in the bicategory obtained by "promoting" a monoidal category. -/
+@[nolint unused_arguments]
+protected def star : monoidal_single_obj C := punit.star
+
+/--
+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.
+-/
+@[simps]
+def End_monoidal_star_functor : monoidal_functor (End_monoidal (monoidal_single_obj.star C)) C :=
+{ obj := λ X, X,
+  map := λ X Y f, f,
+  ε := 𝟙 _,
+  μ := λ X Y, 𝟙 _,
+  μ_natural' := λ X Y X' Y' f g, begin
+    dsimp,
+    simp only [category.id_comp, category.comp_id],
+    -- Should we provide further simp lemmas so this goal becomes visible?
+    exact (tensor_id_comp_id_tensor _ _).symm,
+  end, }
+
+noncomputable theory
+
+/--
+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.
+-/
+def End_monoidal_star_functor_is_equivalence :
+  is_equivalence (End_monoidal_star_functor C).to_functor :=
+{ inverse :=
+  { obj := λ X, X,
+    map := λ X Y f, f, },
+  unit_iso := nat_iso.of_components (λ X, as_iso (𝟙 _)) (by tidy),
+  counit_iso := nat_iso.of_components (λ X, as_iso (𝟙 _)) (by tidy), }
+
+end monoidal_single_obj
+
+end category_theory