isZero_Tor_succ_of_projective — Mathlib

English

The higher Tor groups for X and Y vanish when Y is projective. More precisely, for every X,Y in C and every n ≥ 0, if Y is projective then Tor(C, n+1).obj X .obj Y is the zero object in C.

Русский

Пусть Y является проективным объектом. Тогда все верхние группы Тор(X,Y) нулевые: Tor^{C}_{n+1}(X,Y) = 0 для всех n ≥ 0.

LaTeX

$$$\\text{IsZero}\\big(\\big(\\operatorname{Tor} \\; C (n+1)\\big).obj X\\big).obj Y$, если $Y$ проектен. $\\Rightarrow$ $\\operatorname{Tor}^{C}_{n+1}(X,Y) = 0$.$$

Lean4

/-- The higher `Tor` groups for `X` and `Y` are zero if `Y` is projective. -/
theorem isZero_Tor_succ_of_projective (X Y : C) [Projective Y] (n : ℕ) : IsZero (((Tor C (n + 1)).obj X).obj Y) := by
  apply Functor.isZero_leftDerived_obj_projective_succ

Похожие утверждения