Tensoring is exact in a rigid abelian category

Deligne's 1.14 (Catégories tensorielles): in a rigid category the functor − ⊗ X has − ⊗ Xᘁ as a two-sided adjoint, so over an abelian base it preserves all finite limits and colimits — it is exact. The consequences collected here: tensoring preserves monomorphisms, epimorphisms, and zero objects, and a tensor power of a nonzero object detects nothing (X ^ ⊗ n = 0 forces X = 0, Deligne 1.17).

instance RS.tensorRight_preservesColimits {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (X : A) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorRight X)

Right tensoring preserves all colimits: − ⊗ X is a left adjoint (Frobenius reciprocity, with adjoint − ⊗ Xᘁ).

instance RS.tensorRight_preservesLimits {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (X : A) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorRight X)

Right tensoring preserves all limits: − ⊗ X is a right adjoint (with adjoint − ⊗ ᘁX).

instance RS.tensorLeft_preservesColimits {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (X : A) : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorLeft X)

Left tensoring preserves all colimits.

instance RS.tensorLeft_preservesLimits {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.RigidCategory A] (X : A) : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v, v, u, u} (CategoryTheory.MonoidalCategory.tensorLeft X)

Left tensoring preserves all limits.