From 80f7a578cb083033cce0f4ef0910557aaf397506 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 28 Mar 2023 23:33:53 +0000
Subject: [PATCH] feat(category_theory/idempotents): idempotent completeness of
 homological_complex (#17921)

---
 src/algebra/homology/additive.lean            | 37 +++++++++++++++++++
 .../idempotents/homological_complex.lean      | 13 ++++++-
 src/category_theory/idempotents/karoubi.lean  |  8 ++++
 3 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/src/algebra/homology/additive.lean b/src/algebra/homology/additive.lean
index 2d2d5662d2939..9ecd5b5fab41d 100644
--- a/src/algebra/homology/additive.lean
+++ b/src/algebra/homology/additive.lean
@@ -107,6 +107,17 @@ def functor.map_homological_complex (F : V ⥤ W) [F.additive] (c : complex_shap
   { f := λ i, F.map (f.f i),
     comm' := λ i j h, by { dsimp,  rw [←F.map_comp, ←F.map_comp, f.comm], }, }, }.
 
+variable (V)
+
+/-- The functor on homological complexes induced by the identity functor is
+isomorphic to the identity functor. -/
+@[simps]
+def functor.map_homological_complex_id_iso (c : complex_shape ι) :
+  (𝟭 V).map_homological_complex c ≅ 𝟭 _ :=
+nat_iso.of_components (λ K, hom.iso_of_components (λ i, iso.refl _) (by tidy)) (by tidy)
+
+variable {V}
+
 instance functor.map_homogical_complex_additive
   (F : V ⥤ W) [F.additive] (c : complex_shape ι) : (F.map_homological_complex c).additive := {}
 
@@ -147,6 +158,32 @@ by tidy
     (nat_trans.map_homological_complex α c).app C ≫ (G.map_homological_complex c).map f :=
 by tidy
 
+/--
+A natural isomorphism between functors induces a natural isomorphism
+between those functors applied to homological complexes.
+-/
+@[simps]
+def nat_iso.map_homological_complex {F G : V ⥤ W} [F.additive] [G.additive]
+  (α : F ≅ G) (c : complex_shape ι) : F.map_homological_complex c ≅ G.map_homological_complex c :=
+{ hom := α.hom.map_homological_complex c,
+  inv := α.inv.map_homological_complex c,
+  hom_inv_id' := by simpa only [← nat_trans.map_homological_complex_comp, α.hom_inv_id],
+  inv_hom_id' := by simpa only [← nat_trans.map_homological_complex_comp, α.inv_hom_id], }
+
+/--
+An equivalence of categories induces an equivalences between the respective categories
+of homological complex.
+-/
+@[simps]
+def equivalence.map_homological_complex (e : V ≌ W) [e.functor.additive] (c : complex_shape ι):
+  homological_complex V c ≌ homological_complex W c :=
+{ functor := e.functor.map_homological_complex c,
+  inverse := e.inverse.map_homological_complex c,
+  unit_iso := (functor.map_homological_complex_id_iso V c).symm ≪≫
+    nat_iso.map_homological_complex e.unit_iso c,
+  counit_iso := nat_iso.map_homological_complex e.counit_iso c ≪≫
+    functor.map_homological_complex_id_iso W c, }
+
 end category_theory
 
 namespace chain_complex
diff --git a/src/category_theory/idempotents/homological_complex.lean b/src/category_theory/idempotents/homological_complex.lean
index 5db952eacb7aa..ebc8a609b0b24 100644
--- a/src/category_theory/idempotents/homological_complex.lean
+++ b/src/category_theory/idempotents/homological_complex.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 
-import algebra.homology.homological_complex
+import algebra.homology.additive
 import category_theory.idempotents.karoubi
 
 /-!
@@ -14,6 +14,9 @@ This file contains simplifications lemmas for categories
 `karoubi (homological_complex C c)` and the construction of an equivalence
 of categories `karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c`.
 
+When the category `C` is idempotent complete, it is shown that
+`homological_complex (karoubi C) c` is also idempotent complete.
+
 -/
 
 namespace category_theory
@@ -203,6 +206,14 @@ def karoubi_cochain_complex_equivalence :
   karoubi (cochain_complex C α) ≌ cochain_complex (karoubi C) α :=
 karoubi_homological_complex_equivalence C (complex_shape.up α)
 
+instance [is_idempotent_complete C] : is_idempotent_complete (homological_complex C c) :=
+begin
+  rw [is_idempotent_complete_iff_of_equivalence
+    ((to_karoubi_equivalence C).map_homological_complex c),
+    ← is_idempotent_complete_iff_of_equivalence (karoubi_homological_complex_equivalence C c)],
+  apply_instance,
+end
+
 end idempotents
 
 end category_theory
diff --git a/src/category_theory/idempotents/karoubi.lean b/src/category_theory/idempotents/karoubi.lean
index ec19521b7a1b3..16fc6fd644f28 100644
--- a/src/category_theory/idempotents/karoubi.lean
+++ b/src/category_theory/idempotents/karoubi.lean
@@ -209,6 +209,14 @@ def to_karoubi_is_equivalence [is_idempotent_complete C] :
   is_equivalence (to_karoubi C) :=
 equivalence.of_fully_faithfully_ess_surj (to_karoubi C)
 
+/-- The equivalence `C ≅ karoubi C` when `C` is idempotent complete. -/
+def to_karoubi_equivalence [is_idempotent_complete C] : C ≌ karoubi C :=
+by { haveI := to_karoubi_is_equivalence C, exact functor.as_equivalence (to_karoubi C), }
+
+instance to_karoubi_equivalence_functor_additive
+  [preadditive C] [is_idempotent_complete C] :
+  (to_karoubi_equivalence C).functor.additive := (infer_instance : (to_karoubi C).additive)
+
 namespace karoubi
 
 variables {C}