feat: definition of the distinguished triangles in the opposite categ…

…ory (#7327)

Mathlib/CategoryTheory/Opposites.lean

@@ -69,7 +69,7 @@ instance Category.opposite : Category.{v₁} Cᵒᵖ where
   id X := (𝟙 (unop X)).op
 #align category_theory.category.opposite CategoryTheory.Category.opposite
 
-@[simp]
+@[simp, reassoc]
 theorem op_comp {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).op = g.op ≫ f.op :=
   rfl
 #align category_theory.op_comp CategoryTheory.op_comp
@@ -79,7 +79,7 @@ theorem op_id {X : C} : (𝟙 X).op = 𝟙 (op X) :=
   rfl
 #align category_theory.op_id CategoryTheory.op_id
 
-@[simp]
+@[simp, reassoc]
 theorem unop_comp {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g).unop = g.unop ≫ f.unop :=
   rfl
 #align category_theory.unop_comp CategoryTheory.unop_comp

Mathlib/CategoryTheory/Triangulated/Opposite.lean

@@ -28,6 +28,15 @@ Some compatibilities between the shifts on `C` and `Cᵒᵖ` are also expressed
 the equivalence of categories `opShiftFunctorEquivalence C n : Cᵒᵖ ≌ Cᵒᵖ` whose
 functor is `shiftFunctor Cᵒᵖ n` and whose inverse functor is `(shiftFunctor C n).op`.
 
+If `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` is a distinguished triangle in `C`, then the triangle
+`op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧` that is deduced *without introducing signs*
+shall be a distinguished triangle in `Cᵒᵖ`. This is equivalent to the definition
+in [Verdiers's thesis, p. 96][verdier1996] which would require that the triangle
+`(op X)⟦-1⟧ ⟶ op Z ⟶ op Y ⟶ op X` (without signs) is *antidistinguished*.
+
+## References
+* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996]
+
 -/
 
 namespace CategoryTheory
@@ -79,8 +88,6 @@ lemma shiftFunctorZero_op_hom_app (X : Cᵒᵖ) :
   erw [@pullbackShiftFunctorZero_hom_app (OppositeShift C ℤ), oppositeShiftFunctorZero_hom_app]
   rfl
 
-attribute [reassoc] op_comp unop_comp
-
 lemma shiftFunctorZero_op_inv_app (X : Cᵒᵖ) :
     (shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
       ((shiftFunctorZero C ℤ).hom.app X.unop).op ≫
@@ -165,6 +172,136 @@ lemma opShiftFunctorEquivalence_counitIso_hom_app_shift (X : Cᵒᵖ) (n : ℤ)
       ((opShiftFunctorEquivalence C n).unitIso.inv.app X)⟦n⟧' :=
   (opShiftFunctorEquivalence C n).counit_app_functor X
 
+variable (C)
+
+namespace TriangleOpEquivalence
+
+/-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `C` to the triangle
+`op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧` in `Cᵒᵖ` (without introducing signs). -/
+@[simps]
+noncomputable def functor : (Triangle C)ᵒᵖ ⥤ Triangle Cᵒᵖ where
+  obj T := Triangle.mk T.unop.mor₂.op T.unop.mor₁.op
+      ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op T.unop.obj₁) ≫
+        T.unop.mor₃.op⟦(1 : ℤ)⟧')
+  map {T₁ T₂} φ :=
+    { hom₁ := φ.unop.hom₃.op
+      hom₂ := φ.unop.hom₂.op
+      hom₃ := φ.unop.hom₁.op
+      comm₁ := Quiver.Hom.unop_inj φ.unop.comm₂.symm
+      comm₂ := Quiver.Hom.unop_inj φ.unop.comm₁.symm
+      comm₃ := by
+        dsimp
+        rw [assoc, ← Functor.map_comp, ← op_comp, ← φ.unop.comm₃, op_comp, Functor.map_comp]
+        erw [(opShiftFunctorEquivalence C 1).counitIso.inv.naturality_assoc φ.unop.hom₁.op]
+        rfl }
+
+/-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `Cᵒᵖ` to the triangle
+`Z.unop ⟶ Y.unop ⟶ X.unop ⟶ Z.unop⟦1⟧` in `C` (without introducing signs). -/
+@[simps]
+noncomputable def inverse : Triangle Cᵒᵖ ⥤ (Triangle C)ᵒᵖ where
+  obj T := Opposite.op (Triangle.mk T.mor₂.unop T.mor₁.unop
+      (((opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁).unop ≫ T.mor₃.unop⟦(1 : ℤ)⟧'))
+  map {T₁ T₂} φ := Quiver.Hom.op
+    { hom₁ := φ.hom₃.unop
+      hom₂ := φ.hom₂.unop
+      hom₃ := φ.hom₁.unop
+      comm₁ := Opposite.op_injective φ.comm₂.symm
+      comm₂ := Opposite.op_injective φ.comm₁.symm
+      comm₃ := by
+        dsimp
+        rw [assoc, ← Functor.map_comp, ← unop_comp, ← φ.comm₃, unop_comp, Functor.map_comp,
+          ← unop_comp_assoc]
+        apply Quiver.Hom.op_inj
+        simp only [Opposite.op_unop, op_comp, Quiver.Hom.op_unop, assoc,
+          Opposite.unop_op, unop_comp]
+        erw [← (opShiftFunctorEquivalence C 1).unitIso.inv.naturality φ.hom₁]
+        rfl }
+
+/-- The unit isomorphism of the
+equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ` .-/
+@[simps!]
+noncomputable def unitIso : 𝟭 _ ≅ functor C ⋙ inverse C :=
+  NatIso.ofComponents (fun T => Iso.op (by
+    refine' Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) _ _ _
+    · aesop_cat
+    · aesop_cat
+    · dsimp
+      simp only [Functor.map_comp, Functor.map_id, comp_id, id_comp]
+      erw [← (NatIso.unop (opShiftFunctorEquivalence C 1).unitIso).inv.naturality_assoc]
+      rw [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app (Opposite.op T.unop.obj₁) 1]
+      dsimp
+      rw [← unop_comp, Iso.hom_inv_id_app]
+      dsimp
+      rw [comp_id]))
+    (fun {T₁ T₂} f => Quiver.Hom.unop_inj (by aesop_cat))
+
+/-- The counit isomorphism of the
+equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ` .-/
+@[simps!]
+noncomputable def counitIso : inverse C ⋙ functor C ≅ 𝟭 _ :=
+  NatIso.ofComponents (fun T => by
+    refine' Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) _ _ _
+    · aesop_cat
+    · aesop_cat
+    · dsimp
+      rw [Functor.map_id, comp_id, id_comp, Functor.map_comp]
+      erw [← (opShiftFunctorEquivalence C 1).counitIso.inv.naturality_assoc T.mor₃]
+      simp only [opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp,
+        Iso.hom_inv_id_app, Functor.map_id, Functor.id_obj, comp_id, Functor.id_map])
+    (by aesop_cat)
+
+end TriangleOpEquivalence
+
+/-- An anti-equivalence between the categories of triangles in `C` and in `Cᵒᵖ`.
+A triangle in `Cᵒᵖ` shall be distinguished iff it correspond to a distinguished
+triangle in `C` via this equivalence. -/
+@[simps]
+noncomputable def triangleOpEquivalence :
+    (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ where
+  functor := TriangleOpEquivalence.functor C
+  inverse := TriangleOpEquivalence.inverse C
+  unitIso := TriangleOpEquivalence.unitIso C
+  counitIso := TriangleOpEquivalence.counitIso C
+
+variable [HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive]
+  [Pretriangulated C]
+
+namespace Opposite
+
+/-- A triangle in `Cᵒᵖ` shall be distinguished iff it corresponds to a distinguished
+triangle in `C` via the equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ`. -/
+def distinguishedTriangles : Set (Triangle Cᵒᵖ) :=
+  fun T => ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C
+
+variable {C}
+
+lemma mem_distinguishedTriangles_iff (T : Triangle Cᵒᵖ) :
+    T ∈ distinguishedTriangles C ↔
+      ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C := by
+  rfl
+
+lemma mem_distinguishedTriangles_iff' (T : Triangle Cᵒᵖ) :
+    T ∈ distinguishedTriangles C ↔
+      ∃ (T' : Triangle C) (_ : T' ∈ distTriang C),
+        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')) := by
+  rw [mem_distinguishedTriangles_iff]
+  constructor
+  · intro hT
+    exact ⟨_ ,hT, ⟨(triangleOpEquivalence C).counitIso.symm.app T⟩⟩
+  · rintro ⟨T', hT', ⟨e⟩⟩
+    refine' isomorphic_distinguished _ hT' _ _
+    exact Iso.unop ((triangleOpEquivalence C).unitIso.app (Opposite.op T') ≪≫
+      (triangleOpEquivalence C).inverse.mapIso e.symm)
+
+lemma isomorphic_distinguished (T₁ : Triangle Cᵒᵖ)
+    (hT₁ : T₁ ∈ distinguishedTriangles C) (T₂ : Triangle Cᵒᵖ) (e : T₂ ≅ T₁) :
+    T₂ ∈ distinguishedTriangles C := by
+  simp only [mem_distinguishedTriangles_iff] at hT₁ ⊢
+  exact Pretriangulated.isomorphic_distinguished _ hT₁ _
+    ((triangleOpEquivalence C).inverse.mapIso e).unop.symm
+
+end Opposite
+
 end Pretriangulated
 
 end CategoryTheory