[Merged by Bors] - feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated

Mathlib.lean

@@ -1612,6 +1612,7 @@ import Mathlib.CategoryTheory.Action.Continuous
 import Mathlib.CategoryTheory.Action.Limits
 import Mathlib.CategoryTheory.Action.Monoidal
 import Mathlib.CategoryTheory.Adhesive
+import Mathlib.CategoryTheory.Adjunction.Additive
 import Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
 import Mathlib.CategoryTheory.Adjunction.Basic
 import Mathlib.CategoryTheory.Adjunction.Comma
@@ -2196,6 +2197,7 @@ import Mathlib.CategoryTheory.Subterminal
 import Mathlib.CategoryTheory.Sums.Associator
 import Mathlib.CategoryTheory.Sums.Basic
 import Mathlib.CategoryTheory.Thin
+import Mathlib.CategoryTheory.Triangulated.Adjunction
 import Mathlib.CategoryTheory.Triangulated.Basic
 import Mathlib.CategoryTheory.Triangulated.Functor
 import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Mathlib/CategoryTheory/Adjunction/Additive.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2024 Sophie Morel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sophie More, Joël Riou
+-/
+import Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
+
+/-!
+# Adjunctions between additive functors.
+This provides some results and constructions for adjunctions between functors on
+preadditive categories:
+* If one of the adjoint functors is additive, so is the other.
+* If one of the adjoint functors is additive, the equivalence `Adjunction.homEquiv` lifts to
+an additive equivalence `Adjunction.homAddEquivOfLeftAdjoint` resp.
+`Adjunction.homAddEquivOfRightAdjoint`.
+* We also give a version of this additive equivalence as an isomorphism of `preadditiveYoneda`
+functors (analogous to `Adjunction.compYonedaIso`), in
+`Adjunction.compPreadditiveYonedaIsoOfLeftAdjoint` resp.
+`Adjunction.compPreadditiveYonedaIsoOfRightAdjoint`.
+-/
+
+universe u₁ u₂ v₁ v₂
+
+namespace CategoryTheory
+
+namespace Adjunction
+
+open CategoryTheory Category Functor
+
+variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] [Preadditive C]
+  [Preadditive D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
+
+include adj
+lemma right_adjoint_additive [F.Additive] : G.Additive where
+  map_add {X Y} f g := (adj.homEquiv _ _).symm.injective (by simp [homEquiv_counit])
+
+lemma left_adjoint_additive [G.Additive] : F.Additive where
+  map_add {X Y} f g := (adj.homEquiv _ _).injective (by simp [homEquiv_unit])
+
+variable [F.Additive]
+
+/-- If we have an adjunction `adj : F ⊣ G` of functors between preadditive categories,
+and if `F` is additive, then the hom set equivalence upgrades to an `AddEquiv`.
+Note that `F` is additive if and only if `G` is, by `Adjunction.right_adjoint_additive` and
+`Adjunction.left_adjoint_additive`.
+-/
+def homAddEquiv (X : C) (Y : D) : AddEquiv (F.obj X ⟶ Y) (X ⟶ G.obj Y) :=
+  {
+    adj.homEquiv _ _ with
+    map_add' _ _ := by
+      have := adj.right_adjoint_additive
+      simp [homEquiv_apply] }
+
+@[simp]
+lemma homAddEquiv_apply (X : C) (Y : D) (f : F.obj X ⟶ Y) :
+    adj.homAddEquiv X Y f = adj.homEquiv X Y f := rfl
+
+@[simp]
+lemma homAddEquiv_symm_apply (X : C) (Y : D) (f : X ⟶ G.obj Y) :
+    (adj.homAddEquiv X Y).symm f = (adj.homEquiv X Y).symm f := rfl
+
+@[simp]
+lemma homAddEquiv_zero (X : C) (Y : D) : adj.homEquiv X Y 0 = 0 := by
+  change adj.homAddEquiv X Y 0 = 0
+  rw [map_zero]
+
+@[simp]
+lemma homAddEquiv_add (X : C) (Y : D) (f f' : F.obj X ⟶ Y) :
+    adj.homEquiv X Y (f + f') = adj.homEquiv X Y f + adj.homEquiv X Y f' := by
+  change adj.homAddEquiv X Y (f + f') = _
+  simp [AddEquivClass.map_add]
+
+@[simp]
+lemma homAddEquiv_sub (X : C) (Y : D) (f f' : F.obj X ⟶ Y) :
+    adj.homEquiv X Y (f - f') = adj.homEquiv X Y f - adj.homEquiv X Y f' := by
+  change adj.homAddEquiv X Y (f - f') = _
+  simp [AddEquiv.map_sub]
+
+@[simp]
+lemma homAddEquiv_neg (X : C) (Y : D) (f : F.obj X ⟶ Y) :
+    adj.homEquiv X Y (- f) = - adj.homEquiv X Y f := by
+  change adj.homAddEquiv X Y (- f) = _
+  simp [AddEquiv.map_neg]
+
+@[simp]
+lemma homAddEquiv_symm_zero (X : C) (Y : D) :
+    (adj.homEquiv X Y).symm 0 = 0 := by
+  change (adj.homAddEquiv X Y).symm 0 = 0
+  rw [map_zero]
+
+@[simp]
+lemma homAddEquiv_symm_add (X : C) (Y : D) (f f' : X ⟶ G.obj Y) :
+    (adj.homEquiv X Y).symm (f + f') = (adj.homEquiv X Y).symm f + (adj.homEquiv X Y).symm f' := by
+  change (adj.homAddEquiv X Y).symm (f + f') = _
+  simp [AddEquivClass.map_add]
+
+@[simp]
+lemma homAddEquiv_symm_sub (X : C) (Y : D) (f f' : X ⟶ G.obj Y) :
+    (adj.homEquiv X Y).symm (f - f') = (adj.homEquiv X Y).symm f - (adj.homEquiv X Y).symm f' := by
+  change (adj.homAddEquiv X Y).symm (f - f') = _
+  simp [AddEquiv.map_sub]
+
+@[simp]
+lemma homAddEquiv_symm_neg (X : C) (Y : D) (f : X ⟶ G.obj Y) :
+    (adj.homEquiv X Y).symm (- f) = - (adj.homEquiv X Y).symm f := by
+  change (adj.homAddEquiv X Y).symm (- f) = _
+  simp [AddEquiv.map_neg]
+
+open Opposite in
+/-- If we have an adjunction `adj : F ⊣ G` of functors between preadditive categories,
+and if `F` is additive, then the hom set equivalence upgrades to an isomorphism between
+`G ⋙ preadditiveYoneda` and `preadditiveYoneda ⋙ F`, once we throw in the necessary
+universe lifting functors.
+Note that `F` is additive if and only if `G` is, by `Adjunction.right_adjoint_additive` and
+`Adjunction.left_adjoint_additive`.
+-/
+def compPreadditiveYonedaIso :
+    G ⋙ preadditiveYoneda ⋙ (whiskeringRight _ _ _).obj AddCommGrp.uliftFunctor.{max v₁ v₂} ≅
+      preadditiveYoneda ⋙ (whiskeringLeft _ _ _).obj F.op ⋙
+        (whiskeringRight _ _ _).obj AddCommGrp.uliftFunctor.{max v₁ v₂} := by
+  refine NatIso.ofComponents (fun Y ↦ ?_) (fun _ ↦ ?_)
+  · refine NatIso.ofComponents
+      (fun X ↦ ((AddEquiv.ulift.trans (adj.homAddEquiv (unop X) Y)).trans
+               AddEquiv.ulift.symm).toAddCommGrpIso.symm) (fun _ ↦ ?_)
+    ext
+    simp [homAddEquiv, adj.homEquiv_naturality_left_symm]
+    rfl
+  · ext
+    simp only [comp_obj, preadditiveYoneda_obj, whiskeringLeft_obj_obj, whiskeringRight_obj_obj,
+      op_obj, ModuleCat.forget₂_obj, preadditiveYonedaObj_obj_carrier,
+      preadditiveYonedaObj_obj_isAddCommGroup, AddCommGrp.uliftFunctor_obj, AddCommGrp.coe_of,
+      Functor.comp_map, whiskeringRight_obj_map, NatTrans.comp_app, whiskerRight_app,
+      AddCommGrp.uliftFunctor_map, AddEquiv.toAddMonoidHom_eq_coe, NatIso.ofComponents_hom_app,
+      Iso.symm_hom, AddEquiv.toAddCommGrpIso_inv, AddCommGrp.coe_comp', AddMonoidHom.coe_coe,
+      Function.comp_apply, AddCommGrp.ofHom_apply, AddMonoidHom.coe_comp, AddEquiv.symm_trans_apply,
+      AddEquiv.symm_symm, AddEquiv.apply_symm_apply, whiskeringLeft_obj_map, whiskerLeft_app]
+    erw [adj.homEquiv_naturality_right_symm]
+    rfl
+
+lemma compPreadditiveYonedaIso_hom_app_app_apply (X : Cᵒᵖ) (Y : D)
+    (a : ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y)) :
+      ((adj.compPreadditiveYonedaIso.hom.app Y).app X) a =
+        {down := (adj.homEquiv (Opposite.unop X) Y).symm (AddEquiv.ulift a)} := rfl
+
+lemma compPreadditiveYonedaIso_inv_app_app_apply (X : Cᵒᵖ) (Y : D)
+    (a : ULift.{max v₁ v₂, v₂} (F.obj (Opposite.unop X) ⟶ Y)) :
+      ((adj.compPreadditiveYonedaIso.inv.app Y).app X) a =
+        {down := (adj.homEquiv (Opposite.unop X) Y) (AddEquiv.ulift a)} := rfl
+
+end Adjunction
+
+end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Adjunction.lean

@@ -0,0 +1,143 @@
+/-
+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.Triangulated.Functor
+import Mathlib.CategoryTheory.Shift.Adjunction
+import Mathlib.CategoryTheory.Adjunction.Additive
+
+/-!
+# The adjoint is triangulated
+
+If a functor `F : C ⥤ D` between pretriangulated categories is triangulated, and if we
+have an adjunction `F ⊣ G`, then `G` is also a triangulated functor.
+
+We deduce that, if `E : C ≌ D` is an equivalence of pretriangulated categories, then
+`E.functor` is triangulated if and only if `E.inverse` is triangulated.
+
+TODO: The case of left adjoints.
+-/
+
+namespace CategoryTheory
+
+open Category Limits Preadditive Pretriangulated Adjunction
+
+variable {C D : Type*} [Category C] [Category D] [HasZeroObject C] [HasZeroObject D]
+  [Preadditive C] [Preadditive D] [HasShift C ℤ] [HasShift D ℤ]
+  [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive]
+  [Pretriangulated C] [Pretriangulated D]
+
+namespace Adjunction
+
+variable {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ]
+  [adj.CommShift ℤ] [F.IsTriangulated]
+
+include adj in
+lemma isTriangulated_rightAdjoint : G.IsTriangulated where
+  map_distinguished T hT := by
+    have : G.Additive := adj.right_adjoint_additive
+    dsimp
+    obtain ⟨Z, f, g, mem⟩ := distinguished_cocone_triangle (G.map T.mor₁)
+    obtain ⟨h, ⟨h₁, h₂⟩⟩ := complete_distinguished_triangle_morphism _ _
+      (F.map_distinguished _ mem) hT (adj.counit.app T.obj₁) (adj.counit.app T.obj₂) (by simp)
+    dsimp at h h₁ h₂
+    have h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂ := by
+      simpa [homEquiv_apply] using congr_arg (adj.homEquiv _ _).toFun h₁
+    have h₂' : g ≫ (G.commShiftIso (1 : ℤ)).inv.app T.obj₁ =
+        (adj.homEquiv _ _ h) ≫ G.map T.mor₃ := by
+      apply (adj.homEquiv _ _).symm.injective
+      simp only [Functor.comp_obj, homEquiv_counit, Functor.id_obj, Functor.map_comp, assoc,
+        homEquiv_unit, counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
+        ← h₂, adj.shift_counit_app, Iso.hom_inv_id_app_assoc]
+    rw [assoc] at h₂
+    have : Mono (adj.homEquiv _ _ h) := by
+      rw [mono_iff_cancel_zero]
+      intro Y φ hφ
+      obtain ⟨ψ, rfl⟩ := Triangle.coyoneda_exact₃ _ mem φ (by
+        dsimp
+        simp [homEquiv_unit] at hφ
+        rw [← cancel_mono ((G.commShiftIso (1 : ℤ)).inv.app T.obj₁), assoc, h₂', zero_comp,
+          homEquiv_unit, assoc, reassoc_of% hφ, zero_comp])
+      dsimp at ψ hφ ⊢
+      obtain ⟨α, hα⟩ := T.coyoneda_exact₂ hT ((adj.homEquiv _ _).symm ψ)
+        ((adj.homEquiv _ _).injective (by simpa [homEquiv_counit, homEquiv_unit, ← h₁'] using hφ))
+      have eq := congr_arg (adj.homEquiv _ _ ).toFun hα
+      simp only [homEquiv_counit, Functor.id_obj, Equiv.toFun_as_coe, homEquiv_unit,
+        Functor.comp_obj, Functor.map_comp, unit_naturality_assoc, right_triangle_components,
+        comp_id] at eq
+      rw [eq, assoc, assoc]
+      erw [comp_distTriang_mor_zero₁₂ _ mem, comp_zero, comp_zero]
+    have := isIso_of_yoneda_map_bijective (adj.homEquiv _ _ h) (fun Y => by
+      constructor
+      · intro φ₁ φ₂ hφ
+        rw [← cancel_mono (adj.homEquiv _ _ h)]
+        exact hφ
+      · intro φ
+        obtain ⟨ψ, hψ⟩ := Triangle.coyoneda_exact₁ _ mem (φ ≫ G.map T.mor₃ ≫
+          (G.commShiftIso (1 : ℤ)).hom.app T.obj₁) (by
+            dsimp
+            simp only [assoc]
+            rw [← G.commShiftIso_hom_naturality, ← G.map_comp_assoc,
+              comp_distTriang_mor_zero₃₁ _ hT, G.map_zero, zero_comp, comp_zero])
+        dsimp at ψ hψ
+        obtain ⟨α, hα⟩ : ∃ α, α = φ - ψ ≫ (adj.homEquiv _ _) h := ⟨_, rfl⟩
+        have hα₀ : α ≫ G.map T.mor₃ = 0 := by
+          rw [hα, sub_comp, ← cancel_mono ((Functor.commShiftIso G (1 : ℤ)).hom.app T.obj₁),
+            assoc, sub_comp, assoc, assoc, hψ, zero_comp, sub_eq_zero,
+            ← cancel_mono ((Functor.commShiftIso G (1 : ℤ)).inv.app T.obj₁), assoc,
+            assoc, assoc, assoc, h₂', Iso.hom_inv_id_app, comp_id]
+        suffices ∃ (β : Y ⟶ Z), β ≫ (adj.homEquiv _ _) h = α by
+          obtain ⟨β, hβ⟩ := this
+          refine ⟨ψ + β, ?_⟩
+          dsimp
+          rw [add_comp, hβ, hα, add_sub_cancel]
+        obtain ⟨β, hβ⟩ := T.coyoneda_exact₃ hT ((adj.homEquiv _ _).symm α)
+          ((adj.homEquiv _ _).injective (by simpa [homEquiv_unit, homEquiv_counit] using hα₀))
+        refine ⟨adj.homEquiv _ _ β ≫ f, ?_⟩
+        simpa [homEquiv_unit, h₁'] using congr_arg (adj.homEquiv _ _).toFun hβ.symm)
+    refine isomorphic_distinguished _ mem _ (Iso.symm ?_)
+    refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (asIso (adj.homEquiv Z T.obj₃ h)) ?_ ?_ ?_
+    · dsimp
+      simp
+    · apply (adj.homEquiv _ _).symm.injective
+      dsimp
+      simp only [homEquiv_unit, homEquiv_counit, Functor.map_comp, assoc,
+        counit_naturality, left_triangle_components_assoc, h₁, id_comp]
+    · dsimp
+      rw [Functor.map_id, comp_id, homEquiv_unit, assoc, ← G.map_comp_assoc, ← h₂,
+        Functor.map_comp, Functor.map_comp, assoc, unit_naturality_assoc, assoc,
+        Functor.commShiftIso_hom_naturality, ← adj.shift_unit_app_assoc,
+        ← Functor.map_comp, right_triangle_components, Functor.map_id, comp_id]
+
+end Adjunction
+
+namespace Equivalence
+
+variable (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.CommShift ℤ]
+
+/--
+We say that an equivalence of categories `E` is triangulated if both `E.functor` and
+`E.inverse` are triangulated functors.
+-/
+class IsTriangulated : Prop where
+  functor_isTriangulated : E.functor.IsTriangulated := by infer_instance
+  inverse_isTriangulated : E.inverse.IsTriangulated := by infer_instance
+
+namespace IsTriangulated
+
+attribute [instance] functor_isTriangulated inverse_isTriangulated
+
+/-- Constructor for `Equivalence.IsTriangulated`. -/
+lemma mk' (h : E.functor.IsTriangulated) : E.IsTriangulated where
+  inverse_isTriangulated := E.toAdjunction.isTriangulated_rightAdjoint
+
+/-- Constructor for `Equivalence.IsTriangulated`. -/
+lemma mk'' (h : E.inverse.IsTriangulated) : E.IsTriangulated where
+  functor_isTriangulated := (mk' E.symm h).inverse_isTriangulated
+
+end IsTriangulated
+
+end Equivalence
+
+end CategoryTheory