@[implicit_reducible]

noncomputable instance TensorDual.exactPairingTensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y X' Y' : C} [CategoryTheory.ExactPairing X X'] [CategoryTheory.ExactPairing Y Y'] : CategoryTheory.ExactPairing (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y' X')

Proposition 1.10.7(ii): if X and Y admit right duals X' and Y', then Y' ⊗ X' is naturally a right dual of X ⊗ Y via the standard exact pairing built from the duals of the factors.

@[reducible]

noncomputable def TensorDual.hasRightDualTensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X Y : C) [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] : CategoryTheory.HasRightDual (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

Proposition 1.10.7(ii): the right dual of X ⊗ Y is Yᘁ ⊗ Xᘁ.

@[reducible]

noncomputable def TensorDual.hasLeftDualTensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X Y : C) [CategoryTheory.HasLeftDual X] [CategoryTheory.HasLeftDual Y] : CategoryTheory.HasLeftDual (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

Proposition 1.10.7(ii): the left dual of X ⊗ Y is (ᘁY) ⊗ (ᘁX).

noncomputable def TensorDual.prop_1_10_9_i_eq1 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasRightDual V] (U W : C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj U V ⟶ W) ≃ (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W Vᘁ)

Proposition 1.10.9(i), first equation: the natural Hom-adjunction Hom(U ⊗ V, W) ≃ Hom(U, W ⊗ Vᘁ) when V has a right dual.

noncomputable def TensorDual.prop_1_10_9_i_eq2 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasRightDual V] (U W : C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj Vᘁ U ⟶ W) ≃ (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V W)

Proposition 1.10.9(i), second equation: the natural Hom-adjunction Hom(Vᘁ ⊗ U, W) ≃ Hom(U, V ⊗ W) when V has a right dual.

noncomputable def TensorDual.prop_1_10_9_i_adj_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasRightDual V] : CategoryTheory.MonoidalCategory.tensorRight V ⊣ CategoryTheory.MonoidalCategory.tensorRight Vᘁ

Proposition 1.10.9(i): the functor - ⊗ V is left adjoint to - ⊗ Vᘁ when V has a right dual.

noncomputable def TensorDual.prop_1_10_9_i_adj_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasRightDual V] : CategoryTheory.MonoidalCategory.tensorLeft Vᘁ ⊣ CategoryTheory.MonoidalCategory.tensorLeft V

Proposition 1.10.9(i): the functor Vᘁ ⊗ - is left adjoint to V ⊗ - when V has a right dual.

noncomputable def TensorDual.prop_1_10_9_ii_eq1 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasLeftDual V] (U W : C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj U ᘁV ⟶ W) ≃ (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W V)

Proposition 1.10.9(ii), first equation: the natural Hom-adjunction Hom(U ⊗ ᘁV, W) ≃ Hom(U, W ⊗ V) when V has a left dual.

noncomputable def TensorDual.prop_1_10_9_ii_eq2 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasLeftDual V] (U W : C) : (CategoryTheory.MonoidalCategoryStruct.tensorObj V U ⟶ W) ≃ (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (ᘁV) W)

Proposition 1.10.9(ii), second equation: the natural Hom-adjunction Hom(V ⊗ U, W) ≃ Hom(U, ᘁV ⊗ W) when V has a left dual.

noncomputable def TensorDual.prop_1_10_9_ii_adj_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasLeftDual V] : CategoryTheory.MonoidalCategory.tensorRight ᘁV ⊣ CategoryTheory.MonoidalCategory.tensorRight V

Proposition 1.10.9(ii): the functor - ⊗ ᘁV is left adjoint to - ⊗ V when V has a left dual.

noncomputable def TensorDual.prop_1_10_9_ii_adj_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasLeftDual V] : CategoryTheory.MonoidalCategory.tensorLeft V ⊣ CategoryTheory.MonoidalCategory.tensorLeft ᘁV

Proposition 1.10.9(ii): the functor V ⊗ - is left adjoint to ᘁV ⊗ - when V has a left dual.

noncomputable def TensorDual.prop_1_10_9 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V : C) [CategoryTheory.HasRightDual V] : (CategoryTheory.MonoidalCategory.tensorRight V ⊣ CategoryTheory.MonoidalCategory.tensorRight Vᘁ) × (CategoryTheory.MonoidalCategory.tensorLeft Vᘁ ⊣ CategoryTheory.MonoidalCategory.tensorLeft V)

Proposition 1.10.9: the pair of tensor-dual adjunctions associated to a right dualizable object, packaging both the right-tensor and left-tensor adjunctions in a single statement.