isZero_Tor'_succ_of_projective — Mathlib

English

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

Русский

Если X — проективный объект, то высшие группы Тор'(X,Y) нулевые: Tor'^{C}_{n+1}(X,Y)=0.

LaTeX

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

Lean4

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

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