ι : 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✝ f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)) =
    Subobject.factorThru (cycles C₂ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₂ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)) ≫
      Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g 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✝ f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ cyclesMap (f ≫ g) i = cyclesMap f i ≫ cyclesMap g 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✝ f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)) =
    Subobject.factorThru (cycles C₂ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₂ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)) ≫
      Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g i))
simp [Subobject.factorThru_right]