Documentation

DerivedAlgGeo.CategoryTheory.Monoidal.Triangulated

Monoidal structures compatible with triangulation #

A monoidal category and a triangulated category are independent structures. This file records their compatibility: the tensor bifunctor is exact in both variables, with one coherent two-variable choice of shift comparisons.

The class is deliberately separate from MonoidalCategory. Not every monoidal category is triangulated, and not every triangulated category is monoidal. It is also separate from dg enrichment: enrichment uses a monoidal base category, while a monoidal dg category asks for additional compatibility between its enrichment and its tensor product.

source
class CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] :
Type (max u v)

Compatibility between a monoidal structure and a pretriangulated structure. The complete tensor bifunctor is exact in both variables.

Using Functor.ExactBifunctor here is stronger than listing exactness of every left tensor twist independently. Besides the right tensor twists, it records naturality of all shift comparisons in the fixed variable and Mathlib's Koszul compatibility between the two shift directions.

This is the generic parent interface for concrete exact tensor products such as a derived tensor product on Dᵇ(Coh X).

Instances
    source
    def CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation.exactBifunctor (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] [IsCompatibleWithTriangulation C] :
    (curriedTensor C).ExactBifunctor

    The exact-bifunctor witness carried by the compatibility root.

    Equations
    Instances For
      source
      @[reducible]
      def CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation.tensorCommShift (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] [IsCompatibleWithTriangulation C] (K : C) :
      ((curriedTensor C).obj K).CommShift ℤ

      A left tensor twist commutes with shifts. Retained as a projection-style API for consumers of the earlier one-slot interface.

      Equations
      Instances For
        source
        theorem CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation.tensorIsTriangulated (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] [IsCompatibleWithTriangulation C] (K : C) :
        ((curriedTensor C).obj K).IsTriangulated

        A left tensor twist is triangulated.

        source
        theorem CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation.tensorAdditive (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] [IsCompatibleWithTriangulation C] (K : C) :
        ((curriedTensor C).obj K).Additive

        A left tensor twist is additive.

        source
        @[reducible]
        def CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation.tensorFlipCommShift (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] [IsCompatibleWithTriangulation C] (K : C) :
        ((curriedTensor C).flip.obj K).CommShift ℤ

        A right tensor twist commutes with shifts.

        Equations
        Instances For
          source
          theorem CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation.tensorFlipIsTriangulated (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] [IsCompatibleWithTriangulation C] (K : C) :
          ((curriedTensor C).flip.obj K).IsTriangulated

          A right tensor twist is triangulated.

          source
          theorem CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation.tensorFlipAdditive (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [MonoidalCategory C] [IsCompatibleWithTriangulation C] (K : C) :
          ((curriedTensor C).flip.obj K).Additive

          A right tensor twist is additive.