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} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) : Prop

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.

• isIso' : IsIso (homologyMap φ)

  the homology map is an isomorphism

instance CategoryTheory.ShortComplex.QuasiIso.isIso {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [QuasiIso φ] : IsIso (homologyMap φ)

theorem CategoryTheory.ShortComplex.quasiIso_iff {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) : QuasiIso φ ↔ IsIso (homologyMap φ)

instance CategoryTheory.ShortComplex.quasiIso_of_isIso {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [IsIso φ] : QuasiIso φ

instance CategoryTheory.ShortComplex.quasiIso_comp {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : QuasiIso φ] [hφ' : QuasiIso φ'] : QuasiIso (CategoryStruct.comp φ φ')

theorem CategoryTheory.ShortComplex.quasiIso_of_comp_left {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : QuasiIso φ] [hφφ' : QuasiIso (CategoryStruct.comp φ φ')] : QuasiIso φ'

theorem CategoryTheory.ShortComplex.quasiIso_iff_comp_left {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ : QuasiIso φ] : QuasiIso (CategoryStruct.comp φ φ') ↔ QuasiIso φ'

theorem CategoryTheory.ShortComplex.quasiIso_of_comp_right {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ' : QuasiIso φ'] [hφφ' : QuasiIso (CategoryStruct.comp φ φ')] : QuasiIso φ

theorem CategoryTheory.ShortComplex.quasiIso_iff_comp_right {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ' : QuasiIso φ'] : QuasiIso (CategoryStruct.comp φ φ') ↔ QuasiIso φ

theorem CategoryTheory.ShortComplex.quasiIso_of_arrow_mk_iso {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ S₄ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] [S₄.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₃ ⟶ S₄) (e : Arrow.mk φ ≅ Arrow.mk φ') [hφ : QuasiIso φ] : QuasiIso φ'

theorem CategoryTheory.ShortComplex.quasiIso_iff_of_arrow_mk_iso {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ S₄ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] [S₄.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₃ ⟶ S₄) (e : Arrow.mk φ ≅ Arrow.mk φ') : QuasiIso φ ↔ QuasiIso φ'

theorem CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : LeftHomologyMapData φ h₁ h₂) : QuasiIso φ ↔ IsIso γ.φH

theorem CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : RightHomologyMapData φ h₁ h₂) : QuasiIso φ ↔ IsIso γ.φH

theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_leftHomologyMap' {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) : QuasiIso φ ↔ IsIso (leftHomologyMap' φ h₁ h₂)

theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_rightHomologyMap' {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)

theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_homologyMap' {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) : QuasiIso φ ↔ IsIso (homologyMap' φ h₁ h₂)

theorem CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : QuasiIso φ

theorem CategoryTheory.ShortComplex.quasiIso_opMap_iff {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) : QuasiIso (opMap φ) ↔ QuasiIso φ

theorem CategoryTheory.ShortComplex.quasiIso_opMap {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [QuasiIso φ] : QuasiIso (opMap φ)

theorem CategoryTheory.ShortComplex.quasiIso_unopMap {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex Cᵒᵖ} [S₁.HasHomology] [S₂.HasHomology] [S₁.unop.HasHomology] [S₂.unop.HasHomology] (φ : S₁ ⟶ S₂) [QuasiIso φ] : QuasiIso (unopMap φ)

theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_liftCycles {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) : QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)

theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_descOpcycles {C : Type u_2} [Category.{u_1, u_2} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ ⋯)