ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ boundaries C j ≤ ⊥
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ boundaries C j = ⊥
rw [eq_bot_iff]
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ 0 ≫ Subobject.arrow ⊥ = dTo C j
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ boundaries C j ≤ ⊥
refine' imageSubobject_le _ 0 _
no goals
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ 0 ≫ Subobject.arrow ⊥ = dTo C j
rw [C.dTo_eq_zero h, zero_comp]