mathlib documentation

category_theory.monoidal.rigid

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 #

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
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'
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_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

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.

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

A left rigid monoidal category is one in which every object has a right dual.

Instances
@[class]

A rigid monoidal category is a monoidal category which is left rigid and right rigid.