[Merged by Bors] - feat: the pretriangulated structure on the opposite category

Mathlib/CategoryTheory/Opposites.lean

@@ -460,6 +460,20 @@ theorem unop_op {X Y : Cᵒᵖ} (f : X ≅ Y) : f.unop.op = f := by (ext; rfl)
 theorem op_unop {X Y : C} (f : X ≅ Y) : f.op.unop = f := by (ext; rfl)
 #align category_theory.iso.op_unop CategoryTheory.Iso.op_unop
 
+section
+
+variable {D : Type*} [Category D] {F G : C ⥤ Dᵒᵖ} (e : F ≅ G) (X : C)
+
+@[reassoc (attr := simp)]
+lemma unop_hom_inv_id_app : (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 _ := by
+  rw [← unop_comp, inv_hom_id_app, unop_id]
+
+@[reassoc (attr := simp)]
+lemma unop_inv_hom_id_app : (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 _ := by
+  rw [← unop_comp, hom_inv_id_app, unop_id]
+
+end
+
 end Iso
 
 namespace NatIso

Mathlib/CategoryTheory/Preadditive/Basic.lean

@@ -443,6 +443,38 @@ theorem hasCoequalizers_of_hasCokernels [HasCokernels C] : HasCoequalizers C :=
 
 end Equalizers
 
+section
+
+variable {C : Type*} [Category C] [Preadditive C] {X Y : C}
+
+instance : SMul (Units ℤ) (X ≅ Y) where
+  smul a e :=
+    { hom := (a : ℤ) • e.hom
+      inv := ((a⁻¹ : Units ℤ) : ℤ) • e.inv
+      hom_inv_id := by
+        simp only [comp_zsmul, zsmul_comp, smul_smul, Units.inv_mul, one_smul, e.hom_inv_id]
+      inv_hom_id := by
+        simp only [comp_zsmul, zsmul_comp, smul_smul, Units.mul_inv, one_smul, e.inv_hom_id] }
+
+@[simp]
+lemma smul_iso_hom (a : Units ℤ) (e : X ≅ Y) : (a • e).hom = (a : ℤ) • e.hom := rfl
+
+@[simp]
+lemma smul_iso_inv (a : Units ℤ) (e : X ≅ Y) : (a • e).inv = ((a⁻¹ : Units ℤ) : ℤ) • e.inv := rfl
+
+instance : Neg (X ≅ Y) where
+  neg e :=
+    { hom := -e.hom
+      inv := -e.inv }
+
+@[simp]
+lemma neg_iso_hom (e : X ≅ Y) : (-e).hom = -e.hom := rfl
+
+@[simp]
+lemma neg_iso_inv (e : X ≅ Y) : (-e).inv = -e.inv := rfl
+
+end
+
 end Preadditive
 
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Opposite.lean

@@ -150,6 +150,33 @@ noncomputable def opShiftFunctorEquivalence (n : ℤ) : Cᵒᵖ ≌ Cᵒᵖ wher
       ((shiftFunctorCompIsoId C (-n) n (neg_add_self n)).hom.app X.unop)⟦-n⟧' = 𝟙 _
     rw [shift_shiftFunctorCompIsoId_neg_add_self_hom_app n X.unop, Iso.inv_hom_id_app])
 
+/-! The naturality of the unit and counit isomorphisms are restated in the following
+lemmas so as to mitigate the need for `erw`. -/
+
+@[reassoc (attr := simp)]
+lemma opShiftFunctorEquivalence_unitIso_hom_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    f ≫ (opShiftFunctorEquivalence C n).unitIso.hom.app Y =
+      (opShiftFunctorEquivalence C n).unitIso.hom.app X ≫ (f⟦n⟧').unop⟦n⟧'.op :=
+  (opShiftFunctorEquivalence C n).unitIso.hom.naturality f
+
+@[reassoc (attr := simp)]
+lemma opShiftFunctorEquivalence_unitIso_inv_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    (f⟦n⟧').unop⟦n⟧'.op ≫ (opShiftFunctorEquivalence C n).unitIso.inv.app Y =
+      (opShiftFunctorEquivalence C n).unitIso.inv.app X ≫ f :=
+  (opShiftFunctorEquivalence C n).unitIso.inv.naturality f
+
+@[reassoc (attr := simp)]
+lemma opShiftFunctorEquivalence_counitIso_hom_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    f.unop⟦n⟧'.op⟦n⟧' ≫ (opShiftFunctorEquivalence C n).counitIso.hom.app Y =
+      (opShiftFunctorEquivalence C n).counitIso.hom.app X ≫ f :=
+  (opShiftFunctorEquivalence C n).counitIso.hom.naturality f
+
+@[reassoc (attr := simp)]
+lemma opShiftFunctorEquivalence_counitIso_inv_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    f ≫ (opShiftFunctorEquivalence C n).counitIso.inv.app Y =
+      (opShiftFunctorEquivalence C n).counitIso.inv.app X ≫ f.unop⟦n⟧'.op⟦n⟧' :=
+  (opShiftFunctorEquivalence C n).counitIso.inv.naturality f
+
 variable {C}
 
 lemma shift_unop_opShiftFunctorEquivalence_counitIso_inv_app (X : Cᵒᵖ) (n : ℤ) :
@@ -191,8 +218,8 @@ noncomputable def functor : (Triangle C)ᵒᵖ ⥤ Triangle Cᵒᵖ where
       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]
+        rw [assoc, ← Functor.map_comp, ← op_comp, ← φ.unop.comm₃, op_comp, Functor.map_comp,
+          opShiftFunctorEquivalence_counitIso_inv_naturality_assoc]
         rfl }
 
 /-- The functor which sends a triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧` in `Cᵒᵖ` to the triangle
@@ -205,34 +232,22 @@ noncomputable def inverse : Triangle Cᵒᵖ ⥤ (Triangle C)ᵒᵖ where
     { hom₁ := φ.hom₃.unop
       hom₂ := φ.hom₂.unop
       hom₃ := φ.hom₁.unop
-      comm₁ := Opposite.op_injective φ.comm₂.symm
-      comm₂ := Opposite.op_injective φ.comm₁.symm
-      comm₃ := by
+      comm₁ := Quiver.Hom.op_inj φ.comm₂.symm
+      comm₂ := Quiver.Hom.op_inj φ.comm₁.symm
+      comm₃ := Quiver.Hom.op_inj (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 }
+        rw [assoc, ← opShiftFunctorEquivalence_unitIso_inv_naturality,
+          ← op_comp_assoc, ← Functor.map_comp, ← unop_comp, ← φ.comm₃,
+          unop_comp, Functor.map_comp, op_comp, assoc]) }
 
 /-- 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]))
+  NatIso.ofComponents (fun T => Iso.op
+    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
+      (Quiver.Hom.op_inj
+        (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))))
     (fun {T₁ T₂} f => Quiver.Hom.unop_inj (by aesop_cat))
 
 /-- The counit isomorphism of the
@@ -244,10 +259,11 @@ noncomputable def counitIso : inverse C ⋙ functor C ≅ 𝟭 _ :=
     · 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])
+      rw [Functor.map_id, comp_id, id_comp, Functor.map_comp,
+        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc,
+        opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp,
+        Iso.hom_inv_id_app, Functor.map_id]
+      simp only [Functor.id_obj, comp_id])
     (by aesop_cat)
 
 end TriangleOpEquivalence
@@ -300,8 +316,107 @@ lemma isomorphic_distinguished (T₁ : Triangle Cᵒᵖ)
   exact Pretriangulated.isomorphic_distinguished _ hT₁ _
     ((triangleOpEquivalence C).inverse.mapIso e).unop.symm
 
+/-- Up to rotation, the contractible triangle `X ⟶ X ⟶ 0 ⟶ X⟦1⟧` for `X : Cᵒᵖ` corresponds
+to the contractible triangle for `X.unop` in `C`. -/
+@[simps!]
+noncomputable def contractibleTriangleIso (X : Cᵒᵖ) :
+    contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj
+      (Opposite.op (contractibleTriangle X.unop).invRotate) :=
+  Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
+    (IsZero.iso (isZero_zero _) (by
+      dsimp
+      rw [IsZero.iff_id_eq_zero]
+      change (𝟙 ((0 : C)⟦(-1 : ℤ)⟧)).op = 0
+      rw [← Functor.map_id, id_zero, Functor.map_zero, op_zero]))
+    (by aesop_cat) (by aesop_cat) (by aesop_cat)
+
+lemma contractible_distinguished (X : Cᵒᵖ) :
+    contractibleTriangle X ∈ distinguishedTriangles C := by
+  rw [mem_distinguishedTriangles_iff']
+  exact ⟨_, inv_rot_of_distTriang _ (Pretriangulated.contractible_distinguished X.unop),
+    ⟨contractibleTriangleIso X⟩⟩
+
+/-- Isomorphism expressing a compatibility of the equivalence `triangleOpEquivalence C`
+with the rotation of triangles. -/
+noncomputable def rotateTriangleOpEquivalenceInverseObjRotateUnopIso (T : Triangle Cᵒᵖ) :
+    ((triangleOpEquivalence C).inverse.obj T.rotate).unop.rotate ≅
+      ((triangleOpEquivalence C).inverse.obj T).unop :=
+  Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
+      (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop) (by simp)
+        (Quiver.Hom.op_inj (by aesop_cat)) (by aesop_cat)
+
+lemma rotate_distinguished_triangle (T : Triangle Cᵒᵖ) :
+    T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C := by
+  simp only [mem_distinguishedTriangles_iff, Pretriangulated.rotate_distinguished_triangle
+    ((triangleOpEquivalence C).inverse.obj (T.rotate)).unop]
+  exact distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm
+
+lemma distinguished_cocone_triangle {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    ∃ (Z : Cᵒᵖ) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧),
+      Triangle.mk f g h ∈ distinguishedTriangles C := by
+  obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle₁ f.unop
+  refine' ⟨_, g.op, (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
+    (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op, _⟩
+  simp only [mem_distinguishedTriangles_iff]
+  refine' Pretriangulated.isomorphic_distinguished _ H _ _
+  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
+    (Quiver.Hom.op_inj (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))
+
+lemma complete_distinguished_triangle_morphism (T₁ T₂ : Triangle Cᵒᵖ)
+    (hT₁ : T₁ ∈ distinguishedTriangles C) (hT₂ : T₂ ∈ distinguishedTriangles C)
+    (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁) :
+    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
+      T₁.mor₃ ≫ a⟦1⟧' = c ≫ T₂.mor₃ := by
+  rw [mem_distinguishedTriangles_iff] at hT₁ hT₂
+  obtain ⟨c, hc₁, hc₂⟩ :=
+    Pretriangulated.complete_distinguished_triangle_morphism₁ _ _ hT₂ hT₁
+      b.unop a.unop (Quiver.Hom.op_inj comm.symm)
+  dsimp at c hc₁ hc₂
+  replace hc₂ := ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫= hc₂
+  dsimp at hc₂
+  simp only [assoc, Iso.unop_hom_inv_id_app_assoc] at hc₂
+  refine' ⟨c.op, Quiver.Hom.unop_inj hc₁.symm, Quiver.Hom.unop_inj _⟩
+  apply (shiftFunctor C (1 : ℤ)).map_injective
+  rw [unop_comp, unop_comp, Functor.map_comp, Functor.map_comp,
+    Quiver.Hom.unop_op, hc₂, ← unop_comp_assoc, ← unop_comp_assoc,
+    ← opShiftFunctorEquivalence_unitIso_inv_naturality]
+  simp
+
+/-- The pretriangulated structure on the opposite category of
+a pretriangulated category. It is a scoped instance, so that we need to
+`open CategoryTheory.Pretriangulated.Opposite` in order to be able
+to use it: the reason is that it relies on the definition of the shift
+on the opposite category `Cᵒᵖ`, for which it is unclear whether it should
+be a global instance or not. -/
+scoped instance : Pretriangulated Cᵒᵖ where
+  distinguishedTriangles := distinguishedTriangles C
+  isomorphic_distinguished := isomorphic_distinguished
+  contractible_distinguished := contractible_distinguished
+  distinguished_cocone_triangle := distinguished_cocone_triangle
+  rotate_distinguished_triangle := rotate_distinguished_triangle
+  complete_distinguished_triangle_morphism := complete_distinguished_triangle_morphism
+
 end Opposite
 
+variable {C}
+
+lemma mem_distTriang_op_iff (T : Triangle Cᵒᵖ) :
+    (T ∈ distTriang Cᵒᵖ) ↔ ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C := by
+  rfl
+
+lemma mem_distTriang_op_iff' (T : Triangle Cᵒᵖ) :
+    (T ∈ distTriang Cᵒᵖ) ↔ ∃ (T' : Triangle C) (_ : T' ∈ distTriang C),
+      Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')) :=
+  Opposite.mem_distinguishedTriangles_iff' T
+
+lemma op_distinguished (T : Triangle C) (hT : T ∈ distTriang C) :
+    ((triangleOpEquivalence C).functor.obj (Opposite.op T)) ∈ distTriang Cᵒᵖ := by
+  rw [mem_distTriang_op_iff']
+  exact ⟨T, hT, ⟨Iso.refl _⟩⟩
+
+lemma unop_distinguished (T : Triangle Cᵒᵖ) (hT : T ∈ distTriang Cᵒᵖ) :
+    ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C := hT
+
 end Pretriangulated
 
 end CategoryTheory