feat(CategoryTheory): a product of distinguished triangles is disting…

…uished (#7641)

Mathlib/CategoryTheory/Triangulated/Basic.lean

@@ -3,7 +3,8 @@ Copyright (c) 2021 Luke Kershaw. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Kershaw
 -/
-import Mathlib.Data.Int.Basic
+import Mathlib.CategoryTheory.Adjunction.Limits
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
 import Mathlib.CategoryTheory.Shift.Basic
 
@@ -193,6 +194,12 @@ def Triangle.isoMk (A B : Triangle C)
       Functor.map_id, Category.comp_id])
 #align category_theory.pretriangulated.triangle.iso_mk CategoryTheory.Pretriangulated.Triangle.isoMk
 
+lemma Triangle.isIso_of_isIsos {A B : Triangle C} (f : A ⟶ B)
+    (h₁ : IsIso f.hom₁) (h₂ : IsIso f.hom₂) (h₃ : IsIso f.hom₃) : IsIso f := by
+  let e := Triangle.isoMk A B (asIso f.hom₁) (asIso f.hom₂) (asIso f.hom₃)
+    (by simp) (by simp) (by simp)
+  exact (inferInstance : IsIso e.hom)
+
 lemma Triangle.eqToHom_hom₁ {A B : Triangle C} (h : A = B) :
     (eqToHom h).hom₁ = eqToHom (by subst h; rfl) := by subst h; rfl
 lemma Triangle.eqToHom_hom₂ {A B : Triangle C} (h : A = B) :
@@ -221,4 +228,70 @@ def binaryProductTriangleIsoBinaryBiproductTriangle
   Triangle.isoMk _ _ (Iso.refl _) (biprod.isoProd X₁ X₂).symm (Iso.refl _)
     (by aesop_cat) (by aesop_cat) (by aesop_cat)
 
