# Documentation

Mathlib.Algebra.Homology.ShortComplex.QuasiIso

# Quasi-isomorphisms of short complexes #

This file introduces the typeclass QuasiIso φ for a morphism φ : S₁ ⟶ S₂ of short complexes (which have homology): the condition is that the induced morphism homologyMap φ in homology is an isomorphism.

class CategoryTheory.ShortComplex.QuasiIso {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :

A morphism φ : S₁ ⟶ S₂ of short complexes that have homology is a quasi-isomorphism if the induced map homologyMap φ : S₁.homology ⟶ S₂.homology is an isomorphism.

• the homology map is an isomorphism

Instances
Equations
instance CategoryTheory.ShortComplex.quasiIso_of_isIso {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
Equations
instance CategoryTheory.ShortComplex.quasiIso_comp {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ : S₁ S₂) (φ' : S₂ S₃) [hφ' : ] :
Equations
theorem CategoryTheory.ShortComplex.quasiIso_of_comp_left {C : Type u_2} [] {S₁ : } {S₂ : } {S₃ : } (φ : S₁ S₂) (φ' : S₂ S₃) :
theorem CategoryTheory.ShortComplex.quasiIso_iff_comp_left {C : Type u_2} [] {S₁ : } {S₂ : } {S₃ : } (φ : S₁ S₂) (φ' : S₂ S₃) :
theorem CategoryTheory.ShortComplex.quasiIso_of_comp_right {C : Type u_2} [] {S₁ : } {S₂ : } {S₃ : } (φ : S₁ S₂) (φ' : S₂ S₃) [hφ' : ] :
theorem CategoryTheory.ShortComplex.quasiIso_iff_comp_right {C : Type u_2} [] {S₁ : } {S₂ : } {S₃ : } (φ : S₁ S₂) (φ' : S₂ S₃) [hφ' : ] :
theorem CategoryTheory.ShortComplex.quasiIso_of_arrow_mk_iso {C : Type u_2} [] {S₁ : } {S₂ : } {S₃ : } {S₄ : } (φ : S₁ S₂) (φ' : S₃ S₄) (e : ) :
theorem CategoryTheory.ShortComplex.quasiIso_iff_of_arrow_mk_iso {C : Type u_2} [] {S₁ : } {S₂ : } {S₃ : } {S₄ : } (φ : S₁ S₂) (φ' : S₃ S₄) (e : ) :
theorem CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono {C : Type u_2} [] {S₁ : } {S₂ : } (φ : S₁ S₂) [] [] [] :
theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_liftCycles {C : Type u_2} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) :
theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_descOpcycles {C : Type u_2} [] {S₁ : } {S₂ : } (φ : S₁ S₂) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :