feat(Algebra/Homology): the functor F.rightDerivedFunctorPlus is triangulated

Mathlib.lean

@@ -591,6 +591,7 @@ public import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.MapAdjunction
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
 public import Mathlib.Algebra.Homology.DerivedCategory.Fractions
@@ -3115,8 +3116,10 @@ public import Mathlib.CategoryTheory.Localization.Construction
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
+public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.DerivesTriangulated
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
+public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseLeftDerived
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
 public import Mathlib.CategoryTheory.Localization.Equivalence
 public import Mathlib.CategoryTheory.Localization.FiniteProducts

Mathlib/Algebra/Homology/CochainComplexPlus.lean

@@ -107,6 +107,9 @@ below cochain complexes. -/
 def quasiIso [CategoryWithHomology C] : MorphismProperty (Plus C) :=
   (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).inverseImage (ι C)
 
+lemma quasiIso_iff [CategoryWithHomology C] {X Y : Plus C} (f : X ⟶ Y) :
+    quasiIso C f ↔ QuasiIso f.hom := Iff.rfl
+
 instance [CategoryWithHomology C] : (quasiIso C).HasTwoOutOfThreeProperty := by
   dsimp [quasiIso]
   infer_instance
@@ -135,10 +138,9 @@ section
 
 variable [HasZeroMorphisms C] [HasZeroMorphisms D] [F.PreservesZeroMorphisms]
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The functor on categories of bounded below cochain complexes that
 is induced by a functor (which preserves zero morphisms). -/
