Documentation

Mathlib.CategoryTheory.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 #

ExactPairing of two objects of a monoidal category
Type classes HasLeftDual and HasRightDual that capture that a pairing exists
The rightAdjointMate f as a morphism fᘁ : Yᘁ ⟶ Xᘁ for a morphism f : X ⟶ Y
The classes of RightRigidCategory, LeftRigidCategory and RigidCategory

Main statements #

comp_rightAdjointMate: 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.
Show that ᘁ gives an equivalence of categories C ≅ (Cᵒᵖ)ᴹᵒᵖ.
Define pivotal categories (rigid categories equipped with a natural isomorphism ᘁᘁ ≅ 𝟙 C).

Notes #

Although we construct the adjunction tensorLeft Y ⊣ tensorLeft X from ExactPairing X Y, this is not a bijective correspondence. I think the correct statement is that tensorLeft Y and tensorLeft X are module endofunctors of C as a right C module category, and ExactPairing X Y is in bijection with adjunctions compatible with this right C action.

References #

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

Tags #

rigid category, monoidal category

class CategoryTheory.ExactPairing {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory 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.

coevaluation' : 𝟙_ C ⟶ MonoidalCategoryStruct.tensorObj X Y
Coevaluation of an exact pairing.
Do not use directly. Use ExactPairing.coevaluation instead.
evaluation' : MonoidalCategoryStruct.tensorObj Y X ⟶ 𝟙_ C
Evaluation of an exact pairing.
Do not use directly. Use ExactPairing.evaluation instead.
coevaluation_evaluation' : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y coevaluation') (CategoryStruct.comp (MonoidalCategoryStruct.associator Y X Y).inv (MonoidalCategoryStruct.whiskerRight evaluation' Y)) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).hom (MonoidalCategoryStruct.leftUnitor Y).inv
evaluation_coevaluation' : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight coevaluation' X) (CategoryStruct.comp (MonoidalCategoryStruct.associator X Y X).hom (MonoidalCategoryStruct.whiskerLeft X evaluation')) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom (MonoidalCategoryStruct.rightUnitor X).inv

Instances

def CategoryTheory.ExactPairing.coevaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] :

𝟙_ C ⟶ MonoidalCategoryStruct.tensorObj X Y

Coevaluation of an exact pairing.

Equations

η_ X Y = CategoryTheory.ExactPairing.coevaluation'

Instances For

def CategoryTheory.ExactPairing.evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] :

MonoidalCategoryStruct.tensorObj Y X ⟶ 𝟙_ C

Evaluation of an exact pairing.

Equations

ε_ X Y = CategoryTheory.ExactPairing.evaluation'

Instances For

def CategoryTheory.ExactPairing.termη_ :

Lean.ParserDescr

Coevaluation of an exact pairing.

Equations

CategoryTheory.ExactPairing.termη_ = Lean.ParserDescr.node `CategoryTheory.ExactPairing.termη_ 1024 (Lean.ParserDescr.symbol "η_")

Instances For

def CategoryTheory.ExactPairing.termε_ :

Lean.ParserDescr

Evaluation of an exact pairing.

Equations

CategoryTheory.ExactPairing.termε_ = Lean.ParserDescr.node `CategoryTheory.ExactPairing.termε_ 1024 (Lean.ParserDescr.symbol "ε_")

Instances For

@[simp]

theorem CategoryTheory.ExactPairing.coevaluation_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y (η_ X Y)) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y X Y).inv (MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y)) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).hom (MonoidalCategoryStruct.leftUnitor Y).inv

@[simp]

theorem CategoryTheory.ExactPairing.evaluation_coevaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η_ X Y) X) (CategoryStruct.comp (MonoidalCategoryStruct.associator X Y X).hom (MonoidalCategoryStruct.whiskerLeft X (ε_ X Y))) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom (MonoidalCategoryStruct.rightUnitor X).inv

theorem CategoryTheory.ExactPairing.coevaluation_evaluation'' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] :

monoidalComp (MonoidalCategoryStruct.whiskerLeft Y (η_ X Y)) (MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y) = MonoidalCoherence.iso.hom

theorem CategoryTheory.ExactPairing.evaluation_coevaluation'' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] :

monoidalComp (MonoidalCategoryStruct.whiskerRight (η_ X Y) X) (MonoidalCategoryStruct.whiskerLeft X (ε_ X Y)) = MonoidalCoherence.iso.hom

@[simp]

