Transport rigid structures over a monoidal equivalence.

def CategoryTheory.ExactPairing.ofFaithful {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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

• CategoryTheory.ExactPairing.ofFaithful F eval coeval map_eval map_coeval = { coevaluation' := coeval, evaluation' := eval, coevaluation_evaluation' := ⋯, evaluation_coevaluation' := ⋯ }

noncomputable def CategoryTheory.ExactPairing.ofFullyFaithful {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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

• One or more equations did not get rendered due to their size.

@[deprecated CategoryTheory.ExactPairing.ofFaithful (since := "2025-10-17")]

def CategoryTheory.exactPairingOfFaithful {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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

• @CategoryTheory.exactPairingOfFaithful = @CategoryTheory.ExactPairing.ofFaithful

@[deprecated CategoryTheory.ExactPairing.ofFullyFaithful (since := "2025-10-17")]

def CategoryTheory.exactPairingOfFullyFaithful {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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

• @CategoryTheory.exactPairingOfFullyFaithful = @CategoryTheory.ExactPairing.ofFullyFaithful

def CategoryTheory.hasLeftDualOfEquivalence {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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)] : HasLeftDual X

Pull back a left dual along an equivalence.

Equations

• CategoryTheory.hasLeftDualOfEquivalence adj X = { leftDual := G.obj ᘁ(F.obj X), exact := CategoryTheory.ExactPairing.ofFullyFaithful F (G.obj ᘁ(F.obj X)) X }

def CategoryTheory.hasRightDualOfEquivalence {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, 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)] : HasRightDual X

Pull back a right dual along an equivalence.

Equations

• CategoryTheory.hasRightDualOfEquivalence adj X = { rightDual := G.obj (F.obj X)ᘁ, exact := CategoryTheory.ExactPairing.ofFullyFaithful F X (G.obj (F.obj X)ᘁ) }

def CategoryTheory.leftRigidCategoryOfEquivalence {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : Functor D C} (adj : F ⊣ G) [F.IsEquivalence] [LeftRigidCategory D] : LeftRigidCategory C

Pull back a left rigid structure along an equivalence.

Equations

• CategoryTheory.leftRigidCategoryOfEquivalence adj = { leftDual := fun (X : C) => CategoryTheory.hasLeftDualOfEquivalence adj X }

def CategoryTheory.rightRigidCategoryOfEquivalence {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : Functor D C} (adj : F ⊣ G) [F.IsEquivalence] [RightRigidCategory D] : RightRigidCategory C

Pull back a right rigid structure along an equivalence.

Equations

• CategoryTheory.rightRigidCategoryOfEquivalence adj = { rightDual := fun (X : C) => CategoryTheory.hasRightDualOfEquivalence adj X }

def CategoryTheory.rigidCategoryOfEquivalence {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [MonoidalCategory C] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : Functor D C} (adj : F ⊣ G) [F.IsEquivalence] [RigidCategory D] : RigidCategory C

Pull back a rigid structure along an equivalence.

Equations

• One or more equations did not get rendered due to their size.