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?

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

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

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.

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
def CategoryTheory.torSuccOfProjective (C : Type u_1) [] (X : C) (Y : C) (n : ) :
((CategoryTheory.Tor C (n + 1)).obj X).obj Y 0

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

Instances For
def CategoryTheory.tor'SuccOfProjective (C : Type u_1) [] (X : C) (Y : C) (n : ) :
((CategoryTheory.Tor' C (n + 1)).obj X).obj Y 0

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

Instances For