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

Tags

rigid category, monoidal category

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

  Coevaluation of an exact pairing.

  Do not use directly. Use ExactPairing.coevaluation instead.

• evaluation' : CategoryTheory.MonoidalCategory.tensorObj Y X ⟶ 𝟙_ C

  Evaluation of an exact pairing.

  Do not use directly. Use ExactPairing.evaluation instead.

• coevaluation_evaluation' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) CategoryTheory.ExactPairing.coevaluation') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Y).inv (CategoryTheory.MonoidalCategory.tensorHom CategoryTheory.ExactPairing.evaluation' (CategoryTheory.CategoryStruct.id Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Y).hom (CategoryTheory.MonoidalCategory.leftUnitor Y).inv
• evaluation_coevaluation' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom CategoryTheory.ExactPairing.coevaluation' (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) CategoryTheory.ExactPairing.evaluation')) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.MonoidalCategory.rightUnitor X).inv

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

Coevaluation of an exact pairing.

Equations

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

def CategoryTheory.ExactPairing.evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.ExactPairing X Y] : CategoryTheory.MonoidalCategory.tensorObj Y X ⟶ 𝟙_ 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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.ExactPairing X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) (η_ X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Y).inv (CategoryTheory.MonoidalCategory.tensorHom (ε_ X Y) (CategoryTheory.CategoryStruct.id Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Y).hom (CategoryTheory.MonoidalCategory.leftUnitor Y).inv

@[simp]

theorem CategoryTheory.ExactPairing.evaluation_coevaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.ExactPairing X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (η_ X Y) (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (ε_ X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.MonoidalCategory.rightUnitor X).inv

@[simp]

theorem CategoryTheory.ExactPairing.coevaluation_evaluation_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.ExactPairing X Y] {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) (η_ X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (ε_ X Y) (CategoryTheory.CategoryStruct.id Y)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor Y).inv h)

@[simp]

theorem CategoryTheory.ExactPairing.evaluation_coevaluation_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.ExactPairing X Y] {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (η_ X Y) (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (ε_ X Y)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv h)

instance CategoryTheory.exactPairingUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.ExactPairing (𝟙_ C) (𝟙_ C)

Equations

• CategoryTheory.exactPairingUnit = CategoryTheory.ExactPairing.mk (CategoryTheory.MonoidalCategory.rightUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.rightUnitor (𝟙_ C)).hom

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

class CategoryTheory.HasLeftDual {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.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 : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.HasRightDual (𝟙_ C)

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.hasRightDualLeftDual = CategoryTheory.HasRightDual.mk X

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

Equations

• CategoryTheory.hasLeftDualRightDual = CategoryTheory.HasLeftDual.mk X

@[simp]

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

@[simp]

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

def CategoryTheory.rightAdjointMate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasLeftDual X] [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} [CategoryTheory.HasRightDual X] : CategoryTheory.CategoryStruct.id Xᘁ = CategoryTheory.CategoryStruct.id Xᘁ

@[simp]

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

theorem CategoryTheory.rightAdjointMate_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] {f : X ⟶ Y} {g : Xᘁ ⟶ Z} : CategoryTheory.CategoryStruct.comp (fᘁ) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Yᘁ).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Yᘁ) (η_ X Xᘁ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Yᘁ) (CategoryTheory.MonoidalCategory.tensorHom f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Yᘁ Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (ε_ Y Yᘁ) (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.MonoidalCategory.leftUnitor Z).hom))))

theorem CategoryTheory.leftAdjointMate_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Z : C} [CategoryTheory.HasLeftDual X] [CategoryTheory.HasLeftDual Y] {f : X ⟶ Y} {g : ᘁX ⟶ Z} : CategoryTheory.CategoryStruct.comp (ᘁf) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor ᘁY).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (η_ (ᘁX) X) (CategoryTheory.CategoryStruct.id ᘁY)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom g f) (CategoryTheory.CategoryStruct.id ᘁY)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Z Y ᘁY).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) (ε_ (ᘁY) Y)) (CategoryTheory.MonoidalCategory.rightUnitor Z).hom))))

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

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

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

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

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

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

