ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ Subobject.factorThru (cycles C₁ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₁ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)) =
    𝟙 (Subobject.underlying.obj (cycles C₁ i))
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ cyclesMap (𝟙 C₁) i = 𝟙 (Subobject.underlying.obj (cycles C₁ i))
dsimp only [cyclesMap]
no goals
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ Subobject.factorThru (cycles C₁ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₁ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)) =
    𝟙 (Subobject.underlying.obj (cycles C₁ i))
simp