feat: Functor.mapDerivedCategory is a triangulated functor (#14153)

In this PR, it is shown that an exact functor between abelian categories induces a triangulated functor between the corresponding derived categories.

Author: joelriou

Mathlib/Algebra/Homology/DerivedCategory/ExactFunctor.lean

@@ -9,12 +9,9 @@ import Mathlib.Algebra.Homology.DerivedCategory.Basic
 # An exact functor induces a functor on derived categories
 
 In this file, we show that if `F : C₁ ⥤ C₂` is an exact functor between
-abelian categories, then there is an induced functor
+abelian categories, then there is an induced triangulated functor
 `F.mapDerivedCategory : DerivedCategory C₁ ⥤ DerivedCategory C₂`.
 
-## TODO
-* show that `F.mapDerivedCategory` is a triangulated functor
-
 -/
 
 universe w₁ w₂ v₁ v₂ u₁ u₂
@@ -58,4 +55,19 @@ noncomputable instance :
       (F.mapHomotopyCategory _ ⋙ DerivedCategory.Qh) F.mapDerivedCategory :=
   ⟨F.mapDerivedCategoryFactorsh⟩
 
+noncomputable instance : F.mapDerivedCategory.CommShift ℤ :=
+  Functor.commShiftOfLocalization DerivedCategory.Qh
+    (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ)) ℤ
+    (F.mapHomotopyCategory _ ⋙ DerivedCategory.Qh)
+    F.mapDerivedCategory
+
+instance : NatTrans.CommShift F.mapDerivedCategoryFactorsh.hom ℤ :=
+  inferInstanceAs (NatTrans.CommShift (Localization.Lifting.iso
+      DerivedCategory.Qh (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ))
+        (F.mapHomotopyCategory _ ⋙ DerivedCategory.Qh)
+          F.mapDerivedCategory).hom ℤ)
+
+instance : F.mapDerivedCategory.IsTriangulated :=
+  Functor.isTriangulated_of_precomp_iso F.mapDerivedCategoryFactorsh
+
 end CategoryTheory.Functor

Mathlib/CategoryTheory/Localization/Predicate.lean

@@ -387,6 +387,9 @@ instance id : Lifting L W L (𝟭 D) :=
 @[simps]
 instance compLeft (F : D ⥤ E) : Localization.Lifting L W (L ⋙ F) F := ⟨Iso.refl _⟩
 
+@[simp]
+lemma compLeft_iso (F : D ⥤ E) : Localization.Lifting.iso L W (L ⋙ F) F = Iso.refl _ := rfl
+
 /-- Given a localization functor `L : C ⥤ D` for `W : MorphismProperty C`,
 if `F₁' : D ⥤ E` lifts a functor `F₁ : C ⥤ D`, then a functor `F₂'` which
 is isomorphic to `F₁'` also lifts a functor `F₂` that is isomorphic to `F₁`.  -/

Mathlib/CategoryTheory/Shift/Localization.lean

@@ -18,11 +18,12 @@ a shift by `A`, and the localization functor is compatible with the shift.
 
 --/
 
-universe v₁ v₂ u₁ u₂ w
+universe v₁ v₂ v₃ u₁ u₂ u₃ w
 
 namespace CategoryTheory
 
 variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
+  {E : Type u₃} [Category.{v₃} E]
   (L : C ⥤ D) (W : MorphismProperty C) [L.IsLocalization W]
   (A : Type w) [AddMonoid A] [HasShift C A]
 
@@ -110,4 +111,128 @@ noncomputable instance MorphismProperty.commShift_Q' :
 
 attribute [irreducible] HasShift.localization' MorphismProperty.commShift_Q'
 
