ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ Exact (HomologicalComplex.Hom.f f 0) (d X 0 1)
rw [Preadditive.exact_iff_homology_zero]
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
have h : f.f 0 ≫ X.d 0 1 = 0 := by
  simp only [HomologicalComplex.Hom.comm, CochainComplex.single₀_obj_X_d, zero_comp]
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ cokernel (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h) ≅ 0
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
refine' ⟨h, Nonempty.intro (homologyIsoCokernelLift _ _ _ ≪≫ _)⟩
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h)
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ cokernel (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h) ≅ 0
suffices IsIso (kernel.lift (X.d 0 1) (f.f 0) h) by apply cokernel.ofEpi
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (fromSingle₀KernelAtZeroIso f).inv
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h)
rw [← fromSingle₀KernelAtZeroIso_inv_eq f]
no goals
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (fromSingle₀KernelAtZeroIso f).inv
infer_instance
no goals
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
simp only [HomologicalComplex.Hom.comm, CochainComplex.single₀_obj_X_d, zero_comp]
no goals
ι : Type ?u.92227
V : Type u
inst✝⁸ : Category V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
this : IsIso (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h)
⊢ cokernel (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h) ≅ 0
apply cokernel.ofEpi