Duality in full monoidal subcategories

An exact pairing between two objects of a monoidal category restricts to any full monoidal subcategory containing both objects: it is pulled back along the fully faithful monoidal inclusion by CategoryTheory.ExactPairing.ofFullyFaithful. Its evaluation and coevaluation are the ambient ones on underlying objects. Consequently an object and a chosen dual that both satisfy a monoidal property remain dual to one another after imposing that property.

Main declarations

• CategoryTheory.ObjectProperty.exactPairingFullSubcategory: an ambient exact pairing induces one in a full monoidal subcategory.

@[instance_reducible]

noncomputable instance CategoryTheory.ObjectProperty.exactPairingFullSubcategory {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {P : ObjectProperty C} [P.IsMonoidal] (X Y : P.FullSubcategory) [ExactPairing X.obj Y.obj] : ExactPairing X Y

An exact pairing between the underlying objects of a full monoidal subcategory is an exact pairing in that subcategory, obtained by pulling back along the inclusion P.ι.

Equations

• CategoryTheory.ObjectProperty.exactPairingFullSubcategory X Y = CategoryTheory.ExactPairing.ofFullyFaithful P.ι X Y

@[simp]

theorem CategoryTheory.ObjectProperty.exactPairingFullSubcategory_coevaluation_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {P : ObjectProperty C} [P.IsMonoidal] (X Y : P.FullSubcategory) [ExactPairing X.obj Y.obj] : (η_ X Y).hom = η_ X.obj Y.obj

The coevaluation of an ambient exact pairing, restricted to a full monoidal subcategory, is the ambient coevaluation on underlying objects.

@[simp]

theorem CategoryTheory.ObjectProperty.exactPairingFullSubcategory_evaluation_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {P : ObjectProperty C} [P.IsMonoidal] (X Y : P.FullSubcategory) [ExactPairing X.obj Y.obj] : (ε_ X Y).hom = ε_ X.obj Y.obj

The evaluation of an ambient exact pairing, restricted to a full monoidal subcategory, is the ambient evaluation on underlying objects.