Tor, the left-derived functor of tensor product #
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?
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' := _}
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
The higher Tor
groups for X
and Y
are zero if Y
is projective.
Equations
The higher Tor'
groups for X
and Y
are zero if X
is projective.