CategoryTheory.isZero_Tor_succ_of_projective
theorem CategoryTheory.isZero_Tor_succ_of_projective :
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
[inst_4 : CategoryTheory.HasProjectiveResolutions C] (X Y : C) [inst_5 : CategoryTheory.Projective Y] (n : ℕ),
CategoryTheory.Limits.IsZero (((CategoryTheory.Tor C (n + 1)).obj X).obj Y)
The theorem `CategoryTheory.isZero_Tor_succ_of_projective` states that for any abelian and monoidal preadditive category `C` with projective resolutions, and for any objects `X` and `Y` in `C` where `Y` is projective, the higher Tor groups (of order `n + 1`) between `X` and `Y` are zero. This is a result from homological algebra stating that projective modules have trivial higher Tor groups.
More concisely: In any abelian and monoidal preadditive category with projective resolutions, the higher Tor groups (of order n+1) between any projective object Y and any other object X are zero.
|
CategoryTheory.isZero_Tor'_succ_of_projective
theorem CategoryTheory.isZero_Tor'_succ_of_projective :
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
[inst_4 : CategoryTheory.HasProjectiveResolutions C] (X Y : C) [inst_5 : CategoryTheory.Projective X] (n : ℕ),
CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' C (n + 1)).obj X).obj Y)
This theorem states that for any category `C` which is both monoidal and abelian, and is equipped with projective resolutions, if `X` is a projective object in `C`, then the higher `Tor'` groups for `X` and any other object `Y` in `C` are zero. The `Tor'` groups here refer to a derived functor in the field of homological algebra, and the theorem essentially asserts that projective objects have no higher `Tor'` groups, implying that they do not contribute to the homological invariants of the category.
More concisely: In an abelian, monoidal category `C` with projective resolutions, a projective object `X` has vanishing higher Tor groups Tor^n(X, Y) for all objects Y and all positive integers n.
|