theorem CategoryTheory.ExactPairing.coevaluation_evaluation_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] {Z : C} (h : MonoidalCategoryStruct.tensorObj (𝟙_ C) Y ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y (η_ X Y)) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y X Y).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y) h)) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).hom (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv h)

@[simp]

theorem CategoryTheory.ExactPairing.evaluation_coevaluation_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y : C) [ExactPairing X Y] {Z : C} (h : MonoidalCategoryStruct.tensorObj X (𝟙_ C) ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η_ X Y) X) (CategoryStruct.comp (MonoidalCategoryStruct.associator X Y X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (ε_ X Y)) h)) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv h)

instance CategoryTheory.exactPairingUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

ExactPairing (𝟙_ C) (𝟙_ C)

Equations

One or more equations did not get rendered due to their size.

class CategoryTheory.HasRightDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) :

Type (max u₁ v₁)

A class of objects which have a right dual.

rightDual : C
The right dual of the object X.
exact : ExactPairing X Xᘁ

Instances

class CategoryTheory.HasLeftDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (Y : C) :

Type (max u₁ v₁)

A class of objects which have a left dual.

leftDual : C
The left dual of the object X.
exact : ExactPairing (ᘁY) Y

Instances

def CategoryTheory.«termᘁ_» :

Lean.ParserDescr

The left dual of the object X.

Equations

CategoryTheory.«termᘁ_» = Lean.ParserDescr.node `CategoryTheory.«termᘁ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ᘁ") (Lean.ParserDescr.cat `term 1024))

Instances For

def CategoryTheory.«term_ᘁ» :

Lean.TrailingParserDescr

The right dual of the object X.

Equations

CategoryTheory.«term_ᘁ» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_ᘁ» 1024 1024 (Lean.ParserDescr.symbol "ᘁ")

Instances For

instance CategoryTheory.hasRightDualUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

HasRightDual (𝟙_ C)

Equations

CategoryTheory.hasRightDualUnit = CategoryTheory.HasRightDual.mk (𝟙_ C)

instance CategoryTheory.hasLeftDualUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] :

HasLeftDual (𝟙_ C)

Equations

CategoryTheory.hasLeftDualUnit = CategoryTheory.HasLeftDual.mk (𝟙_ C)

instance CategoryTheory.hasRightDualLeftDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [HasLeftDual X] :

HasRightDual ᘁX

Equations

CategoryTheory.hasRightDualLeftDual = CategoryTheory.HasRightDual.mk X

instance CategoryTheory.hasLeftDualRightDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [HasRightDual X] :

HasLeftDual Xᘁ

Equations

CategoryTheory.hasLeftDualRightDual = CategoryTheory.HasLeftDual.mk X

@[simp]

theorem CategoryTheory.leftDual_rightDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [HasRightDual X] :

@[simp]

theorem CategoryTheory.rightDual_leftDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [HasLeftDual X] :

def CategoryTheory.rightAdjointMate {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def CategoryTheory.leftAdjointMate {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def CategoryTheory.«term_ᘁ_1» :

Lean.TrailingParserDescr

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

Equations

CategoryTheory.«term_ᘁ_1» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_ᘁ_1» 1022 0 (Lean.ParserDescr.symbol "ᘁ")

Instances For

def CategoryTheory.«termᘁ__1» :

Lean.ParserDescr

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

Equations

CategoryTheory.«termᘁ__1» = Lean.ParserDescr.node `CategoryTheory.«termᘁ__1» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ᘁ") (Lean.ParserDescr.cat `term 0))

Instances For

@[simp]

theorem CategoryTheory.rightAdjointMate_id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [HasRightDual X] :

CategoryStruct.id Xᘁ = CategoryStruct.id Xᘁ

@[simp]

theorem CategoryTheory.leftAdjointMate_id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [HasLeftDual X] :

(ᘁCategoryStruct.id X) = CategoryStruct.id ᘁX

theorem CategoryTheory.rightAdjointMate_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Z : C} [HasRightDual X] [HasRightDual Y] {f : X ⟶ Y} {g : Xᘁ ⟶ Z} :

theorem CategoryTheory.leftAdjointMate_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Z : C} [HasLeftDual X] [HasLeftDual Y] {f : X ⟶ Y} {g : ᘁX ⟶ Z} :

theorem CategoryTheory.comp_rightAdjointMate {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Z : C} [HasRightDual X] [HasRightDual Y] [HasRightDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} :

CategoryStruct.comp f gᘁ = CategoryStruct.comp (gᘁ) (fᘁ)

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