def CategoryTheory.tensorLeftHomEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Y' : C) (Z : C) [CategoryTheory.ExactPairing Y Y'] : (CategoryTheory.MonoidalCategory.tensorObj Y' X ⟶ Z) ≃ (X ⟶ CategoryTheory.MonoidalCategory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Y' : C) (Z : C) [CategoryTheory.ExactPairing Y Y'] : (CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) ≃ (X ⟶ CategoryTheory.MonoidalCategory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Y' : C} {Z : C} {Z' : C} [CategoryTheory.ExactPairing Y Y'] (f : CategoryTheory.MonoidalCategory.tensorObj Y' X ⟶ Z) (g : Z ⟶ Z') : (CategoryTheory.tensorLeftHomEquiv X Y Y' Z') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.tensorLeftHomEquiv X Y Y' Z) f) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) g)

theorem CategoryTheory.tensorLeftHomEquiv_symm_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} [CategoryTheory.ExactPairing Y Y'] (f : X ⟶ X') (g : X' ⟶ CategoryTheory.MonoidalCategory.tensorObj Y Z) : (CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y') f) ((CategoryTheory.tensorLeftHomEquiv X' Y Y' Z).symm g)

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

theorem CategoryTheory.tensorRightHomEquiv_symm_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} [CategoryTheory.ExactPairing Y Y'] (f : X ⟶ X') (g : X' ⟶ CategoryTheory.MonoidalCategory.tensorObj Z Y') : (CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y)) ((CategoryTheory.tensorRightHomEquiv X' Y Y' Z).symm g)

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

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

Equations

• CategoryTheory.tensorLeftAdjunction Y Y' = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (X Z : C) => CategoryTheory.tensorLeftHomEquiv X Y Y' Z)

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

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

Equations

• CategoryTheory.tensorRightAdjunction Y Y' = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk fun (X Z : C) => CategoryTheory.tensorRightHomEquiv X Y Y' Z)

def CategoryTheory.closedOfHasLeftDual {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (Y : C) [CategoryTheory.HasLeftDual Y] : CategoryTheory.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 category_theory.monoidal.functor_has_left_dual. 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 = { isAdj := { right := CategoryTheory.MonoidalCategory.tensorLeft ᘁY, adj := CategoryTheory.tensorLeftAdjunction (ᘁY) Y } }

theorem CategoryTheory.tensorLeftHomEquiv_tensor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} [CategoryTheory.ExactPairing Y Y'] (f : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y Z) (g : X' ⟶ Z') : (CategoryTheory.tensorLeftHomEquiv (CategoryTheory.MonoidalCategory.tensorObj X X') Y Y' (CategoryTheory.MonoidalCategory.tensorObj Z Z')).symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.MonoidalCategory.associator Y Z Z').hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y' X X').inv (CategoryTheory.MonoidalCategory.tensorHom ((CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm f) g)

tensorLeftHomEquiv commutes with tensoring on the right

theorem CategoryTheory.tensorRightHomEquiv_tensor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} {Z : C} {Z' : C} [CategoryTheory.ExactPairing Y Y'] (f : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Z Y') (g : X' ⟶ Z') : (CategoryTheory.tensorRightHomEquiv (CategoryTheory.MonoidalCategory.tensorObj X' X) Y Y' (CategoryTheory.MonoidalCategory.tensorObj Z' Z)).symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) (CategoryTheory.MonoidalCategory.associator Z' Z Y').inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X' X Y).hom (CategoryTheory.MonoidalCategory.tensorHom g ((CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm f))

tensorRightHomEquiv commutes with tensoring on the left

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_id_tensor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {Y : C} {Y' : C} {Z : C} [CategoryTheory.ExactPairing Y Y'] (f : Y' ⟶ Z) : (CategoryTheory.tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (CategoryTheory.CategoryStruct.comp (η_ Y Y') (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Y').hom f

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_tensor_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] (f : X ⟶ Y) : (CategoryTheory.tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Xᘁ))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor Yᘁ).hom (fᘁ)

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_id_tensor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasLeftDual X] [CategoryTheory.HasLeftDual Y] (f : X ⟶ Y) : (CategoryTheory.tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (CategoryTheory.CategoryStruct.comp (η_ (ᘁX) X) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ᘁX) f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor ᘁY).hom (ᘁf)

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_tensor_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {Y : C} {Y' : C} {Z : C} [CategoryTheory.ExactPairing Y Y'] (f : Y ⟶ Z) : (CategoryTheory.tensorRightHomEquiv (𝟙_ C) Y Y' Z).symm (CategoryTheory.CategoryStruct.comp (η_ Y Y') (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y'))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor Y).hom f

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_id_tensor_comp_evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {Y : C} {Z : C} [CategoryTheory.HasLeftDual Z] (f : Y ⟶ ᘁZ) : (CategoryTheory.tensorLeftHomEquiv Y (ᘁZ) Z (𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) (ε_ (ᘁZ) Z)) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.rightUnitor ᘁZ).inv

