ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i j'
⊢ kernelSubobject (d C i j' ≫ eqToHom (_ : X C j' = X C j)) = kernelSubobject (d C i j')
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i j'
⊢ kernelSubobject (d C i j) = kernelSubobject (d C i j')
rw [← d_comp_eqToHom C r r']
no goals
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i j'
⊢ kernelSubobject (d C i j' ≫ eqToHom (_ : X C j' = X C j)) = kernelSubobject (d C i j')
apply kernelSubobject_comp_mono