ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i' j
⊢ imageSubobject (eqToHom (_ : X C i = X C i') ≫ d C i' j) = imageSubobject (d C i' j)
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i' j
⊢ imageSubobject (d C i j) = imageSubobject (d C i' j)
rw [← eqToHom_comp_d C r r']
no goals
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i' j
⊢ imageSubobject (eqToHom (_ : X C i = X C i') ≫ d C i' j) = imageSubobject (d C i' j)
apply imageSubobject_iso_comp