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?

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

    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