Rigid (autonomous) monoidal categories #
This file defines rigid (autonomous) monoidal categories and the necessary theory about exact pairings and duals.
Main definitions #
ExactPairingof two objects of a monoidal category- Type classes
HasLeftDualandHasRightDualthat capture that a pairing exists - The
rightAdjointMate fas a morphismfᘁ : Yᘁ ⟶ Xᘁfor a morphismf : X ⟶ Y - The classes of
RightRigidCategory,LeftRigidCategoryandRigidCategory
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ᘁXdenote the right and left dual of an object, as well as the adjoint mate of a morphism.
Future work #
- Show that
X ⊗ YandYᘁ ⊗ 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 categoriesC ≅ (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₁
- coevaluation' : CategoryTheory.MonoidalCategory.tensorUnit C ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y
- evaluation' : CategoryTheory.MonoidalCategory.tensorObj Y X ⟶ CategoryTheory.MonoidalCategory.tensorUnit C
- 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
An exact pairing is a pair of objects X Y : C which admit
a coevaluation and evaluation morphism which fulfill two triangle equalities.
Instances
def
CategoryTheory.ExactPairing.coevaluation
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
(Y : C)
[CategoryTheory.ExactPairing X Y]
:
Instances For
def
CategoryTheory.ExactPairing.evaluation
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
(Y : C)
[CategoryTheory.ExactPairing X Y]
:
Instances For
@[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 (CategoryTheory.MonoidalCategory.tensorUnit 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 (CategoryTheory.MonoidalCategory.tensorUnit 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)
class
CategoryTheory.HasRightDual
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
:
Type (max u₁ v₁)
- rightDual : C
- exact : CategoryTheory.ExactPairing X Xᘁ
A class of objects which have a right dual.
Instances
class
CategoryTheory.HasLeftDual
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(Y : C)
:
Type (max u₁ v₁)
- leftDual : C
- exact : CategoryTheory.ExactPairing (ᘁY) Y
A class of objects which have a left dual.
Instances
instance
CategoryTheory.hasRightDualLeftDual
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
[CategoryTheory.HasLeftDual X]
:
instance
CategoryTheory.hasLeftDualRightDual
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
[CategoryTheory.HasRightDual X]
:
@[simp]
theorem
CategoryTheory.leftDual_rightDual
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
[CategoryTheory.HasRightDual X]
:
@[simp]
theorem
CategoryTheory.rightDual_leftDual
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
[CategoryTheory.HasLeftDual 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)
:
The right adjoint mate fᘁ : Xᘁ ⟶ Yᘁ of a morphism f : X ⟶ Y.
Instances For
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)
:
The left adjoint mate ᘁf : ᘁY ⟶ ᘁX of a morphism f : X ⟶ Y.
Instances For
@[simp]
theorem
CategoryTheory.rightAdjointMate_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
[CategoryTheory.HasRightDual X]
:
@[simp]
theorem
CategoryTheory.leftAdjointMate_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
[CategoryTheory.HasLeftDual 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)
:
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}
:
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)
:
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}
:
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']
:
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.
Instances For
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']
:
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.
Instances For
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')
:
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')
:
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']
:
If Y Y' have an exact pairing,
then the functor tensorLeft Y' is left adjoint to tensorLeft Y.
Instances For
def
CategoryTheory.tensorRightAdjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(Y : C)
(Y' : C)
[CategoryTheory.ExactPairing Y Y']
:
If Y Y' have an exact pairing,
then the functor tensor_right Y is left adjoint to tensor_right Y'.
Instances For
def
CategoryTheory.closedOfHasLeftDual
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(Y : C)
[CategoryTheory.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
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).
Instances For
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 (CategoryTheory.MonoidalCategory.tensorUnit 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 (CategoryTheory.MonoidalCategory.tensorUnit 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 (CategoryTheory.MonoidalCategory.tensorUnit 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 (CategoryTheory.MonoidalCategory.tensorUnit 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 (CategoryTheory.MonoidalCategory.tensorUnit 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 (CategoryTheory.MonoidalCategory.tensorUnit 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ᘁ (CategoryTheory.MonoidalCategory.tensorUnit 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ᘁ (CategoryTheory.MonoidalCategory.tensorUnit 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)
:
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)
:
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)
:
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)
:
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')
:
Transport an exact pairing across an isomorphism in the first argument.
Instances For
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')
:
Transport an exact pairing across an isomorphism in the second argument.
Instances For
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')
:
Transport an exact pairing across isomorphisms.
Instances For
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.
Instances For
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.
Instances For
@[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)
:
@[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)
:
class
CategoryTheory.RightRigidCategory
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
:
Type (max u v)
- rightDual : (X : C) → CategoryTheory.HasRightDual X
A right rigid monoidal category is one in which every object has a right dual.
Instances
class
CategoryTheory.LeftRigidCategory
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
:
Type (max u v)
- leftDual : (X : C) → CategoryTheory.HasLeftDual X
A left rigid monoidal category is one in which every object has a right dual.
Instances
def
CategoryTheory.monoidalClosedOfLeftRigidCategory
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.LeftRigidCategory 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).
Instances For
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.