diff --git a/Mathlib.lean b/Mathlib.lean
index d1bb863d6c31b..1ed66e575d415 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -222,6 +222,7 @@ import Mathlib.Algebra.Homology.Opposite
 import Mathlib.Algebra.Homology.QuasiIso
 import Mathlib.Algebra.Homology.ShortComplex.Basic
 import Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
+import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
 import Mathlib.Algebra.Homology.ShortComplex.Homology
 import Mathlib.Algebra.Homology.ShortComplex.LeftHomology
 import Mathlib.Algebra.Homology.ShortComplex.RightHomology
diff --git a/Mathlib/Algebra/Homology/HomologicalComplex.lean b/Mathlib/Algebra/Homology/HomologicalComplex.lean
index c11aaceeaa0f2..218962429f461 100644
--- a/Mathlib/Algebra/Homology/HomologicalComplex.lean
+++ b/Mathlib/Algebra/Homology/HomologicalComplex.lean
@@ -92,6 +92,58 @@ theorem ext {C₁ C₂ : HomologicalComplex V c} (h_X : C₁.X = C₂.X)
   · rw [s₁ i j hij, s₂ i j hij]
 #align homological_complex.ext HomologicalComplex.ext
 
+/-- The obvious isomorphism `K.X p ≅ K.X q` when `p = q`. -/
+def XIsoOfEq (K : HomologicalComplex V c) {p q : ι} (h : p = q) :
+  K.X p ≅ K.X q := eqToIso (by rw [h])
+
+@[simp]
+lemma XIsoOfEq_rfl (K : HomologicalComplex V c) (p : ι) :
+  K.XIsoOfEq (rfl : p = p) = Iso.refl _ := rfl
+
+@[reassoc (attr := simp)]
+lemma XIsoOfEq_hom_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
+    (h₁₂ : p₁ = p₂) (h₂₃ : p₂ = p₃) :
+    (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq (h₁₂.trans h₂₃)).hom := by
+  dsimp [XIsoOfEq]
+  simp only [eqToHom_trans]
+
+@[reassoc (attr := simp)]
+lemma XIsoOfEq_hom_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
+    (h₁₂ : p₁ = p₂) (h₃₂ : p₃ = p₂) :
+    (K.XIsoOfEq h₁₂).hom ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq (h₁₂.trans h₃₂.symm)).hom := by
+  dsimp [XIsoOfEq]
+  simp only [eqToHom_trans]
+
+@[reassoc (attr := simp)]
+lemma XIsoOfEq_inv_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
+    (h₂₁ : p₂ = p₁) (h₂₃ : p₂ = p₃) :
+    (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₂₃).hom = (K.XIsoOfEq (h₂₁.symm.trans h₂₃)).hom := by
+  dsimp [XIsoOfEq]
+  simp only [eqToHom_trans]
+
+@[reassoc (attr := simp)]
+lemma XIsoOfEq_inv_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
+    (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) :
+    (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq (h₃₂.trans h₂₁).symm).hom := by
+  dsimp [XIsoOfEq]
+  simp only [eqToHom_trans]
+
+@[reassoc (attr := simp)]
+lemma XIsoOfEq_hom_comp_d (K : HomologicalComplex V c) {p₁ p₂ : ι} (h : p₁ = p₂) (p₃ : ι) :
+    (K.XIsoOfEq h).hom ≫ K.d p₂ p₃ = K.d p₁ p₃ := by subst h; simp
+
+@[reassoc (attr := simp)]
+lemma XIsoOfEq_inv_comp_d (K : HomologicalComplex V c) {p₂ p₁ : ι} (h : p₂ = p₁) (p₃ : ι) :
+    (K.XIsoOfEq h).inv ≫ K.d p₂ p₃ = K.d p₁ p₃ := by subst h; simp
+
+@[reassoc (attr := simp)]
+lemma d_comp_XIsoOfEq_hom (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₂ = p₃) (p₁ : ι) :
+    K.d p₁ p₂ ≫ (K.XIsoOfEq h).hom = K.d p₁ p₃ := by subst h; simp
+
+@[reassoc (attr := simp)]
+lemma d_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₂ p₃ : ι} (h : p₃ = p₂) (p₁ : ι) :
+    K.d p₁ p₂ ≫ (K.XIsoOfEq h).inv = K.d p₁ p₃ := by subst h; simp
+
 end HomologicalComplex
 
 /-- An `α`-indexed chain complex is a `HomologicalComplex`
diff --git a/Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean b/Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
new file mode 100644
index 0000000000000..d19936a8bfee7
--- /dev/null
+++ b/Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2023 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Homology.HomologicalComplex
+import Mathlib.Algebra.Homology.ShortComplex.Homology
+
+/-!
+# The short complexes attached to homological complexes
+
+In this file, we define a functor
+`shortComplexFunctor C c i : HomologicalComplex C c ⥤ ShortComplex C`.
+By definition, the image of a homological complex `K` by this functor
+is the short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`.
+
+When the homology refactor is completed (TODO @joelriou), the homology
+of a homological complex `K` in degree `i` shall be the homology
+of the short complex `(shortComplexFunctor C c i).obj K`, which can be
+abbreviated as `K.sc i`.
+
+-/
+
+open CategoryTheory Category Limits
+
+namespace HomologicalComplex
+
+variable (C : Type _) [Category C] [HasZeroMorphisms C] {ι : Type _} (c : ComplexShape ι)
+
+/-- The functor `HomologicalComplex C c ⥤ ShortComplex C` which sends a homological
+complex `K` to the short complex `K.X i ⟶ K.X j ⟶ K.X k` for arbitrary indices `i`, `j` and `k`. -/
+@[simps]
+def shortComplexFunctor' (i j k : ι) : HomologicalComplex C c ⥤ ShortComplex C where
+  obj K := ShortComplex.mk (K.d i j) (K.d j k) (K.d_comp_d i j k)
+  map f :=
+    { τ₁ := f.f i
+      τ₂ := f.f j
+      τ₃ := f.f k }
+
+/-- The functor `HomologicalComplex C c ⥤ ShortComplex C` which sends a homological
+complex `K` to the short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`. -/
+@[simps!]
+noncomputable def shortComplexFunctor (i : ι) :=
+  shortComplexFunctor' C c (c.prev i) i (c.next i)
+
+/-- The natural isomorphism `shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k`
+when `c.prev j = i` and `c.next j = k`. -/
+@[simps!]
+noncomputable def natIsoSc' (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) :
+    shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k :=
+  NatIso.ofComponents (fun K => ShortComplex.isoMk (K.XIsoOfEq hi) (Iso.refl _) (K.XIsoOfEq hk)
+    (by aesop_cat) (by aesop_cat)) (by aesop_cat)
+
+variable {C c}
+variable (K L M : HomologicalComplex C c) (φ : K ⟶ L) (ψ : L ⟶ M)
+
+/-- The short complex `K.X i ⟶ K.X j ⟶ K.X k` for arbitrary indices `i`, `j` and `k`. -/
+abbrev sc' (i j k : ι) := (shortComplexFunctor' C c i j k).obj K
+
+/-- The short complex `K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)`. -/
+noncomputable abbrev sc (i : ι) := (shortComplexFunctor C c i).obj K
+
+/-- The canonical isomorphism `K.sc j ≅ K.sc' i j k` when `c.prev j = i` and `c.next j = k`. -/
+noncomputable abbrev isoSc' (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) :
+    K.sc j ≅ K.sc' i j k := (natIsoSc' C c i j k hi hk).app K
+
+end HomologicalComplex