English
For an abelian monoidal category C with projective resolutions, and for every n ≥ 0, define the endofunctor Tor(C,n) on C by taking the nth left-derived functor in the second variable of the bifunctor (X,Y) ↦ X ⊗ Y. Concretely, for each object X, Tor(C,n).obj X is the nth left-derived functor of the functor Y ↦ X ⊗ Y, and for each morphism f : X → X' the induced natural transformation is given by the left-derived map of tensoringLeft by f.
Русский
Для абелевой монодной категории C, удовлетворяющей условиям проективных резолюций, для каждого n ≥ 0 задаётся эндофунктор Tor(C,n) на C, который получается как левый производный по второй переменной от двоичного тензорирования (X,Y) ↦ X ⊗ Y. То есть для каждого X существует Тор_n(X) = L_n(Y ↦ X ⊗ Y), а для стрелки f: X → X' получаем соответствующее натуральное отображение.
LaTeX
$$$Tor(n) : C \\to (C \\to C), \\\\ Tor(n).obj X = \\mathbb{L}_n\\big(Y \\mapsto X \\otimes Y\\big), \\\\ Tor(n).map f = \\mathbb{L}_n\\big((\\mathrm{tensoringLeft}\\, C).\\mathrm{map} f\\big).$$$
Lean4
/-- We define `Tor C n : C ⥤ C ⥤ C` by left-deriving in the second factor of `(X, Y) ↦ X ⊗ Y`. -/
@[simps]
def Tor (n : ℕ) : C ⥤ C ⥤ C where
obj X := Functor.leftDerived ((tensoringLeft C).obj X) n
map f := NatTrans.leftDerived ((tensoringLeft C).map f) n
