Rigid (autonomous) monoidal categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines rigid (autonomous) monoidal categories and the necessary theory about exact pairings and duals.
Main definitions #
exact_pairingof two objects of a monoidal category- Type classes
has_left_dualandhas_right_dualthat capture that a pairing exists - The
right_adjoint_mate fas a morphismfᘁ : Yᘁ ⟶ Xᘁfor a morphismf : X ⟶ Y - The classes of
right_rigid_category,left_rigid_categoryandrigid_category
Main statements #
comp_right_adjoint_mate: The adjoint mates of the composition is the composition of adjoint mates.
Notations #
η_andε_denote the coevaluation and evaluation morphism of an exact pairing.XᘁandᘁXdenote the right and left dual of an object, as well as the adjoint mate of a morphism.
Future work #
- Show that
X ⊗ YandYᘁ ⊗ Xᘁform an exact pairing. - Show that the left adjoint mate of the right adjoint mate of a morphism is the morphism itself.
- Simplify constructions in the case where a symmetry or braiding is present.
- Show that
ᘁgives an equivalence of categoriesC ≅ (Cᵒᵖ)ᴹᵒᵖ. - Define pivotal categories (rigid categories equipped with a natural isomorphism
ᘁᘁ ≅ 𝟙 C).
Notes #
Although we construct the adjunction tensor_left Y ⊣ tensor_left X from exact_pairing X Y,
this is not a bijective correspondence.
I think the correct statement is that tensor_left Y and tensor_left X are
module endofunctors of C as a right C module category,
and exact_pairing X Y is in bijection with adjunctions compatible with this right C action.
References #
Tags #
rigid category, monoidal category
@[class]
structure
category_theory.exact_pairing
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
Type v₁
- coevaluation : 𝟙_ C ⟶ X ⊗ Y
- evaluation : Y ⊗ X ⟶ 𝟙_ C
- coevaluation_evaluation' : (𝟙 Y ⊗ η_ X Y) ≫ (α_ Y X Y).inv ≫ (ε_ X Y ⊗ 𝟙 Y) = (ρ_ Y).hom ≫ (λ_ Y).inv . "obviously"
- evaluation_coevaluation' : (η_ X Y ⊗ 𝟙 X) ≫ (α_ X Y X).hom ≫ (𝟙 X ⊗ ε_ X Y) = (λ_ X).hom ≫ (ρ_ X).inv . "obviously"
An exact pairing is a pair of objects X Y : C which admit
a coevaluation and evaluation morphism which fulfill two triangle equalities.
Instances of this typeclass
Instances of other typeclasses for category_theory.exact_pairing
- category_theory.exact_pairing.has_sizeof_inst
@[simp]
theorem
category_theory.exact_pairing.coevaluation_evaluation_assoc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C)
[self : category_theory.exact_pairing X Y]
{X' : C}
(f' : 𝟙_ C ⊗ Y ⟶ X') :
@[simp]
theorem
category_theory.exact_pairing.evaluation_coevaluation_assoc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C)
[self : category_theory.exact_pairing X Y]
{X' : C}
(f' : X ⊗ 𝟙_ C ⟶ X') :
@[protected, instance]
def
category_theory.exact_pairing_unit
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C] :
category_theory.exact_pairing (𝟙_ C) (𝟙_ C)
Equations
- category_theory.exact_pairing_unit = {coevaluation := (ρ_ (𝟙_ C)).inv, evaluation := (ρ_ (𝟙_ C)).hom, coevaluation_evaluation' := _, evaluation_coevaluation' := _}
@[class]
structure
category_theory.has_right_dual
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C) :
Type (max u₁ v₁)
- right_dual : C
- exact : category_theory.exact_pairing X Xᘁ
A class of objects which have a right dual.
Instances of this typeclass
Instances of other typeclasses for category_theory.has_right_dual
- category_theory.has_right_dual.has_sizeof_inst
@[class]
structure
category_theory.has_left_dual
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(Y : C) :
Type (max u₁ v₁)
- left_dual : C
- exact : category_theory.exact_pairing ᘁY Y
A class of objects with have a left dual.
Instances of this typeclass
Instances of other typeclasses for category_theory.has_left_dual
- category_theory.has_left_dual.has_sizeof_inst
@[protected, instance]
def
category_theory.has_right_dual_unit
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C] :
@[protected, instance]
def
category_theory.has_left_dual_unit
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C] :
@[protected, instance]
def
category_theory.has_right_dual_left_dual
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X : C}
[category_theory.has_left_dual X] :
@[protected, instance]
def
category_theory.has_left_dual_right_dual
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X : C}
[category_theory.has_right_dual X] :
@[simp]
theorem
category_theory.left_dual_right_dual
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X : C}
[category_theory.has_right_dual X] :
@[simp]
theorem
category_theory.right_dual_left_dual
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X : C}
[category_theory.has_left_dual X] :
def
category_theory.right_adjoint_mate
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
(f : X ⟶ Y) :
The right adjoint mate fᘁ : Xᘁ ⟶ Yᘁ of a morphism f : X ⟶ Y.
def
category_theory.left_adjoint_mate
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
(f : X ⟶ Y) :
The left adjoint mate ᘁf : ᘁY ⟶ ᘁX of a morphism f : X ⟶ Y.
@[simp]
theorem
category_theory.right_adjoint_mate_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X : C}
[category_theory.has_right_dual X] :
@[simp]
theorem
category_theory.left_adjoint_mate_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X : C}
[category_theory.has_left_dual X] :
theorem
category_theory.right_adjoint_mate_comp
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Z : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
{f : X ⟶ Y}
{g : Xᘁ ⟶ Z} :
theorem
category_theory.left_adjoint_mate_comp
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Z : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
{f : X ⟶ Y}
{g : ᘁX ⟶ Z} :
theorem
category_theory.comp_right_adjoint_mate
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Z : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
[category_theory.has_right_dual Z]
{f : X ⟶ Y}
{g : Y ⟶ Z} :
The composition of right adjoint mates is the adjoint mate of the composition.
theorem
category_theory.comp_right_adjoint_mate_assoc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Z : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
[category_theory.has_right_dual Z]
{f : X ⟶ Y}
{g : Y ⟶ Z}
{X' : C}
(f' : Xᘁ ⟶ X') :
theorem
category_theory.comp_left_adjoint_mate
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Z : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
[category_theory.has_left_dual Z]
{f : X ⟶ Y}
{g : Y ⟶ Z} :
The composition of left adjoint mates is the adjoint mate of the composition.
theorem
category_theory.comp_left_adjoint_mate_assoc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Z : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
[category_theory.has_left_dual Z]
{f : X ⟶ Y}
{g : Y ⟶ Z}
{X' : C}
(f' : ᘁX ⟶ X') :
def
category_theory.tensor_left_hom_equiv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Y' Z : C)
[category_theory.exact_pairing Y Y'] :
Given an exact pairing on Y Y',
we get a bijection on hom-sets (Y' ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z)
by "pulling the string on the left" up or down.
This gives the adjunction tensor_left_adjunction Y Y' : tensor_left Y' ⊣ tensor_left Y.
This adjunction is often referred to as "Frobenius reciprocity" in the fusion categories / planar algebras / subfactors literature.
def
category_theory.tensor_right_hom_equiv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Y' Z : C)
[category_theory.exact_pairing Y Y'] :
Given an exact pairing on Y Y',
we get a bijection on hom-sets (X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y')
by "pulling the string on the right" up or down.
theorem
category_theory.tensor_left_hom_equiv_naturality
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Y' Z Z' : C}
[category_theory.exact_pairing Y Y']
(f : Y' ⊗ X ⟶ Z)
(g : Z ⟶ Z') :
⇑(category_theory.tensor_left_hom_equiv X Y Y' Z') (f ≫ g) = ⇑(category_theory.tensor_left_hom_equiv X Y Y' Z) f ≫ (𝟙 Y ⊗ g)
theorem
category_theory.tensor_left_hom_equiv_symm_naturality
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' Y Y' Z : C}
[category_theory.exact_pairing Y Y']
(f : X ⟶ X')
(g : X' ⟶ Y ⊗ Z) :
theorem
category_theory.tensor_right_hom_equiv_naturality
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Y' Z Z' : C}
[category_theory.exact_pairing Y Y']
(f : X ⊗ Y ⟶ Z)
(g : Z ⟶ Z') :
⇑(category_theory.tensor_right_hom_equiv X Y Y' Z') (f ≫ g) = ⇑(category_theory.tensor_right_hom_equiv X Y Y' Z) f ≫ (g ⊗ 𝟙 Y')
theorem
category_theory.tensor_right_hom_equiv_symm_naturality
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' Y Y' Z : C}
[category_theory.exact_pairing Y Y']
(f : X ⟶ X')
(g : X' ⟶ Z ⊗ Y') :
def
category_theory.tensor_left_adjunction
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(Y Y' : C)
[category_theory.exact_pairing Y Y'] :
If Y Y' have an exact pairing,
then the functor tensor_left Y' is left adjoint to tensor_left Y.
Equations
- category_theory.tensor_left_adjunction Y Y' = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X Z : C), category_theory.tensor_left_hom_equiv X Y Y' Z, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
def
category_theory.tensor_right_adjunction
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(Y Y' : C)
[category_theory.exact_pairing Y Y'] :
If Y Y' have an exact pairing,
then the functor tensor_right Y is left adjoint to tensor_right Y'.
Equations
- category_theory.tensor_right_adjunction Y Y' = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X Z : C), category_theory.tensor_right_hom_equiv X Y Y' Z, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
def
category_theory.closed_of_has_left_dual
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(Y : C)
[category_theory.has_left_dual Y] :
If Y has a left dual ᘁY, then it is a closed object, with the internal hom functor Y ⟶[C] -
given by left tensoring by ᘁY.
This has to be a definition rather than an instance to avoid diamonds, for example between
category_theory.monoidal_closed.functor_closed and
category_theory.monoidal.functor_has_left_dual. Moreover, in concrete applications there is often
a more useful definition of the internal hom object than ᘁY ⊗ X, in which case the closed
structure shouldn't come from has_left_dual (e.g. in the category FinVect k, it is more
convenient to define the internal hom as Y →ₗ[k] X rather than ᘁY ⊗ X even though these are
naturally isomorphic).
theorem
category_theory.tensor_left_hom_equiv_tensor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' Y Y' Z Z' : C}
[category_theory.exact_pairing Y Y']
(f : X ⟶ Y ⊗ Z)
(g : X' ⟶ Z') :
tensor_left_hom_equiv commutes with tensoring on the right
theorem
category_theory.tensor_right_hom_equiv_tensor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' Y Y' Z Z' : C}
[category_theory.exact_pairing Y Y']
(f : X ⟶ Z ⊗ Y')
(g : X' ⟶ Z') :
tensor_right_hom_equiv commutes with tensoring on the left
@[simp]
theorem
category_theory.tensor_left_hom_equiv_symm_coevaluation_comp_id_tensor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{Y Y' Z : C}
[category_theory.exact_pairing Y Y']
(f : Y' ⟶ Z) :
@[simp]
theorem
category_theory.tensor_left_hom_equiv_symm_coevaluation_comp_tensor_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.tensor_right_hom_equiv_symm_coevaluation_comp_id_tensor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.tensor_right_hom_equiv_symm_coevaluation_comp_tensor_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{Y Y' Z : C}
[category_theory.exact_pairing Y Y']
(f : Y ⟶ Z) :
@[simp]
theorem
category_theory.tensor_left_hom_equiv_id_tensor_comp_evaluation
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{Y Z : C}
[category_theory.has_left_dual Z]
(f : Y ⟶ ᘁZ) :
@[simp]
theorem
category_theory.tensor_left_hom_equiv_tensor_id_comp_evaluation
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.tensor_right_hom_equiv_id_tensor_comp_evaluation
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.tensor_right_hom_equiv_tensor_id_comp_evaluation
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_right_dual X]
(f : Y ⟶ Xᘁ) :
theorem
category_theory.coevaluation_comp_right_adjoint_mate
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
(f : X ⟶ Y) :
theorem
category_theory.left_adjoint_mate_comp_evaluation
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
(f : X ⟶ Y) :
theorem
category_theory.coevaluation_comp_left_adjoint_mate
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_left_dual X]
[category_theory.has_left_dual Y]
(f : X ⟶ Y) :
theorem
category_theory.right_adjoint_mate_comp_evaluation
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
[category_theory.has_right_dual X]
[category_theory.has_right_dual Y]
(f : X ⟶ Y) :
def
category_theory.exact_pairing_congr_left
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' Y : C}
[category_theory.exact_pairing X' Y]
(i : X ≅ X') :
Transport an exact pairing across an isomorphism in the first argument.
Equations
- category_theory.exact_pairing_congr_left i = {coevaluation := η_ X' Y ≫ (i.inv ⊗ 𝟙 Y), evaluation := (𝟙 Y ⊗ i.hom) ≫ ε_ X' Y, coevaluation_evaluation' := _, evaluation_coevaluation' := _}
def
category_theory.exact_pairing_congr_right
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y Y' : C}
[category_theory.exact_pairing X Y']
(i : Y ≅ Y') :
Transport an exact pairing across an isomorphism in the second argument.
Equations
- category_theory.exact_pairing_congr_right i = {coevaluation := η_ X Y' ≫ (𝟙 X ⊗ i.inv), evaluation := (i.hom ⊗ 𝟙 X) ≫ ε_ X Y', coevaluation_evaluation' := _, evaluation_coevaluation' := _}
def
category_theory.exact_pairing_congr
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' Y Y' : C}
[category_theory.exact_pairing X' Y']
(i : X ≅ X')
(j : Y ≅ Y') :
Transport an exact pairing across isomorphisms.
def
category_theory.right_dual_iso
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y₁ Y₂ : C}
(_x : category_theory.exact_pairing X Y₁)
(_x_1 : category_theory.exact_pairing X Y₂) :
Y₁ ≅ Y₂
Right duals are isomorphic.
Equations
- category_theory.right_dual_iso _x _x_1 = {hom := (𝟙 X)ᘁ, inv := (𝟙 X)ᘁ, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.left_dual_iso
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X₁ X₂ Y : C}
(p₁ : category_theory.exact_pairing X₁ Y)
(p₂ : category_theory.exact_pairing X₂ Y) :
X₁ ≅ X₂
Left duals are isomorphic.
Equations
- category_theory.left_dual_iso p₁ p₂ = {hom := ᘁ(𝟙 Y), inv := ᘁ(𝟙 Y), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.right_dual_iso_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
(p : category_theory.exact_pairing X Y) :
@[simp]
theorem
category_theory.left_dual_iso_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
(p : category_theory.exact_pairing X Y) :
@[class]
structure
category_theory.right_rigid_category
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Type (max u v)
- right_dual : Π (X : C), category_theory.has_right_dual X
A right rigid monoidal category is one in which every object has a right dual.
Instances of this typeclass
Instances of other typeclasses for category_theory.right_rigid_category
- category_theory.right_rigid_category.has_sizeof_inst
@[class]
structure
category_theory.left_rigid_category
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Type (max u v)
- left_dual : Π (X : C), category_theory.has_left_dual X
A left rigid monoidal category is one in which every object has a right dual.
Instances of this typeclass
Instances of other typeclasses for category_theory.left_rigid_category
- category_theory.left_rigid_category.has_sizeof_inst
def
category_theory.monoidal_closed_of_left_rigid_category
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.left_rigid_category C] :
Any left rigid category is monoidal closed, with the internal hom X ⟶[C] Y = ᘁX ⊗ Y.
This has to be a definition rather than an instance to avoid diamonds, for example between
category_theory.monoidal_closed.functor_category and
category_theory.monoidal.left_rigid_functor_category. Moreover, in concrete applications there is
often a more useful definition of the internal hom object than ᘁY ⊗ X, in which case the monoidal
closed structure shouldn't come the rigid structure (e.g. in the category FinVect k, it is more
convenient to define the internal hom as Y →ₗ[k] X rather than ᘁY ⊗ X even though these are
naturally isomorphic).
Equations
@[class]
structure
category_theory.rigid_category
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Type (max u v)
- to_right_rigid_category : category_theory.right_rigid_category C
- to_left_rigid_category : category_theory.left_rigid_category C
A rigid monoidal category is a monoidal category which is left rigid and right rigid.
Instances of this typeclass
Instances of other typeclasses for category_theory.rigid_category
- category_theory.rigid_category.has_sizeof_inst