-@[simps!]
+@[implicit_reducible, simps!]
 def mapCochainComplexPlus : CochainComplex.Plus C ⥤ CochainComplex.Plus D :=
   ObjectProperty.lift _ (CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex _) (fun K => by
     obtain ⟨i, hi⟩ := K.2
@@ -149,13 +151,25 @@ def mapCochainComplexPlus : CochainComplex.Plus C ⥤ CochainComplex.Plus D :=
 /-- The isomorphism between `F.mapCochainComplexPlus ⋙ CochainComplex.Plus.ι D`
 and `CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex _` when `F : C ⥤ D`
 is a functor which preserves zero morphisms -/
-@[simps!]
+@[simps! hom_app inv_app]
 def mapCochainComplexPlusCompι :
     F.mapCochainComplexPlus ⋙ CochainComplex.Plus.ι D ≅
       CochainComplex.Plus.ι C ⋙ F.mapHomologicalComplex _ := Iso.refl _
 
 end
 
+section
+
+variable [Preadditive C] [Preadditive D] [F.Additive]
+
+noncomputable instance : F.mapCochainComplexPlus.CommShift ℤ :=
+  ObjectProperty.commShiftLift ..
+
+instance : NatTrans.CommShift F.mapCochainComplexPlusCompι.hom ℤ :=
+  ObjectProperty.commShift_liftCompιIso_hom ..
+
+end
+
 end Functor
 
 end CategoryTheory

Mathlib/Algebra/Homology/DerivedCategory/DerivabilityStructureInjectives.lean

@@ -101,7 +101,7 @@ variable (C) in
 /-- The localizer morphism (relative to quasi-isomorphisms) that is
 given by the "inclusion functor"
 `CochainComplex.Plus (InjectiveObject C) ⥤ CochainComplex.Plus C`. -/
-@[simps]
+@[implicit_reducible, simps]
 def localizerMorphism :
     LocalizerMorphism ((quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus)
       (quasiIso C) where

Mathlib/Algebra/Homology/DerivedCategory/Ext/MapAdjunction.lean

@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
+
+/-!
+# Adjunctions between exact functors and Ext-groups
+
+Assume that `adj : F ⊣ G` is an adjunction between two exact
+functors `F : C ⥤ D` and `G : D ⥤ C` between abelian categories.
+In this file, we promote the bijection
+`adj.homEquiv X Y : (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)` into
+additive equivalences
+`adj.extEquiv : Ext (F.obj X) Y n ≃+ Ext X (G.obj Y) n`.
+
+-/
+
+@[expose] public section
+
+universe w₁ w₂
+
+namespace CategoryTheory
+
+open Abelian Limits
+
+variable {C D : Type*} [Category* C] [Category* D] [Abelian C] [Abelian D]
+  [HasExt.{w₁} C] [HasExt.{w₂} D]
+  {F : C ⥤ D} {G : D ⥤ C} [F.Additive] [G.Additive]
+  [PreservesFiniteLimits F] [PreservesFiniteColimits F]
+  [PreservesFiniteLimits G] [PreservesFiniteColimits G]
+
+namespace Adjunction
+
+/-- The bijection of `Ext`-groups that is induced by an adjunction
+between exact functors. -/
+@[simps -isSimp apply symm_apply]
+noncomputable def extEquiv (adj : F ⊣ G) {X : C} {Y : D} {n : ℕ} :
+    Ext (F.obj X) Y n ≃+ Ext X (G.obj Y) n where
+  toFun e := (Ext.mk₀ (adj.unit.app X)).comp (e.mapExactFunctor G) (zero_add n)
+  invFun e := (e.mapExactFunctor F).comp (Ext.mk₀ (adj.counit.app Y)) (add_zero n)
+  left_inv e := by
+    dsimp
+    rw [Ext.mapExactFunctor_comp, Ext.comp_assoc _ _ _ _ (add_zero n) (by lia),
+      ← Ext.comp_mapExactFunctor, Ext.mapExactFunctor_comp_mk₀_natTransApp,
+      Ext.id_mapExactFunctor, Ext.mapExactFunctor_mk₀,
+      ← Ext.comp_assoc _ _ _ (zero_add 0) (by lia) (by lia),
+      Ext.mk₀_comp_mk₀, adj.left_triangle_components, Ext.mk₀_id_comp]
+  right_inv e := by
+    dsimp
+    rw [Ext.mapExactFunctor_comp, ← Ext.comp_assoc _ _ _ (zero_add n) (by lia) (by lia),
+      ← Ext.comp_mapExactFunctor, ← Ext.mapExactFunctor_comp_mk₀_natTransApp,
+      Ext.id_mapExactFunctor, Ext.comp_assoc _ _ _ _ (add_zero 0) (by lia),
+      Ext.mapExactFunctor_mk₀, Ext.mk₀_comp_mk₀, adj.right_triangle_components]
+    simp
+  map_add' := by simp
+
+@[simp]
+lemma extEquiv_mk₀ (adj : F ⊣ G) {X : C} {Y : D} (f : F.obj X ⟶ Y) :
+    adj.extEquiv (Ext.mk₀ f) = Ext.mk₀ (adj.homEquiv _ _ f) := by
+  simp [extEquiv_apply, Ext.mapExactFunctor_mk₀, homEquiv_unit]
+
+lemma extEquiv_symm_mk₀ (adj : F ⊣ G) {X : C} {Y : D} (f : X ⟶ G.obj Y) :
+    adj.extEquiv.symm (Ext.mk₀ f) = Ext.mk₀ ((adj.homEquiv _ _).symm f) :=
+  adj.extEquiv.injective (by simp [extEquiv_mk₀])
+
+@[simp]
+lemma extEquiv_symm_mk₀_unit_app (adj : F ⊣ G) (X : C) :
+    dsimp% adj.extEquiv.symm (Ext.mk₀ (adj.unit.app X)) = Ext.mk₀ (𝟙 (F.obj X)) := by
+  simp [extEquiv_symm_mk₀]
+
+@[simp high]
+lemma extEquiv_mk₀_counit_app (adj : F ⊣ G) (Y : D) :
+    dsimp% adj.extEquiv (Ext.mk₀ (adj.counit.app Y)) = Ext.mk₀ (𝟙 (G.obj Y)) := by
+  simp [extEquiv_mk₀, homEquiv_unit]
+
+lemma extEquiv_naturality_left (adj : F ⊣ G) {X₁ X₂ : C} {Y : D} {a b : ℕ}
+    (e : Ext X₁ X₂ a) (e' : Ext (F.obj X₂) Y b) {c : ℕ} (h : a + b = c) :
+    adj.extEquiv ((e.mapExactFunctor F).comp e' h) =
+      e.comp (adj.extEquiv e') h := by
+  rw [extEquiv_apply, extEquiv_apply, Ext.mapExactFunctor_comp,
+    ← Ext.comp_mapExactFunctor,
+    ← Ext.comp_assoc _ _ _ (zero_add a) (by lia) (by lia),
+    ← Ext.mapExactFunctor_comp_mk₀_natTransApp]
+  simp
+
+lemma extEquiv_naturality_left₀ (adj : F ⊣ G) {X₁ X₂ : C} {Y : D}
+    (f : X₁ ⟶ X₂) {n : ℕ} (e : Ext (F.obj X₂) Y n) :
+    adj.extEquiv ((Ext.mk₀ (F.map f)).comp e (zero_add n)) =
+      (Ext.mk₀ f).comp (adj.extEquiv e) (zero_add n) := by
+  simpa [Ext.mapExactFunctor_mk₀] using
+    adj.extEquiv_naturality_left (Ext.mk₀ f) e (zero_add n)
+
+lemma extEquiv_naturality_right (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {a b : ℕ}
+    (e : Ext (F.obj X) Y₁ a) (e' : Ext Y₁ Y₂ b) {c : ℕ} (h : a + b = c) :
+    adj.extEquiv (e.comp e' h) = (adj.extEquiv e).comp (e'.mapExactFunctor G) h := by
+  rw [extEquiv_apply, extEquiv_apply, Ext.mapExactFunctor_comp,
+    Ext.comp_assoc _ _ _ (zero_add a) h (by lia)]
+
+lemma extEquiv_naturality_right₀ (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {n : ℕ}
+    (e : Ext (F.obj X) Y₁ n) (f : Y₁ ⟶ Y₂) :
+    adj.extEquiv (e.comp (Ext.mk₀ f) (add_zero n)) =
+      (adj.extEquiv e).comp (Ext.mk₀ (G.map f)) (add_zero n) := by
+  simpa [Ext.mapExactFunctor_mk₀] using
+    adj.extEquiv_naturality_right e (Ext.mk₀ f) (add_zero n)
+
+lemma extEquiv_symm_naturality_left (adj : F ⊣ G) {X₁ X₂ : C} {Y : D} {a b : ℕ}
+    (e : Ext X₁ X₂ a) (e' : Ext X₂ (G.obj Y) b) {c : ℕ} (h : a + b = c) :
+    adj.extEquiv.symm (e.comp e' h) =
+      (e.mapExactFunctor F).comp (adj.extEquiv.symm e') h :=
+  adj.extEquiv.injective (by simp [extEquiv_naturality_left])
+
+lemma extEquiv_symm_naturality_left₀ (adj : F ⊣ G) {X₁ X₂ : C} {Y : D} {n : ℕ}
+    (f : X₁ ⟶ X₂) (e : Ext X₂ (G.obj Y) n) :
+    adj.extEquiv.symm ((Ext.mk₀ f).comp e (zero_add n)) =
+      (Ext.mk₀ (F.map f)).comp (adj.extEquiv.symm e) (zero_add n) := by
+  simpa [Ext.mapExactFunctor_mk₀] using
+    adj.extEquiv_symm_naturality_left (Ext.mk₀ f) e (zero_add n)
+
+lemma extEquiv_symm_naturality_right (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {a b : ℕ}
+    (e : Ext X (G.obj Y₁) a) (e' : Ext Y₁ Y₂ b) {c : ℕ} (h : a + b = c) :
+    adj.extEquiv.symm (e.comp (e'.mapExactFunctor G) h) =
+    (adj.extEquiv.symm e).comp e' h :=
+  adj.extEquiv.injective (by simp [extEquiv_naturality_right])
+
+lemma extEquiv_symm_naturality_right₀ (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {n : ℕ}
+    (e : Ext X (G.obj Y₁) n) (f : Y₁ ⟶ Y₂) :
+    adj.extEquiv.symm (e.comp (Ext.mk₀ (G.map f)) (add_zero n)) =
+    (adj.extEquiv.symm e).comp (Ext.mk₀ f) (add_zero n) := by
+  simpa [Ext.mapExactFunctor_mk₀] using
+    adj.extEquiv_symm_naturality_right e (Ext.mk₀ f) (add_zero n)
+
+/-- The linear equivalence on `Ext`-modules that is induced by an adjunction
+between exact linear functors. -/
+noncomputable abbrev extLinearEquiv (adj : F ⊣ G) (R : Type*) [Ring R] [Linear R C] [Linear R D]
+    [Functor.Linear R G]
+    {X : C} {Y : D} {n : ℕ} :
+    Ext (F.obj X) Y n ≃ₗ[R] Ext X (G.obj Y) n where
+  toAddEquiv := adj.extEquiv
+  map_smul' := by simp [extEquiv_apply]
+
+end Adjunction
+
+end CategoryTheory

Mathlib/Algebra/Homology/DerivedCategory/Plus.lean

@@ -59,16 +59,16 @@ variable [HasDerivedCategory C]
 namespace Plus
 
 /-- The localization functor `HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C`. -/
+@[implicit_reducible]
 noncomputable def Qh : HomotopyCategory.Plus C ⥤ Plus C :=
   t.plus.lift (HomotopyCategory.Plus.ι _ ⋙ DerivedCategory.Qh) (by
     rintro ⟨K, hK⟩
     obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
     obtain ⟨n, _⟩ := (HomotopyCategory.plus_quotient_obj_iff _).mp hK
     exact ⟨n, t.isGE_of_iso ((quotientCompQhIso C).symm.app K) n⟩)
 
-noncomputable instance : (Qh : _ ⥤ Plus C).CommShift ℤ := by
-  dsimp only [Qh]
-  infer_instance
+noncomputable instance : (Qh : _ ⥤ Plus C).CommShift ℤ :=
+  ObjectProperty.commShiftLift ..
 
 instance : (Qh : _ ⥤ Plus C).IsTriangulated := by
   dsimp only [Qh]
@@ -104,9 +104,13 @@ variable (C)
 
 /-- The functor `DerivedCategory.Plus.Qh : HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C`
 is induced by `DerivedCategory.Qh : HomotopyCategory C (.up ℤ) ⥤ DerivedCategory C`. -/
+@[simps! -isSimp]
 noncomputable def QhCompιIsoιCompQh :
     Qh ⋙ Plus.ι ≅ HomotopyCategory.Plus.ι C ⋙ DerivedCategory.Qh := Iso.refl _
 
+instance : NatTrans.CommShift (QhCompιIsoιCompQh C).hom ℤ :=
+  ObjectProperty.commShift_liftCompιIso_hom ..
+
 instance : (Qh (C := C)).EssSurj where
   mem_essImage := by
     intro ⟨X, n, K, e, h⟩
@@ -217,11 +221,66 @@ lemma isIso_iff {X Y : Plus C} (f : X ⟶ Y) :
   exact isIso_of_fully_faithful ι _
 
 /-- The localization functor `CochainComplex.Plus C ⥤ DerivedCategory.Plus C`. -/
+@[implicit_reducible]
 noncomputable def Q : CochainComplex.Plus C ⥤ DerivedCategory.Plus C :=
   ObjectProperty.lift _ (CochainComplex.Plus.ι C ⋙ DerivedCategory.Q)
     (fun ⟨K, n, hn⟩ ↦ ⟨n, by dsimp; infer_instance⟩)
 
--- TODO: show that `Q` is indeed a localization functor with respect to quasi-isomorphisms
+noncomputable instance : (Q (C := C)).CommShift ℤ := ObjectProperty.commShiftLift ..
+
+variable (C) in
+/-- The localization functor `CochainComplex.Plus C ⥤ DerivedCategory.Plus C` is
+induced by `DerivedCategory.Q : CochainComplex C ℤ ⥤ DerivedCategory C`. -/
+@[simps!]
+noncomputable def QCompιIso :
+    DerivedCategory.Plus.Q ⋙ Plus.ι ≅ CochainComplex.Plus.ι C ⋙ DerivedCategory.Q :=
+  ObjectProperty.liftCompιIso ..
+
+instance : NatTrans.CommShift (QCompιIso C).hom ℤ :=
+  ObjectProperty.commShift_liftCompιIso_hom ..
+
+variable (C) in
+/-- The natural isomorphism `HomotopyCategory.Plus.quotient C ⋙ Qh ≅ Q`. -/
+@[simps!]
+noncomputable def quotientCompQhIso : HomotopyCategory.Plus.quotient C ⋙ Qh ≅ Q :=
+  NatIso.ofComponents (fun X ↦
+    ObjectProperty.isoMk _ ((DerivedCategory.quotientCompQhIso C).app X.obj)) (fun _ ↦ by
+      ext
+      apply (DerivedCategory.quotientCompQhIso C).hom.naturality)
+
+open Functor in
+@[reassoc]
+lemma whiskerRight_quotientCompQhIso_hom_ι :
+    whiskerRight (quotientCompQhIso C).hom ι =
+    (associator _ _ _).hom ≫ whiskerLeft _ (QhCompιIsoιCompQh C).hom ≫
+    (associator _ _ _).inv ≫
+    whiskerRight (HomotopyCategory.Plus.quotientCompιIso C).hom _ ≫ (associator _ _ _).hom ≫
+    whiskerLeft _ (DerivedCategory.quotientCompQhIso C).hom ≫ (QCompιIso C).inv := by
+  ext K
+  dsimp
+  simp [QCompιIso_inv_app, comp_id, id_comp,
+    QhCompιIsoιCompQh_hom_app, HomotopyCategory.Plus.quotientCompιIso_hom_app,
+    DerivedCategory.Qh.map_id ((HomotopyCategory.quotient _ (.up ℤ)).obj K.obj),
+    dsimp% Category.id_comp ((DerivedCategory.quotientCompQhIso C).hom.app K.obj)]
+
+instance : NatTrans.CommShift (quotientCompQhIso C).hom ℤ :=
+  NatTrans.CommShift.of_comp_faithful ι (by
+    rw [whiskerRight_quotientCompQhIso_hom_ι]
+    infer_instance)
+
+instance : (HomotopyCategory.Plus.quotient C ⋙ Qh).IsLocalization
+    (CochainComplex.Plus.quasiIso C) := by
+  refine Functor.IsLocalization.comp _ _
+    (((HomologicalComplex.homotopyEquivalences C (.up ℤ)).inverseImage (CochainComplex.Plus.ι C)))
+    (HomotopyCategory.Plus.quasiIso C) _ (fun _ _ f _ ↦ ?_) (fun _ _ _ hf ↦ ?_)
+    (by rw [HomotopyCategory.Plus.quasiIso_map_quotient_eq_quasiIso])
+  · refine Localization.inverts Qh (HomotopyCategory.Plus.quasiIso C) _ ?_
+    simpa [HomotopyCategory.Plus.quasiIso_iff, HomotopyCategory.quotient_map_mem_quasiIso_iff]
+  · rw [CochainComplex.Plus.quasiIso_iff]
+    exact homotopyEquivalences_le_quasiIso _ _ _ hf
+
+instance : Q.IsLocalization (CochainComplex.Plus.quasiIso C) :=
+  Functor.IsLocalization.of_iso _ (quotientCompQhIso C)
 
 end Plus