ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ ↑(dNext k₀) hom + ↑(prevD k₀) hom = hom k₀ k₁ ≫ d D k₁ k₀
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ Hom.f (nullHomotopicMap hom) k₀ = hom k₀ k₁ ≫ d D k₁ k₀
dsimp only [nullHomotopicMap]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c k₀ (ComplexShape.next c k₀)
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ ↑(dNext k₀) hom + ↑(prevD k₀) hom = hom k₀ k₁ ≫ d D k₁ k₀
rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]
no goals
case a
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c k₀ (ComplexShape.next c k₀)
exact hk₀ _