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} [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₂) :

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

Instances

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

(_ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)) = (_ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ))

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

(_ : CategoryTheory.ShortComplex.QuasiIso φ) = (_ : CategoryTheory.ShortComplex.QuasiIso φ)

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

(_ : CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')) = (_ : CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ'))

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₂ φ.τ₂ (_ : CategoryTheory.CategoryStruct.comp φ.τ₂ S₂.g = 0))

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₁ φ.τ₂ (_ : CategoryTheory.CategoryStruct.comp S₁.f φ.τ₂ = 0))