# 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?

@[simp]
theorem CategoryTheory.Tor_map (C : Type u_1) [] (n : ) :
∀ {X Y : C} (f : X Y), ().map f =
@[simp]
theorem CategoryTheory.Tor_obj (C : Type u_1) [] (n : ) (X : C) :
().obj X =

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
@[simp]
theorem CategoryTheory.Tor'_obj_obj (C : Type u_1) [] (n : ) (k : C) (j : C) :
(().obj k).obj j =

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
@[simp]
theorem CategoryTheory.Tor'_map_app' (C : Type u_1) [] (n : ) {X : C} {Y : C} (f : X Y) (Z : C) :
(().map f).app Z = .map f
@[simp]
theorem CategoryTheory.Tor'_obj_map (C : Type u_1) [] (n : ) {X : C} {Y : C} (Z : C) (f : X Y) :
(().obj Z).map f = .app Z
theorem CategoryTheory.isZero_Tor_succ_of_projective (C : Type u_1) [] (X : C) (Y : C) (n : ) :

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

theorem CategoryTheory.isZero_Tor'_succ_of_projective (C : Type u_1) [] (X : C) (Y : C) (n : ) :

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