feat(Algebra/Homology/HomotopyCategory): various prerequisites for th…

…e triangulated structure (#9592)

This PR adds various small prerequisites for the construction of the triangulated structure on the homotopy category of cochain complexes.

Mathlib/Algebra/Homology/HomotopyCategory.lean

@@ -77,10 +77,13 @@ instance : (quotient V c).Additive where
 
 open ZeroObject
 
--- TODO upgrade this to `HasZeroObject`, presumably for any `quotient`.
 instance [HasZeroObject V] : Inhabited (HomotopyCategory V c) :=
   ⟨(quotient V c).obj 0⟩
 
+instance [HasZeroObject V] : HasZeroObject (HomotopyCategory V c) :=
+  ⟨(quotient V c).obj 0, by
+    rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]⟩
+
 variable {V c}
 
 -- porting note: removed @[simp] attribute because it hinders the automatic application of the
@@ -151,6 +154,15 @@ def homotopyEquivOfIso {C D : HomologicalComplex V c}
       (by rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id])
 #align homotopy_category.homotopy_equiv_of_iso HomotopyCategory.homotopyEquivOfIso
 
+lemma isZero_quotient_obj_iff (C : HomologicalComplex V c) :
+    IsZero ((quotient _ _).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0) := by
+  rw [IsZero.iff_id_eq_zero]
+  constructor
+  · intro h
+    exact ⟨(homotopyOfEq _ _ (by simp [h]))⟩
+  · rintro ⟨h⟩
+    simpa using (eq_of_homotopy _ _ h)
+
 variable (V c)
 
 section

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -556,6 +556,7 @@ lemma δ_neg_one_cochain (z : Cochain F G (-1)) :
   rw [Homotopy.nullHomotopicMap'_f (show (ComplexShape.up ℤ).Rel (p-1) p by simp)
     (show (ComplexShape.up ℤ).Rel p (p+1) by simp)]
   abel
+
 end HomComplex
 
 variable (F G)
@@ -628,6 +629,10 @@ lemma coe_neg (z : Cocycle F G n) :
 lemma coe_smul (z : Cocycle F G n) (x : R) :
     (↑(x • z) : Cochain F G n) = x • (z : Cochain F G n) := rfl
 
+@[simp]
+lemma coe_units_smul (z : Cocycle F G n) (x : Rˣ) :
+    (↑(x • z) : Cochain F G n) = x • (z : Cochain F G n) := rfl
+
 @[simp]
 lemma coe_sub (z₁ z₂ : Cocycle F G n) :
     (↑(z₁ - z₂) : Cochain F G n) = (z₁ : Cochain F G n) - (z₂ : Cochain F G n) := rfl
@@ -703,10 +708,39 @@ def diff : Cocycle K K 1 :=
 
 end Cocycle
 
-namespace Cochain
-
 variable {F G}
 
+@[simp]
+lemma δ_comp_zero_cocycle {n : ℤ} (z₁ : Cochain F G n) (z₂ : Cocycle G K 0) (m : ℤ) :
+    δ n m (z₁.comp z₂.1 (add_zero n)) =
+      (δ n m z₁).comp z₂.1 (add_zero m) := by
+  by_cases hnm : n + 1 = m
+  · simp [δ_comp_zero_cochain _ _ _ hnm]
+  · simp [δ_shape _ _ hnm]
+
+@[simp]
+lemma δ_comp_ofHom {n : ℤ} (z₁ : Cochain F G n) (f : G ⟶ K) (m : ℤ) :
+    δ n m (z₁.comp (Cochain.ofHom f) (add_zero n)) =
+      (δ n m z₁).comp (Cochain.ofHom f) (add_zero m) := by
+  rw [← Cocycle.ofHom_coe, δ_comp_zero_cocycle]
+
+
+@[simp]
+lemma δ_zero_cocycle_comp {n : ℤ} (z₁ : Cocycle F G 0) (z₂ : Cochain G K n) (m : ℤ) :
+    δ n m (z₁.1.comp z₂ (zero_add n)) =
+      z₁.1.comp (δ n m z₂) (zero_add m) := by
+  by_cases hnm : n + 1 = m
+  · simp [δ_zero_cochain_comp _ _ _ hnm]
+  · simp [δ_shape _ _ hnm]
+
+@[simp]
+lemma δ_ofHom_comp {n : ℤ} (f : F ⟶ G) (z : Cochain G K n) (m : ℤ) :
+    δ n m ((Cochain.ofHom f).comp z (zero_add n)) =
+      (Cochain.ofHom f).comp (δ n m z) (zero_add m) := by
+  rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]
+
+namespace Cochain
+
 /-- Given two morphisms of complexes `φ₁ φ₂ : F ⟶ G`, the datum of an homotopy between `φ₁` and
 `φ₂` is equivalent to the datum of a `1`-cochain `z` such that `δ (-1) 0 z` is the difference
 of the zero cochains associated to `φ₂` and `φ₁`. -/

Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean

