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 ⟶ 𝟙_ C) (coeval : 𝟙_ C ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y) [CategoryTheory.ExactPairing (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)] (map_eval : F.toPrefunctor.map eval = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.toLaxMonoidalFunctor.μ Y X)) (CategoryTheory.CategoryStruct.comp (ε_ (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)) F.ε)) (map_coeval : F.toPrefunctor.map coeval = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv F.ε) (CategoryTheory.CategoryStruct.comp (η_ (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)) (F.toLaxMonoidalFunctor.μ X Y))) : CategoryTheory.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

• CategoryTheory.exactPairingOfFaithful F eval coeval map_eval map_coeval = CategoryTheory.ExactPairing.mk coeval eval

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.toPrefunctor.obj X) (F.toPrefunctor.obj Y)] : CategoryTheory.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

• 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.MonoidalFunctor C D) [CategoryTheory.IsEquivalence F.toFunctor] (X : C) [CategoryTheory.HasLeftDual (F.toPrefunctor.obj X)] : CategoryTheory.HasLeftDual X

Pull back a left dual along an equivalence.

Equations

• CategoryTheory.hasLeftDualOfEquivalence F X = CategoryTheory.HasLeftDual.mk ((CategoryTheory.Functor.inv F.toFunctor).toPrefunctor.obj ᘁ(F.toPrefunctor.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.MonoidalFunctor C D) [CategoryTheory.IsEquivalence F.toFunctor] (X : C) [CategoryTheory.HasRightDual (F.toPrefunctor.obj X)] : CategoryTheory.HasRightDual X

Pull back a right dual along an equivalence.

Equations

• CategoryTheory.hasRightDualOfEquivalence F X = CategoryTheory.HasRightDual.mk ((CategoryTheory.Functor.inv F.toFunctor).toPrefunctor.obj (F.toPrefunctor.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.MonoidalFunctor C D) [CategoryTheory.IsEquivalence F.toFunctor] [CategoryTheory.LeftRigidCategory D] : CategoryTheory.LeftRigidCategory C

Pull back a left rigid structure along an equivalence.

Equations

• CategoryTheory.leftRigidCategoryOfEquivalence F = 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.MonoidalFunctor C D) [CategoryTheory.IsEquivalence F.toFunctor] [CategoryTheory.RightRigidCategory D] : CategoryTheory.RightRigidCategory C

Pull back a right rigid structure along an equivalence.

Equations

• CategoryTheory.rightRigidCategoryOfEquivalence F = 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.MonoidalFunctor C D) [CategoryTheory.IsEquivalence F.toFunctor] [CategoryTheory.RigidCategory D] : CategoryTheory.RigidCategory C

Pull back a rigid structure along an equivalence.

Equations

• CategoryTheory.rigidCategoryOfEquivalence F = CategoryTheory.RigidCategory.mk