+section
+
+open Localization
+
+variable (F : C ⥤ E) (F' : D ⥤ E) [Lifting L W F F']
+  [HasShift D A] [HasShift E A] [L.CommShift A] [F.CommShift A]
+
+namespace Functor
+
+namespace commShiftOfLocalization
+
+variable {A}
+
+/-- Auxiliary definition for `Functor.commShiftOfLocalization`. -/
+noncomputable def iso (a : A) :
+    shiftFunctor D a ⋙ F' ≅ F' ⋙ shiftFunctor E a :=
+  Localization.liftNatIso L W (L ⋙ shiftFunctor D a ⋙ F')
+    (L ⋙ F' ⋙ shiftFunctor E a) _ _
+      ((Functor.associator _ _ _).symm ≪≫
+        isoWhiskerRight (L.commShiftIso a).symm F' ≪≫
+        Functor.associator _ _ _ ≪≫
+        isoWhiskerLeft _ (Lifting.iso L W F F') ≪≫
+        F.commShiftIso a ≪≫
+        isoWhiskerRight (Lifting.iso L W F F').symm _ ≪≫ Functor.associator _ _ _)
+
+@[simp, reassoc]
+lemma iso_hom_app (a : A) (X : C) :
+    (commShiftOfLocalization.iso L W F F' a).hom.app (L.obj X) =
+      F'.map ((L.commShiftIso a).inv.app X) ≫
+      (Lifting.iso L W F F').hom.app (X⟦a⟧) ≫
+        (F.commShiftIso a).hom.app X ≫
+          (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X) := by
+  simp [commShiftOfLocalization.iso]
+
+@[simp, reassoc]
+lemma iso_inv_app (a : A) (X : C) :
+    (commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X) =
+        (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
+        (F.commShiftIso a).inv.app X ≫
+      (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫
+      F'.map ((L.commShiftIso a).hom.app X) := by
+  simp [commShiftOfLocalization.iso]
+
+end commShiftOfLocalization
+
+/-- In the context of localization of categories, if a functor
+is induced by a functor which commutes with the shift, then
+this functor commutes with the shift.  -/
+noncomputable def commShiftOfLocalization : F'.CommShift A where
+  iso := commShiftOfLocalization.iso L W F F'
+  zero := by
+    ext1
+    apply natTrans_ext L W
+    intro X
+    dsimp
+    simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_zero,
+      CommShift.isoZero_inv_app, map_comp, CommShift.isoZero_hom_app, Category.assoc,
+      ← NatTrans.naturality_assoc, ← NatTrans.naturality]
+    dsimp
+    simp only [← Functor.map_comp_assoc, ← Functor.map_comp,
+      Iso.inv_hom_id_app, id_obj, map_id, Category.id_comp, Iso.hom_inv_id_app_assoc]
+  add a b := by
+    ext1
+    apply natTrans_ext L W
+    intro X
+    dsimp
+    simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_add,
+      CommShift.isoAdd_inv_app, map_comp, CommShift.isoAdd_hom_app, Category.assoc]
+    congr 1
+    rw [← cancel_epi (F'.map ((shiftFunctor D b).map ((L.commShiftIso a).hom.app X))),
+      ← F'.map_comp_assoc, ← map_comp, Iso.hom_inv_id_app, map_id, map_id, Category.id_comp]
+    conv_lhs =>
+      erw [← NatTrans.naturality_assoc]
+      dsimp
+      rw [← Functor.map_comp_assoc, ← map_comp_assoc, Category.assoc,
+        ← map_comp, Iso.inv_hom_id_app]
+      dsimp
+      rw [map_id, Category.comp_id, ← NatTrans.naturality]
+      dsimp
+    conv_rhs =>
+      erw [← NatTrans.naturality_assoc]
+      dsimp
+      rw [← Functor.map_comp_assoc, ← map_comp, Iso.hom_inv_id_app]
+      dsimp
+      rw [map_id, map_id, Category.id_comp, commShiftOfLocalization.iso_hom_app,
+        Category.assoc, Category.assoc, Category.assoc, ← map_comp_assoc,
+        Iso.inv_hom_id_app, map_id, Category.id_comp]
+
+variable {A}
+
+lemma commShiftOfLocalization_iso_hom_app (a : A) (X : C) :
+    letI := Functor.commShiftOfLocalization L W A F F'
+    (F'.commShiftIso a).hom.app (L.obj X) =
+      F'.map ((L.commShiftIso a).inv.app X) ≫ (Lifting.iso L W F F').hom.app (X⟦a⟧) ≫
+        (F.commShiftIso a).hom.app X ≫
+          (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X) := by
+  apply commShiftOfLocalization.iso_hom_app
+
+lemma commShiftOfLocalization_iso_inv_app (a : A) (X : C) :
+    letI := Functor.commShiftOfLocalization L W A F F'
+    (F'.commShiftIso a).inv.app (L.obj X) =
+      (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
+      (F.commShiftIso a).inv.app X ≫ (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫
+     F'.map ((L.commShiftIso a).hom.app X) := by
+  apply commShiftOfLocalization.iso_inv_app
+
+end Functor
+
+instance NatTrans.commShift_iso_hom_of_localization :
+    letI := Functor.commShiftOfLocalization L W A F F'
+    NatTrans.CommShift (Lifting.iso L W F F').hom A := by
+  letI := Functor.commShiftOfLocalization L W A F F'
+  constructor
+  intro a
+  ext X
+  simp only [comp_app, whiskerRight_app, whiskerLeft_app,
+    Functor.commShiftIso_comp_hom_app,
+    Functor.commShiftOfLocalization_iso_hom_app,
+    Category.assoc, ← Functor.map_comp, ← Functor.map_comp_assoc,
+    Iso.hom_inv_id_app, Functor.map_id, Iso.inv_hom_id_app,
+    Category.comp_id, Category.id_comp, Functor.comp_obj]
+
+end
+
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Functor.lean

@@ -113,6 +113,13 @@ noncomputable def mapTriangleInvRotateIso [F.Additive] :
     (fun T => Triangle.isoMk _ _ ((F.commShiftIso (-1 : ℤ)).symm.app _) (Iso.refl _) (Iso.refl _)
       (by aesop_cat) (by aesop_cat) (by aesop_cat)) (by aesop_cat)
 
+
+variable (C) in
+/-- The canonical isomorphism `(𝟭 C).mapTriangle ≅ 𝟭 (Triangle C)`. -/
+@[simps!]
+def mapTriangleIdIso : (𝟭 C).mapTriangle ≅ 𝟭 _ :=
+  NatIso.ofComponents (fun T ↦ Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _))
+
 /-- The canonical isomorphism `(F ⋙ G).mapTriangle ≅ F.mapTriangle ⋙ G.mapTriangle`. -/
 @[simps!]
 def mapTriangleCompIso : (F ⋙ G).mapTriangle ≅ F.mapTriangle ⋙ G.mapTriangle :=
@@ -132,9 +139,11 @@ def mapTriangleIso {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ
 
 end Additive
 
-variable [HasZeroObject C] [HasZeroObject D] [Preadditive C] [Preadditive D]
+variable [HasZeroObject C] [HasZeroObject D] [HasZeroObject E]
+  [Preadditive C] [Preadditive D] [Preadditive E]
   [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive]
-  [Pretriangulated C] [Pretriangulated D]
+  [∀ (n : ℤ), (shiftFunctor E n).Additive]
+  [Pretriangulated C] [Pretriangulated D] [Pretriangulated E]
 
 /-- A functor which commutes with the shift by `ℤ` is triangulated if
 it sends distinguished triangles to distinguished triangles. -/
@@ -149,9 +158,7 @@ namespace IsTriangulated
 
 open ZeroObject
 
-variable [F.IsTriangulated]
-
-instance (priority := 100) : PreservesZeroMorphisms F where
+instance (priority := 100) [F.IsTriangulated] : PreservesZeroMorphisms F where
   map_zero X Y := by
     have h₁ : (0 : X ⟶ Y) = 0 ≫ 𝟙 0 ≫ 0 := by simp
     have h₂ : 𝟙 (F.obj 0) = 0 := by
@@ -162,7 +169,8 @@ instance (priority := 100) : PreservesZeroMorphisms F where
       infer_instance
     rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
 
-noncomputable instance : PreservesLimitsOfShape (Discrete WalkingPair) F := by
+noncomputable instance [F.IsTriangulated] :
+    PreservesLimitsOfShape (Discrete WalkingPair) F := by
   suffices ∀ (X₁ X₃ : C), IsIso (prodComparison F X₁ X₃) by
     have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.ofIsoProdComparison F X₁ X₃
     exact ⟨fun {K} ↦ preservesLimitOfIsoDiagram F (diagramIsoPair K).symm⟩
@@ -187,10 +195,59 @@ noncomputable instance : PreservesLimitsOfShape (Discrete WalkingPair) F := by
     (binaryProductTriangle_distinguished _ _)
     (by dsimp; infer_instance) (by dsimp; infer_instance)
 
-instance (priority := 100) : F.Additive := F.additive_of_preserves_binary_products
+instance (priority := 100) [F.IsTriangulated] : F.Additive :=
+  F.additive_of_preserves_binary_products
+
+instance : (𝟭 C).IsTriangulated where
+  map_distinguished T hT :=
+    isomorphic_distinguished _ hT _ ((mapTriangleIdIso C).app T)
+
+instance [F.IsTriangulated] [G.IsTriangulated] : (F ⋙ G).IsTriangulated where
+  map_distinguished T hT :=
+    isomorphic_distinguished _ (G.map_distinguished _ (F.map_distinguished T hT)) _
+      ((mapTriangleCompIso F G).app T)
 
 end IsTriangulated
 
+lemma isTriangulated_of_iso {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ]
+    [NatTrans.CommShift e.hom ℤ] [F₁.IsTriangulated] : F₂.IsTriangulated where
+  map_distinguished T hT :=
+    isomorphic_distinguished _ (F₁.map_distinguished T hT) _ ((mapTriangleIso e).app T).symm
+
+lemma isTriangulated_iff_of_iso {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) [F₁.CommShift ℤ] [F₂.CommShift ℤ]
+    [NatTrans.CommShift e.hom ℤ] : F₁.IsTriangulated ↔ F₂.IsTriangulated := by
+  constructor
+  · intro
+    exact isTriangulated_of_iso e
+  · intro
+    have : NatTrans.CommShift e.symm.hom ℤ := inferInstanceAs (NatTrans.CommShift e.inv ℤ)
+    exact isTriangulated_of_iso e.symm
+
+lemma mem_mapTriangle_essImage_of_distinguished
+    [F.IsTriangulated] [F.mapArrow.EssSurj] (T : Triangle D) (hT : T ∈ distTriang D) :
+    ∃ (T' : Triangle C) (_ : T' ∈ distTriang C), Nonempty (F.mapTriangle.obj T' ≅ T) := by
+  obtain ⟨X, Y, f, e₁, e₂, w⟩ : ∃ (X Y : C) (f : X ⟶ Y) (e₁ : F.obj X ≅ T.obj₁)
+    (e₂ : F.obj Y ≅ T.obj₂), F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁ := by
+      let e := F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
+      exact ⟨_, _, _, Arrow.leftFunc.mapIso e, Arrow.rightFunc.mapIso e, e.hom.w.symm⟩
+  obtain ⟨W, g, h, H⟩ := distinguished_cocone_triangle f
+  exact ⟨_, H, ⟨isoTriangleOfIso₁₂ _ _ (F.map_distinguished _ H) hT e₁ e₂ w⟩⟩
+
+lemma isTriangulated_of_precomp
+    [(F ⋙ G).IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] :
+    G.IsTriangulated where
+  map_distinguished T hT := by
+    obtain ⟨T', hT', ⟨e⟩⟩ := F.mem_mapTriangle_essImage_of_distinguished T hT
+    exact isomorphic_distinguished _ ((F ⋙ G).map_distinguished T' hT') _
+      (G.mapTriangle.mapIso e.symm ≪≫ (mapTriangleCompIso F G).symm.app _)
+
+variable {F G} in
+lemma isTriangulated_of_precomp_iso {H : C ⥤ E} (e : F ⋙ G ≅ H) [H.CommShift ℤ]
+    [H.IsTriangulated] [F.IsTriangulated] [F.mapArrow.EssSurj] [NatTrans.CommShift e.hom ℤ] :
+    G.IsTriangulated := by
+  have := (isTriangulated_iff_of_iso e).2 inferInstance
+  exact isTriangulated_of_precomp F G
+
 end Functor
 
 variable {C D : Type*} [Category C] [Category D] [HasShift C ℤ] [HasShift D ℤ]