@@ -400,7 +400,7 @@ lemma δ_rightShift (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a =
       add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp, smul_add,
       add_right_inj, smul_smul]
     congr 1
-    rw [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc,
+    simp only [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc,
       Int.units_mul_self, one_mul]
   · have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by linarith)
     rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_zero, smul_zero]

Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean

@@ -105,9 +105,13 @@ instance (n : ℤ) :
 
 variable {C}
 
+@[simp]
+lemma shiftFunctor_obj_X' (K : CochainComplex C ℤ) (n p : ℤ) :
+    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X p = K.X (p + n) := rfl
+
 @[simp]
 lemma shiftFunctor_map_f' {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n p : ℤ) :
-    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p+n) := rfl
+    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p + n) := rfl
 
 @[simp]
 lemma shiftFunctor_obj_d' (K : CochainComplex C ℤ) (n i j : ℤ) :
@@ -283,4 +287,9 @@ noncomputable instance commShiftQuotient :
     (HomotopyCategory.quotient C (ComplexShape.up ℤ)).CommShift ℤ :=
   Quotient.functor_commShift (homotopic C (ComplexShape.up ℤ)) ℤ
 
+instance (n : ℤ) : (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive := by
+  have : ((quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor _ n)).Additive :=
+    Functor.additive_of_iso ((quotient C (ComplexShape.up ℤ)).commShiftIso n)
+  apply Functor.additive_of_full_essSurj_comp (quotient _ _ )
+
 end HomotopyCategory

Mathlib/CategoryTheory/Triangulated/Basic.lean

@@ -162,6 +162,23 @@ lemma Triangle.hom_ext {A B : Triangle C} (f g : A ⟶ B)
     (h₁ : f.hom₁ = g.hom₁) (h₂ : f.hom₂ = g.hom₂) (h₃ : f.hom₃ = g.hom₃) : f = g :=
   TriangleMorphism.ext _ _ h₁ h₂ h₃
 
+@[simp]
+lemma id_hom₁ (A : Triangle C) : TriangleMorphism.hom₁ (𝟙 A) = 𝟙 _ := rfl
+@[simp]
+lemma id_hom₂ (A : Triangle C) : TriangleMorphism.hom₂ (𝟙 A) = 𝟙 _ := rfl
+@[simp]
+lemma id_hom₃ (A : Triangle C) : TriangleMorphism.hom₃ (𝟙 A) = 𝟙 _ := rfl
+
+@[simp, reassoc]
+lemma comp_hom₁ {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).hom₁ = f.hom₁ ≫ g.hom₁ := rfl
+@[simp, reassoc]
+lemma comp_hom₂ {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).hom₂ = f.hom₂ ≫ g.hom₂ := rfl
+@[simp, reassoc]
+lemma comp_hom₃ {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (f ≫ g).hom₃ = f.hom₃ ≫ g.hom₃ := rfl
+
 @[simps]
 def Triangle.homMk (A B : Triangle C)
     (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃)
@@ -200,6 +217,26 @@ lemma Triangle.isIso_of_isIsos {A B : Triangle C} (f : A ⟶ B)
     (by simp) (by simp) (by simp)
   exact (inferInstance : IsIso e.hom)
 
+@[reassoc (attr := simp)]
+lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₁ {A B : Triangle C} (e : A ≅ B) :
+    e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 _ := by rw [← comp_hom₁, e.hom_inv_id, id_hom₁]
+@[reassoc (attr := simp)]
+lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₂ {A B : Triangle C} (e : A ≅ B) :
+    e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 _ := by rw [← comp_hom₂, e.hom_inv_id, id_hom₂]
+@[reassoc (attr := simp)]
+lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₃ {A B : Triangle C} (e : A ≅ B) :
+    e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 _ := by rw [← comp_hom₃, e.hom_inv_id, id_hom₃]
+
+@[reassoc (attr := simp)]
+lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₁ {A B : Triangle C} (e : A ≅ B) :
+    e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 _ := by rw [← comp_hom₁, e.inv_hom_id, id_hom₁]
+@[reassoc (attr := simp)]
+lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₂ {A B : Triangle C} (e : A ≅ B) :
+    e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 _ := by rw [← comp_hom₂, e.inv_hom_id, id_hom₂]
+@[reassoc (attr := simp)]
+lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₃ {A B : Triangle C} (e : A ≅ B) :
+    e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 _ := by rw [← comp_hom₃, e.inv_hom_id, id_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) :