Tor from a projective presentation of length one

Mathlib's CategoryTheory.Tor C n derives the tensor product in its second variable: ((Tor C n).obj X).obj M is Lₙ(X ⊗ -)(M). Let S : 0 ⟶ P₁ ⟶ P₀ ⟶ M ⟶ 0 be a short exact sequence with P₁ and P₀ projective. Then

• Tor₁(X, M) is the kernel of X ◁ S.f : X ⊗ P₁ ⟶ X ⊗ P₀ (CategoryTheory.ShortComplex.ShortExact.torOneIsoKernel), naturally in X and in maps of such presentations, sending the homology class of a cycle of X ⊗ - applied to the resolution to that cycle;
• Torₙ(X, M) vanishes for n ≥ 2 (CategoryTheory.ShortComplex.ShortExact.isZero_Tor_add_two).

Over a principal ideal domain the boundaries and cycles of a complex of free modules are free, so the homology Hⱼ has the presentation 0 ⟶ Bⱼ ⟶ Zⱼ ⟶ Hⱼ ⟶ 0. This identifies the Tor₁ terms of the Künneth short exact sequence 0 ⟶ ⨁ Hᵢ ⊗ Hⱼ ⟶ Hₙ(K ⊗ L) ⟶ ⨁ Tor₁(Hᵢ, Hⱼ) ⟶ 0 with the kernels of Hᵢ(K) ⊗ Bⱼ(L) ⟶ Hᵢ(K) ⊗ Zⱼ(L).

These are the specializations to X ⊗ - of the computation of left derived functors in TauCeti.CategoryTheory.Abelian.LeftDerived.

If e • 𝟙 X = 0 for a natural number e, then e kills every Torₙ(X, Y) (CategoryTheory.nsmul_id_Tor_eq_zero): the objects killed by e (CategoryTheory.ObjectProperty.isKilledBy) are closed under subobjects and quotients and contain every X ⊗ P.

