ι : 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 l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ ↑(dNext k₁) hom + ↑(prevD k₁) hom = d C k₁ k₀ ≫ hom 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 l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ Hom.f (nullHomotopicMap hom) k₁ = d C k₁ k₀ ≫ hom 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 l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c (ComplexShape.prev c 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 l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ ↑(dNext k₁) hom + ↑(prevD k₁) hom = d C k₁ k₀ ≫ hom k₀ k₁
rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]
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 l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c (ComplexShape.prev c k₁) k₁
exact hk₁ _