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) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (n : ℕ) :
Functor C (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) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
    (Tor C n).map f = NatTrans.leftDerived ((MonoidalCategory.tensoringLeft C).map f) n
    source
    @[simp]
    theorem CategoryTheory.Tor_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (n : ℕ) (X : C) :
    (Tor C n).obj X = ((MonoidalCategory.tensoringLeft C).obj X).leftDerived n
    source
    def CategoryTheory.Tor' (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (n : ℕ) :
    Functor C (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'_map_app (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : C) :
      ((Tor' C n).map f).app j = (((MonoidalCategory.tensoringRight C).obj j).leftDerived n).map f
      source
      @[simp]
      theorem CategoryTheory.Tor'_obj_map (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (n : ℕ) (k : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
      ((Tor' C n).obj k).map f = (NatTrans.leftDerived ((MonoidalCategory.tensoringRight C).map f) n).app k
      source
      @[simp]
      theorem CategoryTheory.Tor'_obj_obj (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (n : ℕ) (k j : C) :
      ((Tor' C n).obj k).obj j = (((MonoidalCategory.tensoringRight C).obj j).leftDerived n).obj k
      source
      theorem CategoryTheory.isZero_Tor_succ_of_projective (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (X Y : C) [Projective Y] (n : ℕ) :
      Limits.IsZero (((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) [Category.{u_2, u_1} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (X Y : C) [Projective X] (n : ℕ) :
      Limits.IsZero (((Tor' C (n + 1)).obj X).obj Y)

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