Transport rigid structures over a monoidal equivalence. #
def
CategoryTheory.exactPairingOfFaithful
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
[CategoryTheory.Faithful F.toFunctor]
{X : C}
{Y : C}
(eval : CategoryTheory.MonoidalCategory.tensorObj Y X ⟶ CategoryTheory.MonoidalCategory.tensorUnit C)
(coeval : CategoryTheory.MonoidalCategory.tensorUnit C ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y)
[CategoryTheory.ExactPairing (F.obj X) (F.obj Y)]
(map_eval : F.map eval = CategoryTheory.CategoryStruct.comp
(CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X))
(CategoryTheory.CategoryStruct.comp (ε_ (F.obj X) (F.obj Y)) F.ε))
(map_coeval : F.map coeval = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv F.ε)
(CategoryTheory.CategoryStruct.comp (η_ (F.obj X) (F.obj Y))
(CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y)))
:
Given candidate data for an exact pairing, which is sent by a faithful monoidal functor to an exact pairing, the equations holds automatically.
Instances For
def
CategoryTheory.exactPairingOfFullyFaithful
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
[CategoryTheory.Full F.toFunctor]
[CategoryTheory.Faithful F.toFunctor]
(X : C)
(Y : C)
[CategoryTheory.ExactPairing (F.obj X) (F.obj Y)]
:
Given a pair of objects which are sent by a fully faithful functor to a pair of objects with an exact pairing, we get an exact pairing.
Instances For
def
CategoryTheory.hasLeftDualOfEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
[CategoryTheory.IsEquivalence F.toFunctor]
(X : C)
[CategoryTheory.HasLeftDual (F.obj X)]
:
Pull back a left dual along an equivalence.
Instances For
def
CategoryTheory.hasRightDualOfEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
[CategoryTheory.IsEquivalence F.toFunctor]
(X : C)
[CategoryTheory.HasRightDual (F.obj X)]
:
Pull back a right dual along an equivalence.
Instances For
def
CategoryTheory.leftRigidCategoryOfEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
[CategoryTheory.IsEquivalence F.toFunctor]
[CategoryTheory.LeftRigidCategory D]
:
Pull back a left rigid structure along an equivalence.
Instances For
def
CategoryTheory.rightRigidCategoryOfEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
[CategoryTheory.IsEquivalence F.toFunctor]
[CategoryTheory.RightRigidCategory D]
:
Pull back a right rigid structure along an equivalence.
Instances For
def
CategoryTheory.rigidCategoryOfEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
[CategoryTheory.IsEquivalence F.toFunctor]
[CategoryTheory.RigidCategory D]
:
Pull back a rigid structure along an equivalence.