For Mathlib's CategoryTheory.Tor' C n, which derives the first variable instead, ((Tor' C n).obj X).obj Y is Lₙ(- ⊗ Y)(X). The file records two facts about it in the underived variable Y: it is an additive functor of Y, and Tor'ₙ₊₁(X, 𝟙_ C) vanishes (CategoryTheory.isZero_Tor'_succ_tensorUnit), since - ⊗ 𝟙_ C is isomorphic to the identity functor and hence exact.

References

• C. A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Sections 2.4 and 3.1, and Theorem 3.6.3 for the Künneth formula.

noncomputable def CategoryTheory.ShortComplex.ShortExact.torOneIsoKernel {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] (X : C) : ((Tor C 1).obj X).obj S.X₃ ≅ Limits.kernel (MonoidalCategoryStruct.whiskerLeft X S.f)

For a projective presentation 0 ⟶ P₁ ⟶ P₀ ⟶ M ⟶ 0, Tor₁(X, M) is the kernel of X ◁ S.f : X ⊗ P₁ ⟶ X ⊗ P₀.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.homologyπ_comp_isoLeftDerivedObj_inv_comp_torOneIsoKernel_hom_comp_ι {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] (X : C) : CategoryStruct.comp (((((MonoidalCategory.tensoringLeft C).obj X).mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).homologyπ 1) (CategoryStruct.comp (hS.projectiveResolution.isoLeftDerivedObj ((MonoidalCategory.tensoringLeft C).obj X) 1).inv (CategoryStruct.comp (hS.torOneIsoKernel X).hom (Limits.kernel.ι (MonoidalCategoryStruct.whiskerLeft X S.f)))) = ((((MonoidalCategory.tensoringLeft C).obj X).mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).iCycles 1

The identification of Tor₁(X, M) with the kernel of X ◁ S.f sends the homology class of a cycle of X ⊗ - applied to the resolution to that cycle.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.homologyπ_comp_isoLeftDerivedObj_inv_comp_torOneIsoKernel_hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] (X : C) {Z : C} (h : MonoidalCategoryStruct.tensorObj X S.X₁ ⟶ Z) : CategoryStruct.comp (((((MonoidalCategory.tensoringLeft C).obj X).mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).homologyπ 1) (CategoryStruct.comp (CategoryStruct.comp (hS.projectiveResolution.isoLeftDerivedObj ((MonoidalCategory.tensoringLeft C).obj X) 1).inv (CategoryStruct.comp (hS.torOneIsoKernel X).hom (Limits.kernel.ι (MonoidalCategoryStruct.whiskerLeft X S.f)))) h) = CategoryStruct.comp (((((MonoidalCategory.tensoringLeft C).obj X).mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).iCycles 1) h

The identification of Tor₁(X, M) with the kernel of X ◁ S.f sends the homology class of a cycle of X ⊗ - applied to the resolution to that cycle.

theorem CategoryTheory.ShortComplex.ShortExact.isZero_Tor_add_two {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] (X : C) (n : ℕ) : Limits.IsZero (((Tor C (n + 2)).obj X).obj S.X₃)

Torₙ(X, M) vanishes for n ≥ 2 when M has a projective presentation of length one.

theorem CategoryTheory.ShortComplex.ShortExact.Tor_map_app_comp_torOneIsoKernel_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (((Tor C 1).map f).app S.X₃) (hS.torOneIsoKernel Y).hom = CategoryStruct.comp (hS.torOneIsoKernel X).hom (Limits.kernel.map (MonoidalCategoryStruct.whiskerLeft X S.f) (MonoidalCategoryStruct.whiskerLeft Y S.f) (MonoidalCategoryStruct.whiskerRight f S.X₁) (MonoidalCategoryStruct.whiskerRight f S.X₂) ⋯)

The identification of Tor₁(X, M) with the kernel of X ◁ S.f is natural in X.

theorem CategoryTheory.ShortComplex.ShortExact.Tor_map_app_comp_torOneIsoKernel_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Limits.kernel (MonoidalCategoryStruct.whiskerLeft Y S.f) ⟶ Z) : CategoryStruct.comp (((Tor C 1).map f).app S.X₃) (CategoryStruct.comp (hS.torOneIsoKernel Y).hom h) = CategoryStruct.comp (hS.torOneIsoKernel X).hom (CategoryStruct.comp (Limits.kernel.map (MonoidalCategoryStruct.whiskerLeft X S.f) (MonoidalCategoryStruct.whiskerLeft Y S.f) (MonoidalCategoryStruct.whiskerRight f S.X₁) (MonoidalCategoryStruct.whiskerRight f S.X₂) ⋯) h)

The identification of Tor₁(X, M) with the kernel of X ◁ S.f is natural in X.

theorem CategoryTheory.ShortComplex.ShortExact.Tor_obj_map_comp_torOneIsoKernel_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S S' : ShortComplex C} {hS : S.ShortExact} [Projective S.X₁] [Projective S.X₂] (hS' : S'.ShortExact) [Projective S'.X₁] [Projective S'.X₂] (X : C) (φ : S ⟶ S') : CategoryStruct.comp (((Tor C 1).obj X).map φ.τ₃) (hS'.torOneIsoKernel X).hom = CategoryStruct.comp (hS.torOneIsoKernel X).hom (Limits.kernel.map (MonoidalCategoryStruct.whiskerLeft X S.f) (MonoidalCategoryStruct.whiskerLeft X S'.f) (MonoidalCategoryStruct.whiskerLeft X φ.τ₁) (MonoidalCategoryStruct.whiskerLeft X φ.τ₂) ⋯)

The identification of Tor₁(X, M) with the kernel of X ◁ S.f is natural in maps of projective presentations.

theorem CategoryTheory.ShortComplex.ShortExact.Tor_obj_map_comp_torOneIsoKernel_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {S S' : ShortComplex C} {hS : S.ShortExact} [Projective S.X₁] [Projective S.X₂] (hS' : S'.ShortExact) [Projective S'.X₁] [Projective S'.X₂] (X : C) (φ : S ⟶ S') {Z : C} (h : Limits.kernel (MonoidalCategoryStruct.whiskerLeft X S'.f) ⟶ Z) : CategoryStruct.comp (((Tor C 1).obj X).map φ.τ₃) (CategoryStruct.comp (hS'.torOneIsoKernel X).hom h) = CategoryStruct.comp (hS.torOneIsoKernel X).hom (CategoryStruct.comp (Limits.kernel.map (MonoidalCategoryStruct.whiskerLeft X S.f) (MonoidalCategoryStruct.whiskerLeft X S'.f) (MonoidalCategoryStruct.whiskerLeft X φ.τ₁) (MonoidalCategoryStruct.whiskerLeft X φ.τ₂) ⋯) h)

The identification of Tor₁(X, M) with the kernel of X ◁ S.f is natural in maps of projective presentations.

theorem CategoryTheory.nsmul_id_Tor_eq_zero {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] {X : C} {e : ℕ} (hX : e • CategoryStruct.id X = 0) (Y : C) (n : ℕ) : e • CategoryStruct.id (((Tor C n).obj X).obj Y) = 0

If a natural number e kills X, in the sense that e • 𝟙 X = 0, then it kills every Torₙ(X, Y).

instance CategoryTheory.instAdditiveObjFunctorTor'_tauCeti {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (X : C) (n : ℕ) : ((Tor' C n).obj X).Additive

Tor' is additive in its second variable, the one that is not derived.

theorem CategoryTheory.isZero_Tor'_succ_tensorUnit {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Abelian C] [MonoidalPreadditive C] [HasProjectiveResolutions C] (X : C) (n : ℕ) : Limits.IsZero (((Tor' C (n + 1)).obj X).obj (MonoidalCategoryStruct.tensorUnit C))

The higher Tor' groups with the tensor unit as second variable vanish: - ⊗ 𝟙_ C is isomorphic to the identity functor, so it is exact.