English
An alternative definition of Tor where the left-derived functor is taken in the first factor. Precisely, Tor'(n) is defined by flipping the order of the factors and deriving with respect to the first factor: Tor'(n) = (Functor.flip { obj := X ↦ LeftDerived ((tensoringRight C).obj X) n; map := f ↦ NatTrans.leftDerived ((tensoringRight C).map f) n }).
Русский
Альтернативное определение Тор: левый производный по первой переменной. Точно: Tor'(n) задаётся через разворот факторов и левый вывод по первой переменной: Tor'(n) = (Functor.flip {...}).
LaTeX
$$$Tor'(n) : C \\to C \\to C \\\\ Tor'(n) = \\mathrm{Functor.flip}\\left\\{\\mathrm{obj}\\;X \\mapsto \\mathbb{L}_n\\big( Y \\mapsto X \\otimes Y \\big), \\\\ \\mathrm{map}\\;f \\mapsto \\mathbb{L}_n\\big((\\mathrm{tensoringRight}\\, C).\\mathrm{map} f\\big)\\right\\}.$$$
Lean4
/-- An alternative definition of `Tor`, where we left-derive in the first factor instead. -/
@[simps! obj_obj map_app obj_map]
def Tor' (n : ℕ) : C ⥤ C ⥤ C :=
Functor.flip
{ obj := fun X => Functor.leftDerived ((tensoringRight C).obj X) n
map := fun f => NatTrans.leftDerived ((tensoringRight C).map f) n }
