isZero_Tor_succ_of_projective — Mathlib

English

Another articulation of torIso, emphasising left-derived-object isomorphism with a projective resolution.

Русский

Дополнительное формулирование torIso, подчёркивающее левостороннее выводимое изоморфность объекта через проективную резольвенцию.

LaTeX

$$torIso (A) {B} (P) (n) : ((Rep.Tor k G n).obj A).obj B ≅ (P.complex.coinvariantsTensorObj A).homology n$$

Lean4

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

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