+section
+
+variable {J : Type*} (T : J → Triangle C)
+  [HasProduct (fun j => (T j).obj₁)] [HasProduct (fun j => (T j).obj₂)]
+  [HasProduct (fun j => (T j).obj₃)] [HasProduct (fun j => (T j).obj₁⟦(1 : ℤ)⟧)]
+
+/-- The product of a family of triangles. -/
+@[simps!]
+def productTriangle : Triangle C :=
+  Triangle.mk (Pi.map (fun j => (T j).mor₁))
+    (Pi.map (fun j => (T j).mor₂))
+    (Pi.map (fun j => (T j).mor₃) ≫ inv (piComparison _ _))
+
+/-- A projection from the product of a family of triangles. -/
+@[simps]
+def productTriangle.π (j : J) :
+    productTriangle T ⟶ T j where
+  hom₁ := Pi.π _ j
+  hom₂ := Pi.π _ j
+  hom₃ := Pi.π _ j
+  comm₃ := by
+    dsimp
+    rw [← piComparison_comp_π, assoc, IsIso.inv_hom_id_assoc]
+    simp only [limMap_π, Discrete.natTrans_app]
+
+/-- The fan given by `productTriangle T`. -/
+@[simp]
+def productTriangle.fan : Fan T := Fan.mk (productTriangle T) (productTriangle.π T)
+
+/-- A family of morphisms `T' ⟶ T j` lifts to a morphism `T' ⟶ productTriangle T`. -/
+@[simps]
+def productTriangle.lift {T' : Triangle C} (φ : ∀ j, T' ⟶ T j) :
+    T' ⟶ productTriangle T where
+  hom₁ := Pi.lift (fun j => (φ j).hom₁)
+  hom₂ := Pi.lift (fun j => (φ j).hom₂)
+  hom₃ := Pi.lift (fun j => (φ j).hom₃)
+  comm₃ := by
+    dsimp
+    rw [← cancel_mono (piComparison _ _), assoc, assoc, assoc, IsIso.inv_hom_id, comp_id]
+    aesop_cat
+
+/-- The triangle `productTriangle T` satisfies the universal property of the categorical
+product of the triangles `T`. -/
+def productTriangle.isLimitFan : IsLimit (productTriangle.fan T) :=
+  mkFanLimit _ (fun s => productTriangle.lift T s.proj) (fun s j => by aesop_cat) (by
+    intro s m hm
+    ext1
+    all_goals
+      exact Pi.hom_ext _ _ (fun j => (by simp [← hm])))
+
+lemma productTriangle.zero₃₁ [HasZeroMorphisms C]
+    (h : ∀ j, (T j).mor₃ ≫ (T j).mor₁⟦(1 : ℤ)⟧' = 0) :
+    (productTriangle T).mor₃ ≫ (productTriangle T).mor₁⟦1⟧' = 0 := by
+  have : HasProduct (fun j => (T j).obj₂⟦(1 : ℤ)⟧) :=
+    ⟨_, isLimitFanMkObjOfIsLimit (shiftFunctor C (1 : ℤ)) _ _
+      (productIsProduct (fun j => (T j).obj₂))⟩
+  dsimp
+  change _ ≫ (Pi.lift (fun j => Pi.π _ j ≫ (T j).mor₁))⟦(1 : ℤ)⟧' = 0
+  rw [assoc, ← cancel_mono (piComparison _ _), zero_comp, assoc, assoc]
+  ext j
+  simp only [map_lift_piComparison, assoc, limit.lift_π, Fan.mk_π_app, zero_comp,
+    Functor.map_comp, ← piComparison_comp_π_assoc, IsIso.inv_hom_id_assoc,
+    limMap_π_assoc, Discrete.natTrans_app, h j, comp_zero]
+
+end
+
 end CategoryTheory.Pretriangulated

Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

@@ -531,6 +531,90 @@ lemma binaryProductTriangle_distinguished (X₁ X₂ : C) :
   isomorphic_distinguished _ (binaryBiproductTriangle_distinguished X₁ X₂) _
     (binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂)
 
+/-- A chosen extension of a commutative square into a morphism of distinguished triangles. -/
+@[simps hom₁ hom₂]
+def completeDistinguishedTriangleMorphism (T₁ T₂ : Triangle C)
+    (hT₁ : T₁ ∈ distTriang C) (hT₂ : T₂ ∈ distTriang C)
+    (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁) :
+    T₁ ⟶ T₂ :=
+    have h := complete_distinguished_triangle_morphism _ _ hT₁ hT₂ a b comm
+    { hom₁ := a
+      hom₂ := b
+      hom₃ := h.choose
+      comm₁ := comm
+      comm₂ := h.choose_spec.1
+      comm₃ := h.choose_spec.2 }
+
+/-- A product of distinguished triangles is distinguished -/
+lemma productTriangle_distinguished {J : Type*} (T : J → Triangle C)
+    (hT : ∀ j, T j ∈ distTriang C)
+    [HasProduct (fun j => (T j).obj₁)] [HasProduct (fun j => (T j).obj₂)]
+    [HasProduct (fun j => (T j).obj₃)] [HasProduct (fun j => (T j).obj₁⟦(1 : ℤ)⟧)] :
+    productTriangle T ∈ distTriang C := by
+  /- The proof proceeds by constructing a morphism of triangles
+    `φ' : T' ⟶ productTriangle T` with `T'` distinguished, and such that
+    `φ'.hom₁` and `φ'.hom₂` are identities. Then, it suffices to show that
+    `φ'.hom₃` is an isomorphism, which is achieved by using Yoneda's lemma
+    and diagram chases. -/
+  let f₁ := Pi.map (fun j => (T j).mor₁)
+  obtain ⟨Z, f₂, f₃, hT'⟩ := distinguished_cocone_triangle f₁
+  let T' := Triangle.mk f₁ f₂ f₃
+  change T' ∈ distTriang C at hT'
+  let φ : ∀ j, T' ⟶ T j := fun j => completeDistinguishedTriangleMorphism _ _
+    hT' (hT j) (Pi.π _ j) (Pi.π _ j) (by simp)
+  let φ' := productTriangle.lift _ φ
+  have h₁ : φ'.hom₁ = 𝟙 _ := by aesop_cat
+  have h₂ : φ'.hom₂ = 𝟙 _ := by aesop_cat
+  have : IsIso φ'.hom₁ := by rw [h₁]; infer_instance
+  have : IsIso φ'.hom₂ := by rw [h₂]; infer_instance
+  suffices IsIso φ'.hom₃ by
+    have : IsIso φ' := by
+      apply Triangle.isIso_of_isIsos
+      all_goals infer_instance
+    exact isomorphic_distinguished _ hT' _ (asIso φ').symm
+  refine' isIso_of_yoneda_map_bijective _ (fun A => ⟨_, _⟩)
+  /- the proofs by diagram chase start here -/
+  · suffices Mono φ'.hom₃ by
+      intro a₁ a₂ ha
+      simpa only [← cancel_mono φ'.hom₃] using ha
+    rw [mono_iff_cancel_zero]
+    intro A f hf
+    have hf' : f ≫ T'.mor₃ = 0 := by
+      rw [← cancel_mono (φ'.hom₁⟦1⟧'), zero_comp, assoc, φ'.comm₃, reassoc_of% hf, zero_comp]
+    obtain ⟨g, hg⟩ := T'.coyoneda_exact₃ hT' f hf'
+    have hg' : ∀ j, (g ≫ Pi.π _ j) ≫ (T j).mor₂ = 0 := fun j => by
+      have : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π _ j = 0 :=
+        by rw [← reassoc_of% hg, reassoc_of% hf, zero_comp]
+      rw [φ'.comm₂_assoc, h₂, id_comp] at this
+      simpa using this
+    have hg'' := fun j => (T j).coyoneda_exact₂ (hT j) _ (hg' j)
+    let α := fun j => (hg'' j).choose
+    have hα : ∀ j, _ = α j ≫ _ := fun j => (hg'' j).choose_spec
+    have hg''' : g = Pi.lift α ≫ T'.mor₁ := by dsimp; ext j; rw [hα]; simp
+    rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]
+  · intro a
+    obtain ⟨a', ha'⟩ : ∃ (a' : A ⟶ Z), a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃ := by
+      have zero : ((productTriangle T).mor₃) ≫ (shiftFunctor C 1).map T'.mor₁ = 0 := by
+        rw [← cancel_mono (φ'.hom₂⟦1⟧'), zero_comp, assoc, ← Functor.map_comp, φ'.comm₁, h₁,
+          id_comp, productTriangle.zero₃₁]
+        intro j
+        exact comp_distTriang_mor_zero₃₁ _ (hT j)
+      have ⟨g, hg⟩ := T'.coyoneda_exact₁ hT' (a ≫ (productTriangle T).mor₃) (by
+        rw [assoc, zero, comp_zero])
+      exact ⟨g, hg.symm⟩
+    have ha'' := fun (j : J) => (T j).coyoneda_exact₃ (hT j) ((a - a' ≫ φ'.hom₃) ≫ Pi.π _ j) (by
+      simp only [sub_comp, assoc]
+      erw [← (productTriangle.π T j).comm₃]
+      rw [← φ'.comm₃_assoc]
+      rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_comp])
+    let b := fun j => (ha'' j).choose
+    have hb : ∀ j, _  = b j ≫ _ := fun j => (ha'' j).choose_spec
+    have hb' : a - a' ≫ φ'.hom₃ = Pi.lift b ≫ (productTriangle T).mor₂ :=
+      Limits.Pi.hom_ext _ _ (fun j => by rw [hb]; simp)
+    have : (a' + (by exact Pi.lift b) ≫ T'.mor₂) ≫ φ'.hom₃ = a := by
+      rw [add_comp, assoc, φ'.comm₂, h₂, id_comp, ← hb', add_sub_cancel'_right]
+    exact ⟨_, this⟩
+
 end Pretriangulated
 
 end CategoryTheory