mathlib3 documentation

category_theory.monoidal.tor

Tor, the left-derived functor of tensor product #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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?