@[simp]

theorem CategoryTheory.tensorLeftHomEquiv_tensor_id_comp_evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasLeftDual X] [CategoryTheory.HasLeftDual Y] (f : X ⟶ Y) : (CategoryTheory.tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id ᘁY)) (ε_ (ᘁY) Y)) = CategoryTheory.CategoryStruct.comp (ᘁf) (CategoryTheory.MonoidalCategory.rightUnitor ᘁX).inv

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_id_tensor_comp_evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] (f : X ⟶ Y) : (CategoryTheory.tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Yᘁ) f) (ε_ Y Yᘁ)) = CategoryTheory.CategoryStruct.comp (fᘁ) (CategoryTheory.MonoidalCategory.leftUnitor Xᘁ).inv

@[simp]

theorem CategoryTheory.tensorRightHomEquiv_tensor_id_comp_evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasRightDual X] (f : Y ⟶ Xᘁ) : (CategoryTheory.tensorRightHomEquiv Y X Xᘁ (𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X)) (ε_ X Xᘁ)) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.leftUnitor Xᘁ).inv

theorem CategoryTheory.coevaluation_comp_rightAdjointMate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (η_ Y Yᘁ) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) (fᘁ)) = CategoryTheory.CategoryStruct.comp (η_ X Xᘁ) (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Xᘁ))

theorem CategoryTheory.leftAdjointMate_comp_evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasLeftDual X] [CategoryTheory.HasLeftDual Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (ᘁf)) (ε_ (ᘁX) X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id ᘁY)) (ε_ (ᘁY) Y)

theorem CategoryTheory.coevaluation_comp_leftAdjointMate {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasLeftDual X] [CategoryTheory.HasLeftDual Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (η_ (ᘁY) Y) (CategoryTheory.MonoidalCategory.tensorHom (ᘁf) (CategoryTheory.CategoryStruct.id Y)) = CategoryTheory.CategoryStruct.comp (η_ (ᘁX) X) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ᘁX) f)

theorem CategoryTheory.rightAdjointMate_comp_evaluation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (fᘁ) (CategoryTheory.CategoryStruct.id X)) (ε_ X Xᘁ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Yᘁ) f) (ε_ Y Yᘁ)

def CategoryTheory.exactPairingCongrLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} [CategoryTheory.ExactPairing X' Y] (i : X ≅ X') : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {Y : C} {Y' : C} [CategoryTheory.ExactPairing X Y'] (i : Y ≅ Y') : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} {X' : C} {Y : C} {Y' : C} [CategoryTheory.ExactPairing X' Y'] (i : X ≅ X') (j : Y ≅ Y') : CategoryTheory.ExactPairing X Y

Transport an exact pairing across isomorphisms.

Equations

• CategoryTheory.exactPairingCongr i j = CategoryTheory.exactPairingCongrLeft i

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

Right duals are isomorphic.

Equations

• CategoryTheory.rightDualIso p₁ p₂ = CategoryTheory.Iso.mk (CategoryTheory.CategoryStruct.id Xᘁ) (CategoryTheory.CategoryStruct.id Xᘁ)

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

Left duals are isomorphic.

Equations

• CategoryTheory.leftDualIso p₁ p₂ = CategoryTheory.Iso.mk (ᘁCategoryTheory.CategoryStruct.id Y) (ᘁCategoryTheory.CategoryStruct.id Y)

@[simp]

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

@[simp]

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

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

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

• rightDual : (X : C) → CategoryTheory.HasRightDual X

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

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

• leftDual : (X : C) → CategoryTheory.HasLeftDual X

def CategoryTheory.monoidalClosedOfLeftRigidCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.LeftRigidCategory C] : CategoryTheory.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 category_theory.monoidal.left_rigid_functor_category. 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) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] extends CategoryTheory.RightRigidCategory , CategoryTheory.LeftRigidCategory : Type (max u v)

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