feat(CategoryTheory): localization of triangulated categories (#11786)

In this PR, it is shown that the localization of a triangulated category is not only pretriangulated but also triangulated (if the class of morphisms has both calculus of left and right fractions). Pretriangulated and triangulated instances are set on the categories `W.Localization` and `W.Localization'`.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean

@@ -33,7 +33,7 @@ a preadditive structure, but only one of these two constructions can be made an
 
 namespace CategoryTheory
 
-open MorphismProperty Preadditive
+open MorphismProperty Preadditive Limits Category
 
 variable {C D : Type*} [Category C] [Category D] [Preadditive C] (L : C ⥤ D)
   {W : MorphismProperty C} [L.IsLocalization W] [W.HasLeftCalculusOfFractions]
@@ -65,6 +65,13 @@ lemma symm_add : φ.symm.add = φ.add := by
   congr 1
   apply add_comm
 
+@[simp]
+lemma map_add (F : C ⥤ D) (hF : W.IsInvertedBy F) [Preadditive D] [F.Additive] :
+    φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF := by
+  have := hF φ.s φ.hs
+  rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
+    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]
+
 end LeftFraction₂
 
 end MorphismProperty
@@ -266,8 +273,8 @@ lemma add_eq_add {X'' Y'' : C} (eX' : L.obj X'' ≅ X') (eY' : L.obj Y'' ≅ Y')
     add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂ := by
   have h₁ := comp_add W eX' eX eY (𝟙 _) f₁ f₂
   have h₂ := add_comp W eX' eY eY' f₁ f₂ (𝟙 _)
-  simp only [Category.id_comp] at h₁
-  simp only [Category.comp_id] at h₂
+  simp only [id_comp] at h₁
+  simp only [comp_id] at h₂
   rw [h₁, h₂]
 
 variable (L X' Y') in
@@ -310,15 +317,39 @@ lemma functor_additive :
 
 attribute [irreducible] preadditive
 
-noncomputable instance : Preadditive W.Localization := preadditive W.Q W
+lemma functor_additive_iff {E : Type*} [Category E] [Preadditive E] [Preadditive D] [L.Additive]
+    (G : D ⥤ E) :
+    G.Additive ↔ (L ⋙ G).Additive := by
+  constructor
+  · intro
+    infer_instance
+  · intro h
+    suffices ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g by
+      refine ⟨fun {X Y f g} => ?_⟩
+      have hL := essSurj L W
+      have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
+        ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
+      rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
+        ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq
+      rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
+        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]
+    intros X Y f g
+    obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g
+    have := Localization.inverts L W φ.s φ.hs
+    rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
+      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
+      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
+      Functor.map_add, Functor.comp_map, Functor.comp_map]
 
+noncomputable instance : Preadditive W.Localization := preadditive W.Q W
 instance : W.Q.Additive := functor_additive W.Q W
+instance [HasZeroObject C] : HasZeroObject W.Localization := W.Q.hasZeroObject_of_additive
 
 variable [W.HasLocalization]
 
 noncomputable instance : Preadditive W.Localization' := preadditive W.Q' W
-
 instance : W.Q'.Additive := functor_additive W.Q' W
+instance [HasZeroObject C] : HasZeroObject W.Localization' := W.Q'.hasZeroObject_of_additive
 
 end Localization
 

Mathlib/CategoryTheory/Localization/Triangulated.lean

@@ -3,19 +3,17 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.CategoryTheory.Localization.CalculusOfFractions
+import Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
+import Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
 import Mathlib.CategoryTheory.Triangulated.Functor
 import Mathlib.CategoryTheory.Shift.Localization
 
 /-! # Localization of triangulated categories
 
 If `L : C ⥤ D` is a localization functor for a class of morphisms `W` that is compatible
-with the triangulation on the category `C` and admits left and right calculus of fractions,
+with the triangulation on the category `C` and admits a left calculus of fractions,
 it is shown in this file that `D` can be equipped with a pretriangulated category structure,
