Transport rigid structures over a monoidal equivalence. #
def
CategoryTheory.ExactPairing.ofFaithful
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
[F.Faithful]
{X Y : C}
(eval : MonoidalCategoryStruct.tensorObj Y X ⟶ MonoidalCategoryStruct.tensorUnit C)
(coeval : MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj X Y)
[ExactPairing (F.obj X) (F.obj Y)]
(map_eval :
F.map eval = CategoryStruct.comp (Functor.OplaxMonoidal.δ F Y X)
(CategoryStruct.comp (ε_ (F.obj X) (F.obj Y)) (Functor.LaxMonoidal.ε F)))
(map_coeval :
F.map coeval = CategoryStruct.comp (Functor.OplaxMonoidal.η F)
(CategoryStruct.comp (η_ (F.obj X) (F.obj Y)) (Functor.LaxMonoidal.μ F X Y)))
:
ExactPairing 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
Instances For
noncomputable def
CategoryTheory.ExactPairing.ofFullyFaithful
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
[F.Full]
[F.Faithful]
(X Y : C)
[ExactPairing (F.obj X) (F.obj Y)]
:
ExactPairing X 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
Instances For
@[deprecated CategoryTheory.ExactPairing.ofFaithful (since := "2025-10-17")]
def
CategoryTheory.exactPairingOfFaithful
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
[F.Faithful]
{X Y : C}
(eval : MonoidalCategoryStruct.tensorObj Y X ⟶ MonoidalCategoryStruct.tensorUnit C)
(coeval : MonoidalCategoryStruct.tensorUnit C ⟶ MonoidalCategoryStruct.tensorObj X Y)
[ExactPairing (F.obj X) (F.obj Y)]
(map_eval :
F.map eval = CategoryStruct.comp (Functor.OplaxMonoidal.δ F Y X)
(CategoryStruct.comp (ε_ (F.obj X) (F.obj Y)) (Functor.LaxMonoidal.ε F)))
(map_coeval :
F.map coeval = CategoryStruct.comp (Functor.OplaxMonoidal.η F)
(CategoryStruct.comp (η_ (F.obj X) (F.obj Y)) (Functor.LaxMonoidal.μ F X Y)))
:
ExactPairing X Y
Alias of CategoryTheory.ExactPairing.ofFaithful.
Given candidate data for an exact pairing, which is sent by a faithful monoidal functor to an exact pairing, the equations holds automatically.
Equations
Instances For
@[deprecated CategoryTheory.ExactPairing.ofFullyFaithful (since := "2025-10-17")]
def
CategoryTheory.exactPairingOfFullyFaithful
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
(F : Functor C D)
[F.Monoidal]
[F.Full]
[F.Faithful]
(X Y : C)
[ExactPairing (F.obj X) (F.obj Y)]
:
ExactPairing X Y
Alias of CategoryTheory.ExactPairing.ofFullyFaithful.
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
Instances For
def
CategoryTheory.hasLeftDualOfEquivalence
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
{F : Functor C D}
[F.Monoidal]
{G : Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
(X : C)
[HasLeftDual (F.obj X)]
:
Pull back a left dual along an equivalence.
Equations
Instances For
def
CategoryTheory.hasRightDualOfEquivalence
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
{F : Functor C D}
[F.Monoidal]
{G : Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
(X : C)
[HasRightDual (F.obj X)]
:
Pull back a right dual along an equivalence.
Equations
Instances For
def
CategoryTheory.leftRigidCategoryOfEquivalence
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
{F : Functor C D}
[F.Monoidal]
{G : Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
[LeftRigidCategory D]
:
Pull back a left rigid structure along an equivalence.
Equations
Instances For
def
CategoryTheory.rightRigidCategoryOfEquivalence
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
{F : Functor C D}
[F.Monoidal]
{G : Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
[RightRigidCategory D]
:
Pull back a right rigid structure along an equivalence.
Equations
Instances For
def
CategoryTheory.rigidCategoryOfEquivalence
{C : Type u_1}
{D : Type u_2}
[Category.{v_1, u_1} C]
[Category.{v_2, u_2} D]
[MonoidalCategory C]
[MonoidalCategory D]
{F : Functor C D}
[F.Monoidal]
{G : Functor D C}
(adj : F ⊣ G)
[F.IsEquivalence]
[RigidCategory D]
:
Pull back a rigid structure along an equivalence.