@[reducible, inline]

abbrev TensorCategories.Definition_1_10_1 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u v)

Definition 1.10.1 (alias): an object X has a right dual.

@[reducible, inline]

abbrev TensorCategories.Definition_1_10_1_RightDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u v)

Definition 1.10.1 (named right dual): an object X has a right dual.

@[reducible, inline]

abbrev TensorCategories.def_1_10_1_LeftDual {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u v)

Companion to Definition 1.10.1: an object X has a left dual.

@[reducible, inline]

abbrev TensorCategories.Definition_1_10_2 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u v)

Definition 1.10.2: an object X has a left dual.

def TensorCategories.prop_1_10_4_right_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : CategoryTheory.ExactPairing X Y₁) (p₂ : CategoryTheory.ExactPairing X Y₂) : Y₁ ≅ Y₂

Proposition 1.10.4 (right): Any two right duals Y₁, Y₂ of X are canonically isomorphic.

def TensorCategories.prop_1_10_4_left_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y : C} (p₁ : CategoryTheory.ExactPairing X₁ Y) (p₂ : CategoryTheory.ExactPairing X₂ Y) : X₁ ≅ X₂

Proposition 1.10.4 (left): Any two left duals X₁, X₂ of Y are canonically isomorphic.

theorem TensorCategories.whiskerRight_evaluation_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y₁ Y₂ : C} (p₂ : CategoryTheory.ExactPairing X Y₂) {f g : Y₁ ⟶ Y₂} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) (ε_ X Y₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g X) (ε_ X Y₂)) : f = g

If two morphisms f, g : Y₁ ⟶ Y₂ agree after whiskering by X on the right and composing with the evaluation of an exact pairing (X, Y₂), then they are equal.

theorem TensorCategories.whiskerLeft_evaluation_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y : C} (p₂ : CategoryTheory.ExactPairing X₂ Y) {f g : X₁ ⟶ X₂} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f) (ε_ X₂ Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y g) (ε_ X₂ Y)) : f = g

If two morphisms f, g : X₁ ⟶ X₂ agree after whiskering by Y on the left and composing with the evaluation of an exact pairing (X₂, Y), then they are equal.

theorem TensorCategories.rightDualIso_hom_comp_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : CategoryTheory.ExactPairing X Y₁) (p₂ : CategoryTheory.ExactPairing X Y₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.rightDualIso p₁ p₂).hom X) (ε_ X Y₂) = ε_ X Y₁

The canonical isomorphism between two right duals of X intertwines the evaluation maps: (rightDualIso p₁ p₂).hom ▷ X ≫ p₂.evaluation = p₁.evaluation.

theorem TensorCategories.leftDualIso_hom_comp_evaluation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y : C} (p₁ : CategoryTheory.ExactPairing X₁ Y) (p₂ : CategoryTheory.ExactPairing X₂ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.leftDualIso p₁ p₂).hom) (ε_ X₂ Y) = ε_ X₁ Y

The canonical isomorphism between two left duals of Y intertwines the evaluation maps: Y ◁ (leftDualIso p₁ p₂).hom ≫ p₂.evaluation = p₁.evaluation.

theorem TensorCategories.Proposition_1_10_4_rightDual_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : CategoryTheory.ExactPairing X Y₁) (p₂ : CategoryTheory.ExactPairing X Y₂) : ∃! f : Y₁ ⟶ Y₂, CategoryTheory.IsIso f ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) (ε_ X Y₂) = ε_ X Y₁

Proposition 1.10.4: A right dual of X is unique up to a unique isomorphism that intertwines the evaluation maps.

theorem TensorCategories.prop_1_10_7i_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y Z : C} [CategoryTheory.HasRightDual X] [CategoryTheory.HasRightDual Y] [CategoryTheory.HasRightDual Z] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f gᘁ = CategoryTheory.CategoryStruct.comp (gᘁ) (fᘁ)

Proposition 1.10.7(i) for right duals: the right dual of a composition is the composition of the right duals in reverse order, (f ≫ g)ᘁ = gᘁ ≫ fᘁ.

def TensorCategories.prop_1_10_9_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (U V V' W : C) [CategoryTheory.ExactPairing V V'] : (CategoryTheory.MonoidalCategoryStruct.tensorObj U V ⟶ W) ≃ (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W V')

Proposition 1.10.9 (i, first equivalence): Hom(U ⊗ V, W) ≃ Hom(U, W ⊗ V') for an exact pairing (V, V').

def TensorCategories.prop_1_10_9_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (U V V' W : C) [CategoryTheory.ExactPairing V V'] : (CategoryTheory.MonoidalCategoryStruct.tensorObj V' U ⟶ W) ≃ (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V W)

Proposition 1.10.9 (i, second equivalence): Hom(V' ⊗ U, W) ≃ Hom(U, V ⊗ W) for an exact pairing (V, V').

def TensorCategories.prop_1_10_9_right_adj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V V' : C) [CategoryTheory.ExactPairing V V'] : CategoryTheory.MonoidalCategory.tensorRight V ⊣ CategoryTheory.MonoidalCategory.tensorRight V'

Proposition 1.10.9 adjunction (i): (- ⊗ V) ⊣ (- ⊗ V') for an exact pairing (V, V').

def TensorCategories.prop_1_10_9_left_adj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V V' : C) [CategoryTheory.ExactPairing V V'] : CategoryTheory.MonoidalCategory.tensorLeft V' ⊣ CategoryTheory.MonoidalCategory.tensorLeft V

Proposition 1.10.9 adjunction (i, left): (V' ⊗ -) ⊣ (V ⊗ -) for an exact pairing (V, V').

