Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-13 18:51 461130bc

View on Github →

feat(category_theory/monoidal): the definition of Tor (#7512)

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.

Estimated changes