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' : MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj X Y

  Coevaluation of an exact pairing.

  Do not use directly. Use ExactPairing.coevaluation instead.

• evaluation' : MonoidalCategoryStruct.tensorObj Y X ⟶ MonoidalCategoryStruct.tensorUnit 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

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

Coevaluation of an exact pairing.

Equations

• η_ X Y = CategoryTheory.ExactPairing.coevaluation'

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

Evaluation of an exact pairing.

Equations

• ε_ X Y = CategoryTheory.ExactPairing.evaluation'

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 "η_")

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 "ε_")

@[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 (MonoidalCategoryStruct.tensorUnit 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 (MonoidalCategoryStruct.tensorUnit 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 (MonoidalCategoryStruct.tensorUnit C) (MonoidalCategoryStruct.tensorUnit 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ᘁ

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

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

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 "ᘁ")

instance CategoryTheory.hasRightDualUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : HasRightDual (MonoidalCategoryStruct.tensorUnit C)

Equations

• CategoryTheory.hasRightDualUnit = { rightDual := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, exact := CategoryTheory.exactPairingUnit }

instance CategoryTheory.hasLeftDualUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : HasLeftDual (MonoidalCategoryStruct.tensorUnit C)

Equations

• CategoryTheory.hasLeftDualUnit = { leftDual := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, exact := CategoryTheory.exactPairingUnit }

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

Equations

• CategoryTheory.hasRightDualLeftDual = { rightDual := X, exact := CategoryTheory.HasLeftDual.exact }

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

Equations

• CategoryTheory.hasLeftDualRightDual = { leftDual := X, exact := CategoryTheory.HasRightDual.exact }

@[simp]

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

@[simp]

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

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

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.

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

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.

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 "ᘁ")

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

@[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} : CategoryStruct.comp (fᘁ) g = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Yᘁ).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Yᘁ (η_ X Xᘁ)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Yᘁ (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (MonoidalCategoryStruct.associator Yᘁ Y Z).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (ε_ Y Yᘁ) Z) (MonoidalCategoryStruct.leftUnitor Z).hom))))

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} : CategoryStruct.comp (ᘁf) g = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor ᘁY).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (η_ (ᘁX) X) ᘁY) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (MonoidalCategoryStruct.tensorHom g f) ᘁY) (CategoryStruct.comp (MonoidalCategoryStruct.associator Z Y ᘁY).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Z (ε_ (ᘁY) Y)) (MonoidalCategoryStruct.rightUnitor Z).hom))))

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.

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.

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.

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.

def CategoryTheory.closedOfHasLeftDual {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (Y : C) [HasLeftDual Y] : Closed 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 }

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 (MonoidalCategoryStruct.tensorUnit 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 (MonoidalCategoryStruct.tensorUnit 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 (MonoidalCategoryStruct.tensorUnit 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 (MonoidalCategoryStruct.tensorUnit 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 (MonoidalCategoryStruct.tensorUnit 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 (MonoidalCategoryStruct.tensorUnit 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ᘁ (MonoidalCategoryStruct.tensorUnit 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ᘁ (MonoidalCategoryStruct.tensorUnit 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 : MonoidalCategoryStruct.tensorUnit 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 : MonoidalCategoryStruct.tensorUnit 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.

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.

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

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

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

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

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

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 }

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