English
The higher Tor groups vanish when the second argument is projective. For all X,Y with Y projective and all n, IsZero((Tor C (n+1)).obj X .obj Y).
Русский
Пусть Y проектен; тогда высшие группы Тор(X,Y) нулевые: IsZero(Tor_{n+1}^C(X,Y)).
LaTeX
$$$\\text{IsZero}\\big(((\\operatorname{Tor} \\, C (n+1)).\\mathrm{obj} X).\\mathrm{obj} Y\\big).$$$
Lean4
/-- If `F` is a monoidal functor out of `Type`, it takes the (n+1)st Cartesian power
of a type to the image of that type, tensored with the image of the nth Cartesian power. -/
noncomputable def mapPi {C : Type*} [Category C] [MonoidalCategory C] (F : Type _ ⥤ C) [F.Monoidal] (n : ℕ)
(β : Type*) : F.obj (Fin (n + 1) → β) ≅ F.obj β ⊗ F.obj (Fin n → β) :=
Functor.mapIso _ (Fin.consEquiv _).symm.toIso ≪≫ (Functor.Monoidal.μIso F β (Fin n → β)).symm