def TensorCategories.prop_1_10_9_tensorRight_adj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [CategoryTheory.HasRightDual X] : CategoryTheory.MonoidalCategory.tensorRight X ⊣ CategoryTheory.MonoidalCategory.tensorRight Xᘁ

Proposition 1.10.9: For X with a right dual Xᘁ, the functor (- ⊗ X) is left adjoint to (- ⊗ Xᘁ).

def TensorCategories.prop_1_10_9_tensorLeft_adj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [CategoryTheory.HasRightDual X] : CategoryTheory.MonoidalCategory.tensorLeft Xᘁ ⊣ CategoryTheory.MonoidalCategory.tensorLeft X

Proposition 1.10.9: For X with a right dual Xᘁ, the functor (Xᘁ ⊗ -) is left adjoint to (X ⊗ -).

def TensorCategories.prop_1_10_9ii_tensorRight_adj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [CategoryTheory.HasLeftDual X] : CategoryTheory.MonoidalCategory.tensorRight ᘁX ⊣ CategoryTheory.MonoidalCategory.tensorRight X

Proposition 1.10.9 (ii): For X with a left dual ᘁX, the functor (- ⊗ ᘁX) is left adjoint to (- ⊗ X).

def TensorCategories.prop_1_10_9ii_tensorLeft_adj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) [CategoryTheory.HasLeftDual X] : CategoryTheory.MonoidalCategory.tensorLeft X ⊣ CategoryTheory.MonoidalCategory.tensorLeft ᘁX

Proposition 1.10.9 (ii): For X with a left dual ᘁX, the functor (X ⊗ -) is left adjoint to (ᘁX ⊗ -).

noncomputable def TensorCategories.remark_1_10_10_representability {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (V V' W : C) [CategoryTheory.ExactPairing V V'] : (V' ⟶ W) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj V W)

Remark 1.10.10 (representability): Hom(V', W) ≃ Hom(𝟙, V ⊗ W) for an exact pairing (V, V').

noncomputable def TensorCategories.remark_1_10_10_hom_equiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y₁ Y₂ : C} (p₁ : CategoryTheory.ExactPairing X Y₁) (p₂ : CategoryTheory.ExactPairing X Y₂) (W : C) : (Y₁ ⟶ W) ≃ (Y₂ ⟶ W)

Remark 1.10.10: For two right duals Y₁, Y₂ of X, the hom-functor out of them agrees: Hom(Y₁, W) ≃ Hom(Y₂, W).

noncomputable def TensorCategories.remark_1_10_10_representability_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X X' W : C) [CategoryTheory.ExactPairing X' X] : (X' ⟶ W) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W X)

Remark 1.10.10 (representability, left version): Hom(X', W) ≃ Hom(𝟙, W ⊗ X) for an exact pairing (X', X).

noncomputable def TensorCategories.remark_1_10_10_hom_equiv_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X₁ X₂ Y : C} (p₁ : CategoryTheory.ExactPairing X₁ Y) (p₂ : CategoryTheory.ExactPairing X₂ Y) (W : C) : (X₁ ⟶ W) ≃ (X₂ ⟶ W)

Remark 1.10.10 (left version): Two left duals X₁, X₂ of Y have the same hom-out functor: Hom(X₁, W) ≃ Hom(X₂, W).

instance TensorCategories.tensorLeft_preservesLimitsOfSize' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorLeft X)

In a rigid monoidal category, the functor X ⊗ - preserves all limits, as it is the right adjoint of Xᘁ ⊗ -.

instance TensorCategories.tensorLeft_preservesColimitsOfSize' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorLeft X)

In a rigid monoidal category, the functor X ⊗ - preserves all colimits, as it is the left adjoint of ᘁX ⊗ -.

instance TensorCategories.tensorRight_preservesLimitsOfSize' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorRight X)

In a rigid monoidal category, the functor - ⊗ X preserves all limits.

instance TensorCategories.tensorRight_preservesColimitsOfSize' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorRight X)

In a rigid monoidal category, the functor - ⊗ X preserves all colimits.

instance TensorCategories.tensorLeft_preservesFiniteLimits' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft X)

Specialization of preservation of all limits: X ⊗ - preserves finite limits.

instance TensorCategories.tensorLeft_preservesFiniteColimits' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft X)

Specialization of preservation of all colimits: X ⊗ - preserves finite colimits.

instance TensorCategories.tensorRight_preservesFiniteLimits' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorRight X)

Specialization of preservation of all limits: - ⊗ X preserves finite limits.

instance TensorCategories.tensorRight_preservesFiniteColimits' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RigidCategory C] (X : C) : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorRight X)

Specialization of preservation of all colimits: - ⊗ X preserves finite colimits.

@[reducible, inline]

abbrev TensorCategories.def_1_10_11 (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Type (max u_1 u_2)

Definition 1.10.11 (alias): a rigid monoidal category.

@[reducible, inline]

abbrev TensorCategories.Definition_1_10_11_RigidCategory (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Type (max u_1 u_2)

Definition 1.10.11: A monoidal category C is rigid if every object has both a right dual and a left dual.

def TensorCategories.dualityFunctor_right (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.RightRigidCategory C] : CategoryTheory.Functor C Cᵒᵖᴹᵒᵖ

The right-duality functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ on a right-rigid category, sending each object to its right dual.

def TensorCategories.dualityFunctor_left (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.LeftRigidCategory C] : CategoryTheory.Functor C Cᵒᵖᴹᵒᵖ

The left-duality functor C ⥤ (Cᵒᵖ)ᴹᵒᵖ on a left-rigid category, sending each object to its left dual.