ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ Exact (d X 1 0) (HomologicalComplex.Hom.f f 0)
rw [Preadditive.exact_iff_homology_zero]
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
have h : X.d 1 0 ≫ f.f 0 = 0 := by
  simp only [← f.2 1 0 rfl, ChainComplex.single₀_obj_X_d, comp_zero]
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ kernel (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h) ≅ 0
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
refine' ⟨h, Nonempty.intro (homologyIsoKernelDesc _ _ _ ≪≫ _)⟩
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h)
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ kernel (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h) ≅ 0
suffices IsIso (cokernel.desc _ _ h) by apply kernel.ofMono
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (toSingle₀CokernelAtZeroIso f).hom
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h)
rw [← toSingle₀CokernelAtZeroIso_hom_eq]
no goals
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (toSingle₀CokernelAtZeroIso f).hom
infer_instance
no goals
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
simp only [← f.2 1 0 rfl, ChainComplex.single₀_obj_X_d, comp_zero]
no goals
ι : Type ?u.46272
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 : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
this : IsIso (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h)
⊢ kernel (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h) ≅ 0
apply kernel.ofMono