theorem CategoryTheory.comp_rightAdjointMate_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Z : C} [HasRightDual X] [HasRightDual Y] [HasRightDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} {Z✝ : C} (h : Xᘁ ⟶ Z✝) :

CategoryStruct.comp (CategoryStruct.comp f gᘁ) h = CategoryStruct.comp (gᘁ) (CategoryStruct.comp (fᘁ) h)

theorem CategoryTheory.comp_leftAdjointMate {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Z : C} [HasLeftDual X] [HasLeftDual Y] [HasLeftDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} :

(ᘁCategoryStruct.comp f g) = CategoryStruct.comp (ᘁg) (ᘁf)

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

theorem CategoryTheory.comp_leftAdjointMate_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Z : C} [HasLeftDual X] [HasLeftDual Y] [HasLeftDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} {Z✝ : C} (h : ᘁX ⟶ Z✝) :

CategoryStruct.comp (ᘁCategoryStruct.comp f g) h = CategoryStruct.comp (ᘁg) (CategoryStruct.comp (ᘁf) h)

def CategoryTheory.tensorLeftHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Y' Z : C) [ExactPairing Y Y'] :

(MonoidalCategoryStruct.tensorObj Y' X ⟶ Z) ≃ (X ⟶ MonoidalCategoryStruct.tensorObj Y Z)

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 tensorLeftAdjunction Y Y' : tensorLeft Y' ⊣ tensorLeft Y.

This adjunction is often referred to as "Frobenius reciprocity" in the fusion categories / planar algebras / subfactors literature.

Equations

One or more equations did not get rendered due to their size.

Instances For

def CategoryTheory.tensorRightHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X Y Y' Z : C) [ExactPairing Y Y'] :

