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} [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' : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

  the homology map is an isomorphism

theorem CategoryTheory.ShortComplex.QuasiIso.isIso' {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {S₁ S₂ : CategoryTheory.ShortComplex C} {inst_2 : S₁.HasHomology} {inst_3 : S₂.HasHomology} {φ : S₁ ⟶ S₂} [self : CategoryTheory.ShortComplex.QuasiIso φ], CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)

the homology map is an isomorphism

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

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

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.quasiIso_comp {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₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] [S₄.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] [S₃.HasHomology] [S₄.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : 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} [S₁.HasHomology] [S₂.HasHomology] {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : 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} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) : 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} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : 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} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) : 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} [S₁.HasHomology] [S₂.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] (φ : 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} [S₁.HasHomology] [S₂.HasHomology] (φ : 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ᵒᵖ} [S₁.HasHomology] [S₂.HasHomology] [S₁.unop.HasHomology] [S₂.unop.HasHomology] (φ : 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₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) : CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (S₂.liftCycles φ.τ₂ ⋯)

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₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) : CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso (S₁.descOpcycles φ.τ₂ ⋯)