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.

source
class CategoryTheory.ShortComplex.QuasiIso {C : Type u_1} [Category.{v_1, 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.

Instances
    source
    instance CategoryTheory.ShortComplex.QuasiIso.isIso {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [QuasiIso φ] :
    IsIso (homologyMap φ)
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) :
    QuasiIso φ ↔ IsIso (homologyMap φ)
    source
    instance CategoryTheory.ShortComplex.quasiIso_of_isIso {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [IsIso φ] :
    QuasiIso φ
    source
    instance CategoryTheory.ShortComplex.quasiIso_comp {C : Type u_1} [Category.{v_1, u_1} 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 φ φ')
    source
    theorem CategoryTheory.ShortComplex.quasiIso_of_comp_left {C : Type u_1} [Category.{v_1, u_1} 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 φ'
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_comp_left {C : Type u_1} [Category.{v_1, u_1} 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 φ'
    source
    theorem CategoryTheory.ShortComplex.quasiIso_of_comp_right {C : Type u_1} [Category.{v_1, u_1} 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 φ
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_comp_right {C : Type u_1} [Category.{v_1, u_1} 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 φ
    source
    theorem CategoryTheory.ShortComplex.quasiIso_of_arrow_mk_iso {C : Type u_1} [Category.{v_1, u_1} 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 φ'
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_of_arrow_mk_iso {C : Type u_1} [Category.{v_1, u_1} 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 φ'
    source
    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff {C : Type u_1} [Category.{v_1, u_1} 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
    source
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff {C : Type u_1} [Category.{v_1, u_1} 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
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_leftHomologyMap' {C : Type u_1} [Category.{v_1, u_1} 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₂)
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_rightHomologyMap' {C : Type u_1} [Category.{v_1, u_1} 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₂)
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_homologyMap' {C : Type u_1} [Category.{v_1, u_1} 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₂)
    source
    theorem CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    QuasiIso φ
    source
    theorem CategoryTheory.ShortComplex.quasiIso_opMap_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) :
    QuasiIso (opMap φ) ↔ QuasiIso φ
    source
    theorem CategoryTheory.ShortComplex.quasiIso_opMap {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) [QuasiIso φ] :
    QuasiIso (opMap φ)
    source
    theorem CategoryTheory.ShortComplex.quasiIso_unopMap {C : Type u_1} [Category.{v_1, 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 φ)
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_liftCycles {C : Type u_1} [Category.{v_1, u_1} 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 φ.τ₂ ⋯)
    source
    theorem CategoryTheory.ShortComplex.quasiIso_iff_isIso_descOpcycles {C : Type u_1} [Category.{v_1, u_1} 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 φ.τ₂ ⋯)