mathlib documentation

category_theory.monoidal.rigid.basic

Rigid (autonomous) monoidal categories #

This file defines rigid (autonomous) monoidal categories and the necessary theory about exact pairings and duals.

Main definitions #

Main statements #

Notations #

Future work #

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₁

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') :
(𝟙 Y η_ X Y) (α_ Y X Y).inv (ε_ X Y 𝟙 Y) f' = (ρ_ Y).hom (λ_ Y).inv f'
@[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') :
(η_ X Y 𝟙 X) (α_ X Y X).hom (𝟙 X ε_ X Y) f' = (λ_ X).hom (ρ_ X).inv f'
@[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₁)

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₁)

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

The right adjoint mate fᘁ : Xᘁ ⟶ Yᘁ of a morphism f : X ⟶ Y.

Equations

The left adjoint mate ᘁf : ᘁY ⟶ ᘁX of a morphism f : X ⟶ Y.

Equations

The composition of right adjoint mates is the adjoint mate of the composition.

The composition of left adjoint mates is the adjoint mate of the composition.

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.

Equations

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.

Equations
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') :
((category_theory.tensor_left_hom_equiv (X X') Y Y' (Z Z')).symm) ((f g) (α_ Y Z Z').hom) = (α_ Y' X X').inv (((category_theory.tensor_left_hom_equiv X Y Y' Z).symm) f g)

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') :
((category_theory.tensor_right_hom_equiv (X' X) Y Y' (Z' Z)).symm) ((g f) (α_ Z' Z Y').inv) = (α_ X' X Y).hom (g ((category_theory.tensor_right_hom_equiv X Y Y' Z).symm) f)

tensor_right_hom_equiv commutes with tensoring on the left

Transport an exact pairing across an isomorphism in the first argument.

Equations

Transport an exact pairing across an isomorphism in the second argument.

Equations

Right duals are isomorphic.

Equations
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
@[class]

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]

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
@[class]

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