Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(category_theory/bicategory): monoidal categories are single obje…
…ct bicategories (#13157) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
- Loading branch information
1 parent
823699f
commit 6abb6de
Showing
3 changed files
with
146 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |