ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ⊤ ≤ cycles C i
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ cycles C i = ⊤
rw [eq_top_iff]
case h
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ Subobject.arrow ⊤ ≫ dFrom C i = 0
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ⊤ ≤ cycles C i
apply le_kernelSubobject
no goals
case h
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ Subobject.arrow ⊤ ≫ dFrom C i = 0
rw [C.dFrom_eq_zero h, comp_zero]