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.Functor C D)
[F.Monoidal]
[F.Faithful]
{X Y : C}
(eval : CategoryTheory.MonoidalCategory.tensorObj Y X ⟶ 𝟙_ C)
(coeval : 𝟙_ C ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y)
[CategoryTheory.ExactPairing (F.obj X) (F.obj Y)]
(map_eval :
F.map eval = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F Y X)
(CategoryTheory.CategoryStruct.comp (ε_ (F.obj X) (F.obj Y)) (CategoryTheory.Functor.LaxMonoidal.ε F)))
(map_coeval :
F.map coeval = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F)
(CategoryTheory.CategoryStruct.comp (η_ (F.obj X) (F.obj Y)) (CategoryTheory.Functor.LaxMonoidal.μ F 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.
Equations
- CategoryTheory.exactPairingOfFaithful F eval coeval map_eval map_coeval = { coevaluation' := coeval, evaluation' := eval, coevaluation_evaluation' := ⋯, evaluation_coevaluation' := ⋯ }
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.Functor C D)
[F.Monoidal]
[F.Full]
[F.Faithful]
(X 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.
Equations
- One or more equations did not get rendered due to their size.
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.Functor C D}
[F.Monoidal]
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
(X : C)
[CategoryTheory.HasLeftDual (F.obj X)]
:
Pull back a left dual along an equivalence.
Equations
- CategoryTheory.hasLeftDualOfEquivalence adj X = CategoryTheory.HasLeftDual.mk (G.obj ᘁ(F.obj X))
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.Functor C D}
[F.Monoidal]
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
(X : C)
[CategoryTheory.HasRightDual (F.obj X)]
:
Pull back a right dual along an equivalence.
Equations
- CategoryTheory.hasRightDualOfEquivalence adj X = CategoryTheory.HasRightDual.mk (G.obj (F.obj X)ᘁ)
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.Functor C D}
[F.Monoidal]
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
[CategoryTheory.LeftRigidCategory D]
:
Pull back a left rigid structure along an equivalence.
Equations
- CategoryTheory.leftRigidCategoryOfEquivalence adj = CategoryTheory.LeftRigidCategory.mk
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.Functor C D}
[F.Monoidal]
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
[CategoryTheory.RightRigidCategory D]
:
Pull back a right rigid structure along an equivalence.
Equations
- CategoryTheory.rightRigidCategoryOfEquivalence adj = CategoryTheory.RightRigidCategory.mk
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.Functor C D}
[F.Monoidal]
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
[CategoryTheory.RigidCategory D]
:
Pull back a rigid structure along an equivalence.
Equations
- CategoryTheory.rigidCategoryOfEquivalence adj = CategoryTheory.RigidCategory.mk