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

  the homology map is an isomorphism

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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