-and that it is triangulated (TODO).
-
-## TODO
-* obtain (pre)triangulated instances on `W.Localization` and `W.Localization'`.
+and that it is triangulated.
 
 ## References
 * [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996]
@@ -194,6 +192,33 @@ instance isTriangulated_functor :
     letI : Pretriangulated D := pretriangulated L W; L.IsTriangulated :=
     letI : Pretriangulated D := pretriangulated L W; ⟨fun T hT => ⟨T, Iso.refl _, hT⟩⟩
 
+lemma isTriangulated [Pretriangulated D] [L.IsTriangulated] [IsTriangulated C] :
+    IsTriangulated D := by
+  have := essSurj_mapComposableArrows L W 2
+  exact isTriangulated_of_essSurj_mapComposableArrows_two L
+
+instance (n : ℤ) : (shiftFunctor (W.Localization) n).Additive := by
+  rw [Localization.functor_additive_iff W.Q W]
+  exact Functor.additive_of_iso (W.Q.commShiftIso n)
+
+instance : Pretriangulated W.Localization := pretriangulated W.Q W
+
+instance [IsTriangulated C] : IsTriangulated W.Localization := isTriangulated W.Q W
+
+section
+
+variable [W.HasLocalization]
+
+instance (n : ℤ) : (shiftFunctor (W.Localization') n).Additive := by
+  rw [Localization.functor_additive_iff W.Q' W]
+  exact Functor.additive_of_iso (W.Q'.commShiftIso n)
+
+instance : Pretriangulated W.Localization' := pretriangulated W.Q' W
+
+instance [IsTriangulated C] : IsTriangulated W.Localization' := isTriangulated W.Q' W
+
+end
+
 end Localization
 
 end Triangulated

Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

@@ -131,6 +131,11 @@ lemma additive_of_comp_faithful
   map_add {_ _ f₁ f₂} := G.map_injective (by
     rw [← Functor.comp_map, G.map_add, (F ⋙ G).map_add, Functor.comp_map, Functor.comp_map])
 
+open ZeroObject Limits in
+lemma hasZeroObject_of_additive [HasZeroObject C] :
+    HasZeroObject D where
+  zero := ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
+
 end
 
 section InducedCategory

Mathlib/CategoryTheory/Shift/Localization.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Shift.Induced
-import Mathlib.CategoryTheory.Localization.Predicate
+import Mathlib.CategoryTheory.Localization.HasLocalization
 
 /-!
 # The shift induced on a localized category
@@ -88,4 +88,18 @@ noncomputable instance MorphismProperty.commShift_Q :
 
 attribute [irreducible] HasShift.localization MorphismProperty.commShift_Q
 
+variable [W.HasLocalization]
+
+/-- The localized category `W.Localization'` is endowed with the induced shift.  -/
+noncomputable instance HasShift.localization' :
+    HasShift W.Localization' A :=
+  HasShift.localized W.Q' W A
+
+/-- The localization functor `W.Q' : C ⥤ W.Localization'` is compatible with the shift. -/
+noncomputable instance MorphismProperty.commShift_Q' :
+    W.Q'.CommShift A :=
+  Functor.CommShift.localized W.Q' W A
+
+attribute [irreducible] HasShift.localization' MorphismProperty.commShift_Q'
+
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Functor.lean

@@ -3,7 +3,8 @@ Copyright (c) 2023 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.CategoryTheory.Triangulated.Pretriangulated
+import Mathlib.CategoryTheory.Triangulated.Triangulated
+import Mathlib.CategoryTheory.ComposableArrows
 import Mathlib.CategoryTheory.Shift.CommShift
 
 /-!
@@ -146,4 +147,60 @@ end IsTriangulated
 
 end Functor
 
+variable {C D : Type*} [Category C] [Category D] [HasShift C ℤ] [HasShift D ℤ]
+  [HasZeroObject C] [HasZeroObject D] [Preadditive C] [Preadditive D]
+  [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive]
+  [Pretriangulated C] [Pretriangulated D]
+
+namespace Triangulated
+
+namespace Octahedron
+
+variable {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
+  {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} {comm : u₁₂ ≫ u₂₃ = u₁₃}
+  {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ X₁⟦(1 : ℤ)⟧} {h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distTriang C}
+  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ X₂⟦(1 : ℤ)⟧} {h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distTriang C}
+  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ X₁⟦(1 : ℤ)⟧} {h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distTriang C}
+  (h : Octahedron comm h₁₂ h₂₃ h₁₃)
+  (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated]
+
+/-- The image of an octahedron by a triangulated functor. -/
+@[simps]
+def map : Octahedron (by dsimp; rw [← F.map_comp, comm])
+    (F.map_distinguished _ h₁₂) (F.map_distinguished _ h₂₃) (F.map_distinguished _ h₁₃) where
+  m₁ := F.map h.m₁
+  m₃ := F.map h.m₃
+  comm₁ := by simpa using F.congr_map h.comm₁
+  comm₂ := by simpa using F.congr_map h.comm₂ =≫ (F.commShiftIso 1).hom.app X₁
+  comm₃ := by simpa using F.congr_map h.comm₃
+  comm₄ := by simpa using F.congr_map h.comm₄ =≫ (F.commShiftIso 1).hom.app X₂
+  mem := isomorphic_distinguished _ (F.map_distinguished _ h.mem) _
+    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _))
+
+end Octahedron
+
+end Triangulated
+
+open Triangulated
+
+/-- If `F : C ⥤ D` is a triangulated functor from a triangulated category, then `D`
+is also triangulated if tuples of composables arrows in `D` can be lifted to `C`. -/
+lemma isTriangulated_of_essSurj_mapComposableArrows_two
+    (F : C ⥤ D) [F.CommShift ℤ] [F.IsTriangulated]
+    [(F.mapComposableArrows 2).EssSurj] [IsTriangulated C] :
+    IsTriangulated D := by
+  apply IsTriangulated.mk
+  intro Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ u₁₂ u₂₃ u₁₃ comm v₁₂ w₁₂ h₁₂ v₂₃ w₂₃ h₂₃ v₁₃ w₁₃ h₁₃
+  obtain ⟨α, ⟨e⟩⟩ : ∃ (α : ComposableArrows C 2),
+      Nonempty ((F.mapComposableArrows 2).obj α ≅ ComposableArrows.mk₂ u₁₂ u₂₃) :=
+    ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩
+  obtain ⟨X₁, X₂, X₃, f, g, rfl⟩ := ComposableArrows.mk₂_surjective α
+  obtain ⟨_, _, _, h₁₂'⟩ := distinguished_cocone_triangle f
+  obtain ⟨_, _, _, h₂₃'⟩ := distinguished_cocone_triangle g
+  obtain ⟨_, _, _, h₁₃'⟩ := distinguished_cocone_triangle (f ≫ g)
+  exact ⟨Octahedron.ofIso (e₁ := (e.app 0).symm) (e₂ := (e.app 1).symm) (e₃ := (e.app 2).symm)
+    (comm₁₂ := ComposableArrows.naturality' e.inv 0 1)
+    (comm₂₃ := ComposableArrows.naturality' e.inv 1 2)
+    (H := (someOctahedron rfl h₁₂' h₂₃' h₁₃').map F) _ _ _ _ _⟩
+
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Triangulated.lean

@@ -109,20 +109,21 @@ def triangleMorphism₂ : Triangle.mk u₁₃ v₁₃ w₁₃ ⟶ Triangle.mk u
 variable (u₁₂ u₁₃ u₂₃ comm h₁₂ h₁₃ h₂₃)
 
 /-- When two diagrams are isomorphic, an octahedron for one gives an octahedron for the other. -/
-def ofIso {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C} (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃')
-    (e₁ : X₁ ≅ X₁') (e₂ : X₂ ≅ X₂')(e₃ : X₃ ≅ X₃')
+def ofIso {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C} (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃') (u₁₃' : X₁' ⟶ X₃')
+    (comm' : u₁₂' ≫ u₂₃' = u₁₃')
+    (e₁ : X₁ ≅ X₁') (e₂ : X₂ ≅ X₂') (e₃ : X₃ ≅ X₃')
     (comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂') (comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ u₂₃')
     (v₁₂' : X₂' ⟶ Z₁₂') (w₁₂' : Z₁₂' ⟶ X₁'⟦(1 : ℤ)⟧)
     (h₁₂' : Triangle.mk u₁₂' v₁₂' w₁₂' ∈ distTriang C)
     (v₂₃' : X₃' ⟶ Z₂₃') (w₂₃' : Z₂₃' ⟶ X₂'⟦(1 : ℤ)⟧)
     (h₂₃' : Triangle.mk u₂₃' v₂₃' w₂₃' ∈ distTriang C)
     (v₁₃' : X₃' ⟶ Z₁₃') (w₁₃' : Z₁₃' ⟶ X₁'⟦(1 : ℤ)⟧)
-    (h₁₃' : Triangle.mk (u₁₂' ≫ u₂₃') v₁₃' w₁₃' ∈ distTriang C)
-    (H : Octahedron rfl h₁₂' h₂₃' h₁₃') : Octahedron comm h₁₂ h₂₃ h₁₃ := by
+    (h₁₃' : Triangle.mk (u₁₃') v₁₃' w₁₃' ∈ distTriang C)
+    (H : Octahedron comm' h₁₂' h₂₃' h₁₃') : Octahedron comm h₁₂ h₂₃ h₁₃ := by
   let iso₁₂ := isoTriangleOfIso₁₂ _ _ h₁₂ h₁₂' e₁ e₂ comm₁₂
   let iso₂₃ := isoTriangleOfIso₁₂ _ _ h₂₃ h₂₃' e₂ e₃ comm₂₃
   let iso₁₃ := isoTriangleOfIso₁₂ _ _ h₁₃ h₁₃' e₁ e₃ (by
-    dsimp; rw [← comm, assoc, ← reassoc_of% comm₁₂, comm₂₃])
+    dsimp; rw [← comm, assoc, ← comm', ← reassoc_of% comm₁₂, comm₂₃])
   have eq₁₂ := iso₁₂.hom.comm₂
   have eq₁₂' := iso₁₂.hom.comm₃
   have eq₁₃ := iso₁₃.hom.comm₂
@@ -222,6 +223,6 @@ lemma IsTriangulated.mk' (h : ∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁'
     obtain ⟨X₁, X₂, X₃, Z₁₂, Z₂₃, Z₁₃, u₁₂, u₂₃, e₁, e₂, e₃, comm₁₂, comm₂₃,
       v₁₂, w₁₂, h₁₂, v₂₃, w₂₃, h₂₃, v₁₃, w₁₃, h₁₃, H⟩ := h u₁₂' u₂₃'
     exact ⟨Octahedron.ofIso u₁₂' u₂₃' u₁₃' comm' h₁₂' h₂₃' h₁₃'
-      u₁₂ u₂₃ e₁ e₂ e₃ comm₁₂ comm₂₃ v₁₂ w₁₂ h₁₂ v₂₃ w₂₃ h₂₃ v₁₃ w₁₃ h₁₃ H.some⟩
+      u₁₂ u₂₃ _ rfl e₁ e₂ e₃ comm₁₂ comm₂₃ v₁₂ w₁₂ h₁₂ v₂₃ w₂₃ h₂₃ v₁₃ w₁₃ h₁₃ H.some⟩
 
 end CategoryTheory