Tor, the left-derived functor of tensor product #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define Tor C n : C ⥤ C ⥤ C, by left-deriving in the second factor of (X, Y) ↦ X ⊗ Y.
For now we have almost nothing to say about it!
It would be good to show that this is naturally isomorphic to the functor obtained
by left-deriving in the first factor, instead.
For now we define Tor' by left-deriving in the first factor,
but showing Tor C n ≅ Tor' C n will require a bit more theory!
Possibly it's best to axiomatize delta functors, and obtain a unique characterisation?
@[simp]
theorem
category_theory.Tor_obj
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(n : ℕ)
(X : C) :
(category_theory.Tor C n).obj X = ((category_theory.monoidal_category.tensoring_left C).obj X).left_derived n
noncomputable
def
category_theory.Tor
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(n : ℕ) :
We define Tor C n : C ⥤ C ⥤ C by left-deriving in the second factor of (X, Y) ↦ X ⊗ Y.
Equations
- category_theory.Tor C n = {obj := λ (X : C), ((category_theory.monoidal_category.tensoring_left C).obj X).left_derived n, map := λ (X Y : C) (f : X ⟶ Y), category_theory.nat_trans.left_derived ((category_theory.monoidal_category.tensoring_left C).map f) n, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.Tor_map
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(n : ℕ)
(X Y : C)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.Tor'_obj_map
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(n : ℕ)
(k j j' : C)
(f : j ⟶ j') :
((category_theory.Tor' C n).obj k).map f = (homotopy_category.homology_functor C (complex_shape.down ℕ) n).map ((homotopy_category.quotient C (complex_shape.down ℕ)).map ((category_theory.nat_trans.map_homological_complex ((category_theory.monoidal_category.tensoring_right C).map f) (complex_shape.down ℕ)).app ((category_theory.projective_resolutions C).obj k).as))
@[simp]
theorem
category_theory.Tor'_map_app
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(n : ℕ)
(c c' : C)
(f : c ⟶ c')
(j : C) :
((category_theory.Tor' C n).map f).app j = ((category_theory.monoidal_category.tensor_right j).left_derived n).map f
noncomputable
def
category_theory.Tor'
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(n : ℕ) :
An alternative definition of Tor, where we left-derive in the first factor instead.
Equations
- category_theory.Tor' C n = {obj := λ (X : C), ((category_theory.monoidal_category.tensoring_right C).obj X).left_derived n, map := λ (X Y : C) (f : X ⟶ Y), category_theory.nat_trans.left_derived ((category_theory.monoidal_category.tensoring_right C).map f) n, map_id' := _, map_comp' := _}.flip
@[simp]
theorem
category_theory.Tor'_obj_obj
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(n : ℕ)
(k j : C) :
((category_theory.Tor' C n).obj k).obj j = ((category_theory.monoidal_category.tensor_right j).left_derived n).obj k
noncomputable
def
category_theory.Tor_succ_of_projective
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(X Y : C)
[category_theory.projective Y]
(n : ℕ) :
((category_theory.Tor C (n + 1)).obj X).obj Y ≅ 0
The higher Tor groups for X and Y are zero if Y is projective.
Equations
noncomputable
def
category_theory.Tor'_succ_of_projective
(C : Type u_1)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_cokernels C]
[category_theory.limits.has_images C]
[category_theory.limits.has_image_maps C]
[category_theory.has_projective_resolutions C]
(X Y : C)
[category_theory.projective X]
(n : ℕ) :
((category_theory.Tor' C (n + 1)).obj X).obj Y ≅ 0
The higher Tor' groups for X and Y are zero if X is projective.