# mathlibdocumentation

category_theory.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?

@[simp]

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

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.Tor'_map_app (C : Type u_1) (n : ) (c c' : C) (f : c c') (j : C) :
n).map f).app j =

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

Equations
@[simp]
noncomputable def category_theory.Tor_succ_of_projective (C : Type u_1) (X Y : C) (n : ) :
(n + 1)).obj X).obj Y 0

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

Equations
noncomputable def category_theory.Tor'_succ_of_projective (C : Type u_1) (X Y : C) (n : ) :
(n + 1)).obj X).obj Y 0

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

Equations