feat(algebra/homology): construct isomorphisms of complexes (#7741)

From LTE. 



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/homology/homological_complex.lean

@@ -415,6 +415,34 @@ end
 namespace hom
 
 variables {C₁ C₂ C₃ : homological_complex V c}
+
+/-- The `i`-th component of an isomorphism of chain complexes. -/
+@[simps]
+def iso_app (f : C₁ ≅ C₂) (i : ι) : C₁.X i ≅ C₂.X i :=
+(eval V c i).map_iso f
+
+/-- Construct an isomorphism of chain complexes from isomorphism of the objects
+which commute with the differentials. -/
+@[simps]
+def iso_of_components (f : Π i, C₁.X i ≅ C₂.X i)
+  (hf : ∀ i j, c.rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) :
+  C₁ ≅ C₂ :=
+{ hom := { f := λ i, (f i).hom, comm' := hf },
+  inv :=
+  { f := λ i, (f i).inv,
+    comm' := λ i j hij,
+    calc (f i).inv ≫ C₁.d i j
+        = (f i).inv ≫ (C₁.d i j ≫ (f j).hom) ≫ (f j).inv : by simp
+    ... = (f i).inv ≫ ((f i).hom ≫ C₂.d i j) ≫ (f j).inv : by rw hf i j hij
+    ... =  C₂.d i j ≫ (f j).inv : by simp },
+  hom_inv_id' := by { ext i, exact (f i).hom_inv_id },
+  inv_hom_id' := by { ext i, exact (f i).inv_hom_id } }
+
+@[simp] lemma iso_of_components_app (f : Π i, C₁.X i ≅ C₂.X i)
+  (hf : ∀ i j, c.rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) (i : ι) :
+  iso_app (iso_of_components f hf) i = f i :=
+by { ext, simp, }
+
 variables [has_zero_object V]
 open_locale zero_object