mathlib3 documentation

category_theory.monoidal.rigid.basic

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 #

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]

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

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]

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

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

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

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

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

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]

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