feat(category_theory/monoidal): the definition of Tor (#7512)

# 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.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Author: kim-em

src/category_theory/monoidal/category.lean

@@ -439,13 +439,32 @@ def tensor_right (X : C) : C ⥤ C :=
 
 variables (C)
 
+/--
+Tensoring on the left, as a functor from `C` into endofunctors of `C`.
+
+TODO: show this is a op-monoidal functor.
+-/
+@[simps]
+def tensoring_left : C ⥤ C ⥤ C :=
+{ obj := tensor_left,
+  map := λ X Y f,
+  { app := λ Z, f ⊗ (𝟙 Z) } }
+
+instance : faithful (tensoring_left C) :=
+{ map_injective' := λ X Y f g h,
+  begin
+    injections with h,
+    replace h := congr_fun h (𝟙_ C),
+    simpa using h,
+  end }
+
 /--
 Tensoring on the right, as a functor from `C` into endofunctors of `C`.
 
 We later show this is a monoidal functor.
 -/
 @[simps]
-def tensoring_right : C ⥤ (C ⥤ C) :=
+def tensoring_right : C ⥤ C ⥤ C :=
 { obj := tensor_right,
   map := λ X Y f,
   { app := λ Z, (𝟙 Z) ⊗ f } }

src/category_theory/monoidal/preadditive.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.preadditive.additive_functor
+import category_theory.monoidal.category
+
+/-!
+# Preadditive monoidal categories
+
+A monoidal category is `monoidal_preadditive` if it is preadditive and tensor product of morphisms
+is linear in both factors.
+-/
+
+noncomputable theory
+
+namespace category_theory
+
+open category_theory.limits
+open category_theory.monoidal_category
+
+variables (C : Type*) [category C] [preadditive C] [monoidal_category C]
+
+/--
+A category is `monoidal_preadditive` if tensoring is linear in both factors.
+
+Note we don't `extend preadditive C` here, as `abelian C` already extends it,
+and we'll need to have both typeclasses sometimes.
+-/
+class monoidal_preadditive :=
+(tensor_zero' : ∀ {W X Y Z : C} (f : W ⟶ X), f ⊗ (0 : Y ⟶ Z) = 0 . obviously)
+(zero_tensor' : ∀ {W X Y Z : C} (f : Y ⟶ Z), (0 : W ⟶ X) ⊗ f = 0 . obviously)
+(tensor_add' : ∀ {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h . obviously)
+(add_tensor' : ∀ {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h . obviously)
+
+restate_axiom monoidal_preadditive.tensor_zero'
+restate_axiom monoidal_preadditive.zero_tensor'
+restate_axiom monoidal_preadditive.tensor_add'
+restate_axiom monoidal_preadditive.add_tensor'
+attribute [simp] monoidal_preadditive.tensor_zero monoidal_preadditive.zero_tensor
+
+variables [monoidal_preadditive C]
+
+local attribute [simp] monoidal_preadditive.tensor_add monoidal_preadditive.add_tensor
+
+instance tensoring_left_additive (X : C) : ((tensoring_left C).obj X).additive := {}
+instance tensoring_right_additive (X : C) : ((tensoring_right C).obj X).additive := {}
+
+end category_theory

src/category_theory/monoidal/tor.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.derived
+import category_theory.monoidal.preadditive
+
+/-!
+# 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?
+
+-/
+
+noncomputable theory
+
+open category_theory.limits
+open category_theory.monoidal_category
+
+namespace category_theory
+
+variables {C : Type*} [category C] [monoidal_category C] [preadditive C] [monoidal_preadditive C]
+  [has_zero_object C] [has_equalizers C] [has_cokernels C] [has_images C] [has_image_maps C]
+  [has_projective_resolutions C]
+
+variables (C)
+
+/-- We define `Tor C n : C ⥤ C ⥤ C` by left-deriving in the second factor of `(X, Y) ↦ X ⊗ Y`. -/
+@[simps]
+def Tor (n : ℕ) : C ⥤ C ⥤ C :=
+{ obj := λ X, functor.left_derived ((tensoring_left C).obj X) n,
+  map := λ X Y f, nat_trans.left_derived ((tensoring_left C).map f) n,
+  map_id' := λ X, by rw [(tensoring_left C).map_id, nat_trans.left_derived_id],
+  map_comp' := λ X Y Z f g, by rw [(tensoring_left C).map_comp, nat_trans.left_derived_comp], }
+
+/-- An alternative definition of `Tor`, where we left-derive in the first factor instead. -/
+@[simps]
+def Tor' (n : ℕ) : C ⥤ C ⥤ C :=
+functor.flip
+{ obj := λ X, functor.left_derived ((tensoring_right C).obj X) n,
+  map := λ X Y f, nat_trans.left_derived ((tensoring_right C).map f) n,
+  map_id' := λ X, by rw [(tensoring_right C).map_id, nat_trans.left_derived_id],
+  map_comp' := λ X Y Z f g, by rw [(tensoring_right C).map_comp, nat_trans.left_derived_comp], }
+
+open_locale zero_object
+
+/-- The higher `Tor` groups for `X` and `Y` are zero if `Y` is projective. -/
+def Tor_succ_of_projective (X Y : C) [projective Y] (n : ℕ) : ((Tor C (n + 1)).obj X).obj Y ≅ 0 :=
+((tensoring_left C).obj X).left_derived_obj_projective_succ n Y
+
+/-- The higher `Tor'` groups for `X` and `Y` are zero if `X` is projective. -/
+def Tor'_succ_of_projective (X Y : C) [projective X] (n : ℕ) :
+  ((Tor' C (n + 1)).obj X).obj Y ≅ 0 :=
+-- This unfortunately needs a manual `dsimp`, to avoid a slow unification problem.
+begin
+  dsimp only [Tor', functor.flip],
+  exact ((tensoring_right C).obj Y).left_derived_obj_projective_succ n X
+end
+
+end category_theory