(MonoidalCategoryStruct.tensorObj X Y ⟶ Z) ≃ (X ⟶ MonoidalCategoryStruct.tensorObj Z Y')

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

One or more equations did not get rendered due to their size.

Instances For

theorem CategoryTheory.tensorLeftHomEquiv_naturality {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Y' Z Z' : C} [ExactPairing Y Y'] (f : MonoidalCategoryStruct.tensorObj Y' X ⟶ Z) (g : Z ⟶ Z') :

(tensorLeftHomEquiv X Y Y' Z') (CategoryStruct.comp f g) = CategoryStruct.comp ((tensorLeftHomEquiv X Y Y' Z) f) (MonoidalCategoryStruct.whiskerLeft Y g)

theorem CategoryTheory.tensorLeftHomEquiv_symm_naturality {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X X' Y Y' Z : C} [ExactPairing Y Y'] (f : X ⟶ X') (g : X' ⟶ MonoidalCategoryStruct.tensorObj Y Z) :

(tensorLeftHomEquiv X Y Y' Z).symm (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y' f) ((tensorLeftHomEquiv X' Y Y' Z).symm g)

theorem CategoryTheory.tensorRightHomEquiv_naturality {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Y' Z Z' : C} [ExactPairing Y Y'] (f : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) (g : Z ⟶ Z') :

(tensorRightHomEquiv X Y Y' Z') (CategoryStruct.comp f g) = CategoryStruct.comp ((tensorRightHomEquiv X Y Y' Z) f) (MonoidalCategoryStruct.whiskerRight g Y')

theorem CategoryTheory.tensorRightHomEquiv_symm_naturality {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X X' Y Y' Z : C} [ExactPairing Y Y'] (f : X ⟶ X') (g : X' ⟶ MonoidalCategoryStruct.tensorObj Z Y') :

(tensorRightHomEquiv X Y Y' Z).symm (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) ((tensorRightHomEquiv X' Y Y' Z).symm g)

def CategoryTheory.tensorLeftAdjunction {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (Y Y' : C) [ExactPairing Y Y'] :

MonoidalCategory.tensorLeft Y' ⊣ MonoidalCategory.tensorLeft Y

If Y Y' have an exact pairing, then the functor tensorLeft Y' is left adjoint to tensorLeft Y.

Equations

One or more equations did not get rendered due to their size.

Instances For

def CategoryTheory.tensorRightAdjunction {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (Y Y' : C) [ExactPairing Y Y'] :

MonoidalCategory.tensorRight Y ⊣ MonoidalCategory.tensorRight Y'

If Y Y' have an exact pairing, then the functor tensor_right Y is left adjoint to tensor_right Y'.

Equations

One or more equations did not get rendered due to their size.

Instances For

def CategoryTheory.closedOfHasLeftDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (Y : C) [HasLeftDual Y] :

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 CategoryTheory.Monoidal.functorHasLeftDual. 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

CategoryTheory.closedOfHasLeftDual Y = { rightAdj := CategoryTheory.MonoidalCategory.tensorLeft ᘁY, adj := CategoryTheory.tensorLeftAdjunction (ᘁY) Y }

Instances For

theorem CategoryTheory.tensorLeftHomEquiv_tensor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⟶ MonoidalCategoryStruct.tensorObj Y Z) (g : X' ⟶ Z') :

(tensorLeftHomEquiv (MonoidalCategoryStruct.tensorObj X X') Y Y' (MonoidalCategoryStruct.tensorObj Z Z')).symm (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (MonoidalCategoryStruct.associator Y Z Z').hom) = CategoryStruct.comp (MonoidalCategoryStruct.associator Y' X X').inv (MonoidalCategoryStruct.tensorHom ((tensorLeftHomEquiv X Y Y' Z).symm f) g)

tensorLeftHomEquiv commutes with tensoring on the right

theorem CategoryTheory.tensorRightHomEquiv_tensor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X X' Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⟶ MonoidalCategoryStruct.tensorObj Z Y') (g : X' ⟶ Z') :

(tensorRightHomEquiv (MonoidalCategoryStruct.tensorObj X' X) Y Y' (MonoidalCategoryStruct.tensorObj Z' Z)).symm (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g f) (MonoidalCategoryStruct.associator Z' Z Y').inv) = CategoryStruct.comp (MonoidalCategoryStruct.associator X' X Y).hom (MonoidalCategoryStruct.tensorHom g ((tensorRightHomEquiv X Y Y' Z).symm f))

tensorRightHomEquiv commutes with tensoring on the left

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {Y Y' Z : C} [ExactPairing Y Y'] (f : Y' ⟶ Z) :

(tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (CategoryStruct.comp (η_ Y Y') (MonoidalCategoryStruct.whiskerLeft Y f)) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y').hom f

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :

(tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (CategoryStruct.comp (η_ X Xᘁ) (MonoidalCategoryStruct.whiskerRight f Xᘁ)) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Yᘁ).hom (fᘁ)

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :

(tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (CategoryStruct.comp (η_ (ᘁX) X) (MonoidalCategoryStruct.whiskerLeft (ᘁX) f)) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor ᘁY).hom (ᘁf)

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {Y Y' Z : C} [ExactPairing Y Y'] (f : Y ⟶ Z) :

(tensorRightHomEquiv (𝟙_ C) Y Y' Z).symm (CategoryStruct.comp (η_ Y Y') (MonoidalCategoryStruct.whiskerRight f Y')) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).hom f

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {Y Z : C} [HasLeftDual Z] (f : Y ⟶ ᘁZ) :

(tensorLeftHomEquiv Y (ᘁZ) Z (𝟙_ C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Z f) (ε_ (ᘁZ) Z)) = CategoryStruct.comp f (MonoidalCategoryStruct.rightUnitor ᘁZ).inv

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :

(tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f ᘁY) (ε_ (ᘁY) Y)) = CategoryStruct.comp (ᘁf) (MonoidalCategoryStruct.rightUnitor ᘁX).inv

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :

(tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Yᘁ f) (ε_ Y Yᘁ)) = CategoryStruct.comp (fᘁ) (MonoidalCategoryStruct.leftUnitor Xᘁ).inv

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] (f : Y ⟶ Xᘁ) :

(tensorRightHomEquiv Y X Xᘁ (𝟙_ C)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f X) (ε_ X Xᘁ)) = CategoryStruct.comp f (MonoidalCategoryStruct.leftUnitor Xᘁ).inv

theorem CategoryTheory.coevaluation_comp_rightAdjointMate {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :

CategoryStruct.comp (η_ Y Yᘁ) (MonoidalCategoryStruct.whiskerLeft Y (fᘁ)) = CategoryStruct.comp (η_ X Xᘁ) (MonoidalCategoryStruct.whiskerRight f Xᘁ)

theorem CategoryTheory.coevaluation_comp_rightAdjointMate_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj Y Xᘁ ⟶ Z) :

CategoryStruct.comp (η_ Y Yᘁ) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y (fᘁ)) h) = CategoryStruct.comp (η_ X Xᘁ) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Xᘁ) h)

theorem CategoryTheory.leftAdjointMate_comp_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (ᘁf)) (ε_ (ᘁX) X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f ᘁY) (ε_ (ᘁY) Y)

theorem CategoryTheory.leftAdjointMate_comp_evaluation_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) {Z : C} (h : 𝟙_ C ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (ᘁf)) (CategoryStruct.comp (ε_ (ᘁX) X) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f ᘁY) (CategoryStruct.comp (ε_ (ᘁY) Y) h)

theorem CategoryTheory.coevaluation_comp_leftAdjointMate {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) :

CategoryStruct.comp (η_ (ᘁY) Y) (MonoidalCategoryStruct.whiskerRight (ᘁf) Y) = CategoryStruct.comp (η_ (ᘁX) X) (MonoidalCategoryStruct.whiskerLeft (ᘁX) f)

theorem CategoryTheory.coevaluation_comp_leftAdjointMate_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasLeftDual X] [HasLeftDual Y] (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj (ᘁX) Y ⟶ Z) :

CategoryStruct.comp (η_ (ᘁY) Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ᘁf) Y) h) = CategoryStruct.comp (η_ (ᘁX) X) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (ᘁX) f) h)

theorem CategoryTheory.rightAdjointMate_comp_evaluation {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (fᘁ) X) (ε_ X Xᘁ) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Yᘁ f) (ε_ Y Yᘁ)

theorem CategoryTheory.rightAdjointMate_comp_evaluation_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} [HasRightDual X] [HasRightDual Y] (f : X ⟶ Y) {Z : C} (h : 𝟙_ C ⟶ Z) :

CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (fᘁ) X) (CategoryStruct.comp (ε_ X Xᘁ) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Yᘁ f) (CategoryStruct.comp (ε_ Y Yᘁ) h)

def CategoryTheory.exactPairingCongrLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X X' Y : C} [ExactPairing X' Y] (i : X ≅ X') :

ExactPairing X Y

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def CategoryTheory.exactPairingCongrRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y Y' : C} [ExactPairing X Y'] (i : Y ≅ Y') :

ExactPairing X Y

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

Equations

One or more equations did not get rendered due to their size.

Instances For

def CategoryTheory.exactPairingCongr {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X X' Y Y' : C} [ExactPairing X' Y'] (i : X ≅ X') (j : Y ≅ Y') :

ExactPairing X Y

Transport an exact pairing across isomorphisms.

Equations

CategoryTheory.exactPairingCongr i j = CategoryTheory.exactPairingCongrLeft i

Instances For

def CategoryTheory.rightDualIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) :

Y₁ ≅ Y₂

Right duals are isomorphic.

Equations

CategoryTheory.rightDualIso p₁ p₂ = { hom := CategoryTheory.CategoryStruct.id Xᘁ, inv := CategoryTheory.CategoryStruct.id Xᘁ, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

def CategoryTheory.leftDualIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y : C} (p₁ : ExactPairing X₁ Y) (p₂ : ExactPairing X₂ Y) :

X₁ ≅ X₂

Left duals are isomorphic.

Equations

CategoryTheory.leftDualIso p₁ p₂ = { hom := ᘁCategoryTheory.CategoryStruct.id Y, inv := ᘁCategoryTheory.CategoryStruct.id Y, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.rightDualIso_id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} (p : ExactPairing X Y) :

rightDualIso p p = Iso.refl Y

@[simp]

theorem CategoryTheory.leftDualIso_id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X Y : C} (p : ExactPairing X Y) :

leftDualIso p p = Iso.refl X

class CategoryTheory.RightRigidCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :

Type (max u v)

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

rightDual (X : C) : HasRightDual X

Instances

class CategoryTheory.LeftRigidCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] :

Type (max u v)

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

leftDual (X : C) : HasLeftDual X

Instances

def CategoryTheory.monoidalClosedOfLeftRigidCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [LeftRigidCategory C] :

MonoidalClosed C

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 CategoryTheory.Monoidal.leftRigidFunctorCategory. 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

CategoryTheory.monoidalClosedOfLeftRigidCategory C = { closed := fun (X : C) => CategoryTheory.closedOfHasLeftDual X }

Instances For

class CategoryTheory.RigidCategory (C : Type u) [Category.{v, u} C] [MonoidalCategory C] extends CategoryTheory.RightRigidCategory C, CategoryTheory.LeftRigidCategory C :

Type (max u v)

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

rightDual (X : C) : HasRightDual X
leftDual (X : C) : HasLeftDual X

Instances