# mathlibdocumentation

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 #

• exact_pairing of two objects of a monoidal category
• Type classes has_left_dual and has_right_dual that capture that a pairing exists
• The right_adjoint_mate f as a morphism fᘁ : Yᘁ ⟶ Xᘁ for a morphism f : X ⟶ Y
• The classes of right_rigid_category, left_rigid_category and rigid_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 ᘁX denote the right and left dual of an object, as well as the adjoint mate of a morphism.

## Future work #

• Show that X ⊗ Y and Yᘁ ⊗ 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.

## Tags #

rigid category, monoidal category

@[class]
structure category_theory.exact_pairing {C : Type u₁} (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
@[simp]
theorem category_theory.exact_pairing.coevaluation_evaluation {C : Type u₁} (X Y : C) [self : Y] :
(𝟙 Y η_ X Y) (α_ Y X Y).inv (ε_ X Y 𝟙 Y) = (ρ_ Y).hom (λ_ Y).inv
theorem category_theory.exact_pairing.coevaluation_evaluation_assoc {C : Type u₁} (X Y : C) [self : 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 {C : Type u₁} (X Y : C) [self : Y] :
(η_ X Y 𝟙 X) (α_ X Y X).hom (𝟙 X ε_ X Y) = (λ_ X).hom (ρ_ X).inv
theorem category_theory.exact_pairing.evaluation_coevaluation_assoc {C : Type u₁} (X Y : C) [self : 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₁} (X : C) :
Type (max u₁ v₁)
• right_dual : C
• exact :

A class of objects which have a right dual.

Instances
@[class]
structure category_theory.has_left_dual {C : Type u₁} (Y : C) :
Type (max u₁ v₁)
• left_dual : C
• exact :

A class of objects with have a left dual.

Instances
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.left_dual_right_dual {C : Type u₁} {X : C}  :
(X) = X
@[simp]
theorem category_theory.right_dual_left_dual {C : Type u₁} {X : C}  :
def category_theory.right_adjoint_mate {C : Type u₁} {X Y : C} (f : X Y) :

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

Equations
def category_theory.left_adjoint_mate {C : Type u₁} {X Y : C} (f : X Y) :

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

Equations
@[simp]
theorem category_theory.right_adjoint_mate_id {C : Type u₁} {X : C}  :
@[simp]
theorem category_theory.left_adjoint_mate_id {C : Type u₁} {X : C}  :
theorem category_theory.right_adjoint_mate_comp {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z} :
f g = (ρ_ Y).inv (𝟙 Y η_ X X) (𝟙 Y (f g)) (α_ Y Y Z).inv (ε_ Y Y 𝟙 Z) (λ_ Z).hom
theorem category_theory.left_adjoint_mate_comp {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z} :
f g = (λ_ Y).inv (η_ X X 𝟙 Y) (g f 𝟙 Y) (α_ Z Y Y).hom (𝟙 Z ε_ Y Y) (ρ_ Z).hom
theorem category_theory.comp_right_adjoint_mate {C : Type u₁} {X Y Z : C} {f : X Y} {g : Y Z} :
(f g) = g f

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

theorem category_theory.comp_right_adjoint_mate_assoc {C : Type u₁} {X Y Z : C} {f : X Y} {g : Y Z} {X' : C} (f' : X X') :
(f g) f' = g f f'
theorem category_theory.comp_left_adjoint_mate {C : Type u₁} {X Y Z : C} {f : X Y} {g : Y Z} :
(f g) = g f

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

theorem category_theory.comp_left_adjoint_mate_assoc {C : Type u₁} {X Y Z : C} {f : X Y} {g : Y Z} {X' : C} (f' : X X') :
(f g) f' = g f f'
def category_theory.right_dual_iso {C : Type u₁} {X Y₁ Y₂ : C} (_x : Y₁) (_x_1 : Y₂) :
Y₁ Y₂

Right duals are isomorphic.

Equations
def category_theory.left_dual_iso {C : Type u₁} {X₁ X₂ Y : C} (p₁ : Y) (p₂ : Y) :
X₁ X₂

Left duals are isomorphic.

Equations
@[simp]
theorem category_theory.right_dual_iso_id {C : Type u₁} {X Y : C} (p : Y) :
@[simp]
theorem category_theory.left_dual_iso_id {C : Type u₁} {X Y : C} (p : Y) :
@[class]
structure category_theory.right_rigid_category (C : Type u)  :
Type (max u v)
• right_dual : Π (X : C),

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

Instances
@[class]
structure category_theory.left_rigid_category (C : Type u)  :
Type (max u v)
• left_dual : Π (X : C),

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

Instances
@[class]
structure category_theory.rigid_category (C : Type u)  :
Type (max u v)
• to_right_rigid_category :
• to_left_rigid_category :

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