Documentation

Mathlib.CategoryTheory.Monoidal.Tor

Tor, the left-derived functor of tensor product #

We define Tor C n : C ⥤ C ⥤ C, by left-deriving in the second factor of (X, Y) ↦ X ⊗ Y.

For now we have almost nothing to say about it!

It would be good to show that this is naturally isomorphic to the functor obtained by left-deriving in the first factor, instead. For now we define Tor' by left-deriving in the first factor, but showing Tor C n ≅ Tor' C n will require a bit more theory! Possibly it's best to axiomatize delta functors, and obtain a unique characterisation?

source
def CategoryTheory.Tor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) :
CategoryTheory.Functor C (CategoryTheory.Functor C C)

We define Tor C n : C ⥤ C ⥤ C by left-deriving in the second factor of (X, Y) ↦ X ⊗ Y.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Tor_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
    (CategoryTheory.Tor C n).map f = CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f) n
    source
    @[simp]
    theorem CategoryTheory.Tor_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (X : C) :
    (CategoryTheory.Tor C n).obj X = ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X).leftDerived n
    source
    def CategoryTheory.Tor' (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) :
    CategoryTheory.Functor C (CategoryTheory.Functor C C)

    An alternative definition of Tor, where we left-derive in the first factor instead.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Tor'_obj_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (k j : C) :
      ((CategoryTheory.Tor' C n).obj k).obj j = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).obj k
      source
      @[simp]
      theorem CategoryTheory.Tor'_map_app' (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X Y : C} (f : X ⟶ Y) (Z : C) :
      ((CategoryTheory.Tor' C n).map f).app Z = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj Z).leftDerived n).map f
      source
      @[simp]
      theorem CategoryTheory.Tor'_obj_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X Y : C} (Z : C) (f : X ⟶ Y) :
      ((CategoryTheory.Tor' C n).obj Z).map f = (CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringRight C).map f) n).app Z
      source
      theorem CategoryTheory.isZero_Tor_succ_of_projective (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective Y] (n : ℕ) :
      CategoryTheory.Limits.IsZero (((CategoryTheory.Tor C (n + 1)).obj X).obj Y)

      The higher Tor groups for X and Y are zero if Y is projective.

      source
      theorem CategoryTheory.isZero_Tor'_succ_of_projective (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective X] (n : ℕ) :
      CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' C (n + 1)).obj X).obj Y)

      The higher Tor' groups for X and Y are zero if X is projective.