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 #

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.

References #

https://ncatlab.org/nlab/show/rigid+monoidal+category

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

@[simp]

theorem category_theory.exact_pairing.coevaluation_evaluation {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) [self : category_theory.exact_pairing X 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₁} [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 {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) [self : category_theory.exact_pairing X 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₁} [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'

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

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

@[protected, instance]

def category_theory.has_right_dual_unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.has_right_dual (𝟙_ C)

Equations

category_theory.has_right_dual_unit = category_theory.has_right_dual.mk (𝟙_ C)

@[protected, instance]

def category_theory.has_left_dual_unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.has_left_dual (𝟙_ C)

Equations

category_theory.has_left_dual_unit = category_theory.has_left_dual.mk (𝟙_ 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] :

category_theory.has_right_dual ᘁX

Equations

category_theory.has_right_dual_left_dual = category_theory.has_right_dual.mk 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] :

category_theory.has_left_dual Xᘁ

Equations

category_theory.has_left_dual_right_dual = category_theory.has_left_dual.mk 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.

Equations

fᘁ = (ρ_ Yᘁ).inv ≫ (𝟙 Yᘁ ⊗ η_ X Xᘁ) ≫ (𝟙 Yᘁ ⊗ (f ⊗ 𝟙 Xᘁ)) ≫ (α_ Yᘁ Y Xᘁ).inv ≫ (ε_ Y Yᘁ ⊗ 𝟙 Xᘁ) ≫ (λ_ Xᘁ).hom

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.

Equations

ᘁf = (λ_ ᘁY).inv ≫ (η_ ᘁX X ⊗ 𝟙 ᘁY) ≫ (𝟙 ᘁX ⊗ f ⊗ 𝟙 ᘁY) ≫ (α_ ᘁX Y ᘁY).hom ≫ (𝟙 ᘁX ⊗ ε_ ᘁY Y) ≫ (ρ_ ᘁX).hom

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

(𝟙 X)ᘁ = 𝟙 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] :

ᘁ(𝟙 X) = 𝟙 ᘁ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} :

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₁} [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} :

ᘁ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₁} [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} :

(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₁} [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') :

(f ≫ g)ᘁ ≫ f' = gᘁ ≫ fᘁ ≫ f'

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} :

ᘁ(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₁} [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') :

ᘁ(f ≫ g) ≫ f' = ᘁg ≫ ᘁf ≫ f'

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

category_theory.right_dual_iso p p = category_theory.iso.refl 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) :

category_theory.left_dual_iso p p = category_theory.iso.refl X

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

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

category_theory.rigid_category.to_left_rigid_category

@[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.