feat(CategoryTheory/Triangulated): more API (#10527)

In this PR, it is shown that in order to show that a pretriangulated category is triangulated category, i.e. in order to check the octahedron axiom, it is possible to replace a given diagram by an isomorphic diagram. This shall be used in #9550 in order to show that the homotopy category of cochain complexes in an additive category is triangulated.

Mathlib/CategoryTheory/Triangulated/Basic.lean

@@ -331,4 +331,36 @@ lemma productTriangle.zero₃₁ [HasZeroMorphisms C]
 
 end
 
+namespace Triangle
+
+/-- The first projection `Triangle C ⥤ C`. -/
+@[simps]
+def π₁ : Triangle C ⥤ C where
+  obj T := T.obj₁
+  map f := f.hom₁
+
+/-- The second projection `Triangle C ⥤ C`. -/
+@[simps]
+def π₂ : Triangle C ⥤ C where
+  obj T := T.obj₂
+  map f := f.hom₂
+
+/-- The third projection `Triangle C ⥤ C`. -/
+@[simps]
+def π₃ : Triangle C ⥤ C where
+  obj T := T.obj₃
+  map f := f.hom₃
+
+section
+
+variable {A B : Triangle C} (φ : A ⟶ B) [IsIso φ]
+
+instance : IsIso φ.hom₁ := (inferInstance : IsIso (π₁.map φ))
+instance : IsIso φ.hom₂ := (inferInstance : IsIso (π₂.map φ))
+instance : IsIso φ.hom₃ := (inferInstance : IsIso (π₃.map φ))
+
+end
+
+end Triangle
+
 end CategoryTheory.Pretriangulated

Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

@@ -615,6 +615,33 @@ lemma productTriangle_distinguished {J : Type*} (T : J → Triangle C)
       rw [add_comp, assoc, φ'.comm₂, h₂, id_comp, ← hb', add_sub_cancel'_right]
     exact ⟨_, this⟩
 
+lemma exists_iso_of_arrow_iso (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distTriang C)
+    (hT₂ : T₂ ∈ distTriang C) (e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁) :
+    ∃ (e' : T₁ ≅ T₂), e'.hom.hom₁ = e.hom.left ∧ e'.hom.hom₂ = e.hom.right := by
+  let φ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ e.hom.left e.hom.right e.hom.w.symm
+  have : IsIso φ.hom₁ := by dsimp; infer_instance
+  have : IsIso φ.hom₂ := by dsimp; infer_instance
+  have : IsIso φ.hom₃ := isIso₃_of_isIso₁₂ φ hT₁ hT₂ inferInstance inferInstance
+  have : IsIso φ := by
+    apply Triangle.isIso_of_isIsos
+    all_goals infer_instance
+  exact ⟨asIso φ, by simp, by simp⟩
+
+/-- A choice of isomorphism `T₁ ≅ T₂` between two distinguished triangles
+when we are given two isomorphisms `e₁ : T₁.obj₁ ≅ T₂.obj₁` and `e₂ : T₁.obj₂ ≅ T₂.obj₂`. -/
+@[simps! hom_hom₁ hom_hom₂ inv_hom₁ inv_hom₂]
+def isoTriangleOfIso₁₂ (T₁ T₂ : Triangle C) (hT₁ : T₁ ∈ distTriang C)
+    (hT₂ : T₂ ∈ distTriang C) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂)
+    (comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁) : T₁ ≅ T₂ := by
+  have h := exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ (Arrow.isoMk e₁ e₂ comm.symm)
+  exact Triangle.isoMk _ _ e₁ e₂ (Triangle.π₃.mapIso h.choose) comm (by
+    have eq := h.choose_spec.2
+    dsimp at eq ⊢
+    conv_rhs => rw [← eq, ← TriangleMorphism.comm₂]) (by
+    have eq := h.choose_spec.1
+    dsimp at eq ⊢
+    conv_lhs => rw [← eq, TriangleMorphism.comm₃])
+
 end Pretriangulated
 
 end CategoryTheory

Mathlib/CategoryTheory/Triangulated/Triangulated.lean

@@ -64,7 +64,7 @@ namespace Octahedron
 attribute [reassoc] comm₁ comm₂ comm₃ comm₄
 
 variable {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
-  {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃)
+  {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}
@@ -108,9 +108,58 @@ def triangleMorphism₂ : Triangle.mk u₁₃ v₁₃ w₁₃ ⟶ Triangle.mk u
   comm₃ := h.comm₄
 #align category_theory.triangulated.octahedron.triangle_morphism₂ CategoryTheory.Triangulated.Octahedron.triangleMorphism₂
 
-/- TODO (@joelriou): show that in order to verify the existence of an octahedron, one may
-replace the composable maps `u₁₂` and `u₂₃` by any isomorphic composable maps
-and the given "cones" of `u₁₂`, `u₂₃`, `u₁₃` by any choice of cones. -/
+
+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₃')
+    (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
+  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₂₃])
+  have eq₁₂ := iso₁₂.hom.comm₂
+  have eq₁₂' := iso₁₂.hom.comm₃
+  have eq₁₃ := iso₁₃.hom.comm₂
+  have eq₁₃' := iso₁₃.hom.comm₃
+  have eq₂₃ := iso₂₃.hom.comm₂
+  have eq₂₃' := iso₂₃.hom.comm₃
+  have rel₁₂ := H.triangleMorphism₁.comm₂
+  have rel₁₃ := H.triangleMorphism₁.comm₃
+  have rel₂₂ := H.triangleMorphism₂.comm₂
+  have rel₂₃ := H.triangleMorphism₂.comm₃
+  dsimp at eq₁₂ eq₁₂' eq₁₃ eq₁₃' eq₂₃ eq₂₃' rel₁₂ rel₁₃ rel₂₂ rel₂₃
+  rw [Functor.map_id, comp_id] at rel₁₃
+  rw [id_comp] at rel₂₂
+  refine' ⟨iso₁₂.hom.hom₃ ≫ H.m₁ ≫ iso₁₃.inv.hom₃,
+    iso₁₃.hom.hom₃ ≫ H.m₃ ≫ iso₂₃.inv.hom₃, _, _, _, _, _⟩
+  · rw [reassoc_of% eq₁₂, ← cancel_mono iso₁₃.hom.hom₃, assoc, assoc, assoc, assoc,
+      iso₁₃.inv_hom_id_triangle_hom₃, eq₁₃, reassoc_of% comm₂₃, ← rel₁₂]
+    dsimp
+    rw [comp_id]
+  · rw [← cancel_mono (e₁.hom⟦(1 : ℤ)⟧'), eq₁₂', assoc, assoc, assoc, eq₁₃',
+      iso₁₃.inv_hom_id_triangle_hom₃_assoc, ← rel₁₃]
+  · rw [reassoc_of% eq₁₃, reassoc_of% rel₂₂, ← cancel_mono iso₂₃.hom.hom₃, assoc, assoc,
+      iso₂₃.inv_hom_id_triangle_hom₃, eq₂₃]
+    dsimp
+    rw [comp_id]
+  · rw [← cancel_mono (e₂.hom⟦(1 : ℤ)⟧'), assoc, assoc, assoc,assoc, eq₂₃',
+      iso₂₃.inv_hom_id_triangle_hom₃_assoc, ← rel₂₃, ← Functor.map_comp, comm₁₂,
+      Functor.map_comp, reassoc_of% eq₁₃']
+  · refine' isomorphic_distinguished _ H.mem _ _
+    refine' Triangle.isoMk _ _ (Triangle.π₃.mapIso iso₁₂) (Triangle.π₃.mapIso iso₁₃)
+      (Triangle.π₃.mapIso iso₂₃) (by simp) (by simp) _
+    · dsimp
+      rw [assoc, ← Functor.map_comp, eq₁₂, Functor.map_comp, reassoc_of% eq₂₃']
+
 end Octahedron
 
 end Triangulated
@@ -158,4 +207,25 @@ def someOctahedron [IsTriangulated C]
 
 end Triangulated
 
+variable {C}
+
+/-- Constructor for `IsTriangulated C` which shows that it suffices to obtain an octahedron
+for a suitable isomorphic diagram instead of the given diagram. -/
+lemma IsTriangulated.mk' (h : ∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃'),
+    ∃ (X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C) (u₁₂ : X₁ ⟶ X₂) (u₂₃ : X₂ ⟶ X₃) (e₁ : X₁' ≅ X₁) (e₂ : X₂' ≅ X₂)
+    (e₃ : X₃' ≅ X₃) (_ : u₁₂' ≫ e₂.hom = e₁.hom ≫ u₁₂)
+    (_ : 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),
+        Nonempty (Octahedron rfl h₁₂ h₂₃ h₁₃)) :
+    IsTriangulated C where
+  octahedron_axiom {X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' u₁₂' u₂₃' u₁₃'} comm'
+    {v₁₂' w₁₂'} h₁₂' {v₂₃' w₂₃'} h₂₃' {v₁₃' w₁₃'} h₁₃' := by
+    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⟩
+
 end CategoryTheory