Quasi-isomorphisms #

A chain map is a quasi-isomorphism if it induces isomorphisms on homology.

class QuasiIsoAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] :

Prop

A morphism of homological complexes f : K ⟶ L is a quasi-isomorphism in degree i when it induces a quasi-isomorphism of short complexes K.sc i ⟶ L.sc i.

quasiIso : CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)

Instances

source

theorem quasiIsoAt_iff {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] :

QuasiIsoAt f i ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)

source

instance quasiIsoAt_of_isIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [CategoryTheory.IsIso f] (i : ι) [K.HasHomology i] [L.HasHomology i] :

QuasiIsoAt f i

source

theorem quasiIsoAt_iff' {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j] [L.HasHomology j] [(K.sc' i j k).HasHomology] [(L.sc' i j k).HasHomology] :

QuasiIsoAt f j ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C c i j k).map f)

source

theorem quasiIsoAt_of_retract {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c} {f : K ⟶ L} {f' : K' ⟶ L'} (h : CategoryTheory.RetractArrow f f') (i : ι) [K.HasHomology i] [L.HasHomology i] [K'.HasHomology i] [L'.HasHomology i] [hf' : QuasiIsoAt f' i] :

QuasiIsoAt f i

source

theorem quasiIsoAt_iff_isIso_homologyMap {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] :

QuasiIsoAt f i ↔ CategoryTheory.IsIso (HomologicalComplex.homologyMap f i)

source

theorem quasiIsoAt_iff_exactAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] (hK : K.ExactAt i) :

QuasiIsoAt f i ↔ L.ExactAt i

source

theorem quasiIsoAt_iff_exactAt' {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] (hL : L.ExactAt i) :

QuasiIsoAt f i ↔ K.ExactAt i

source

theorem exactAt_iff_of_quasiIsoAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :

K.ExactAt i ↔ L.ExactAt i

source

instance instIsIsoHomologyMapOfQuasiIsoAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [hf : QuasiIsoAt f i] :

CategoryTheory.IsIso (HomologicalComplex.homologyMap f i)

source

noncomputable def isoOfQuasiIsoAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :

K.homology i ≅ L.homology i

The isomorphism K.homology i ≅ L.homology i induced by a morphism f : K ⟶ L such that [QuasiIsoAt f i] holds.

Equations

isoOfQuasiIsoAt f i = CategoryTheory.asIso (HomologicalComplex.homologyMap f i)

Instances For

source

@[simp]

theorem isoOfQuasiIsoAt_hom {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :

(isoOfQuasiIsoAt f i).hom = HomologicalComplex.homologyMap f i

source

@[simp]

theorem isoOfQuasiIsoAt_hom_inv_id {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :

CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i) (isoOfQuasiIsoAt f i).inv = CategoryTheory.CategoryStruct.id (K.homology i)

source

@[simp]

theorem isoOfQuasiIsoAt_hom_inv_id_assoc {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] {Z : C} (h : K.homology i ⟶ Z) :

CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i) (CategoryTheory.CategoryStruct.comp (isoOfQuasiIsoAt f i).inv h) = h

source

@[simp]

theorem isoOfQuasiIsoAt_inv_hom_id {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :

CategoryTheory.CategoryStruct.comp (isoOfQuasiIsoAt f i).inv (HomologicalComplex.homologyMap f i) = CategoryTheory.CategoryStruct.id (L.homology i)

source

@[simp]

theorem isoOfQuasiIsoAt_inv_hom_id_assoc {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] {Z : C} (h : L.homology i ⟶ Z) :

CategoryTheory.CategoryStruct.comp (isoOfQuasiIsoAt f i).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i) h) = h

source

theorem CochainComplex.quasiIsoAt₀_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : CochainComplex C ℕ} (f : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] [(HomologicalComplex.sc' K 0 0 1).HasHomology] [(HomologicalComplex.sc' L 0 0 1).HasHomology] :

QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map f)

source

theorem ChainComplex.quasiIsoAt₀_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K L : ChainComplex C ℕ} (f : K ⟶ L) [HomologicalComplex.HasHomology K 0] [HomologicalComplex.HasHomology L 0] [(HomologicalComplex.sc' K 1 0 0).HasHomology] [(HomologicalComplex.sc' L 1 0 0).HasHomology] :

QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map f)

source

class QuasiIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :

Prop

A morphism of homological complexes f : K ⟶ L is a quasi-isomorphism when it is so in every degree, i.e. when the induced maps homologyMap f i : K.homology i ⟶ L.homology i are all isomorphisms (see quasiIso_iff and quasiIsoAt_iff_isIso_homologyMap).

quasiIsoAt (i : ι) : QuasiIsoAt f i

Instances

source

theorem quasiIso_iff {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :

QuasiIso f ↔ ∀ (i : ι), QuasiIsoAt f i

source

instance quasiIso_of_isIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L) [CategoryTheory.IsIso f] [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :

QuasiIso f

source

instance quasiIsoAt_comp {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : QuasiIsoAt φ i] [hφ' : QuasiIsoAt φ' i] :

QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i

source

instance quasiIso_comp {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ] [hφ' : QuasiIso φ'] :

QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')

source

theorem quasiIsoAt_of_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : QuasiIsoAt φ i] [hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i] :

QuasiIsoAt φ' i

source

theorem quasiIsoAt_iff_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : QuasiIsoAt φ i] :

QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ' i

source

theorem quasiIso_iff_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ] :

QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ QuasiIso φ'

source

theorem quasiIso_of_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ] [hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')] :

QuasiIso φ'

source

theorem quasiIsoAt_of_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ' : QuasiIsoAt φ' i] [hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i] :

QuasiIsoAt φ i

source

theorem quasiIsoAt_iff_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ' : QuasiIsoAt φ' i] :

QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ i

source

theorem quasiIso_iff_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ' : QuasiIso φ'] :

QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ QuasiIso φ

source

theorem quasiIso_of_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (φ' : L ⟶ M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ'] [hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')] :

QuasiIso φ

source

theorem quasiIso_iff_of_arrow_mk_iso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c} (φ : K ⟶ L) (φ' : K' ⟶ L') (e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ') [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), K'.HasHomology i] [∀ (i : ι), L'.HasHomology i] :

QuasiIso φ ↔ QuasiIso φ'

source

theorem quasiIso_of_arrow_mk_iso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c} (φ : K ⟶ L) (φ' : K' ⟶ L') (e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ') [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), K'.HasHomology i] [∀ (i : ι), L'.HasHomology i] [hφ : QuasiIso φ] :

QuasiIso φ'

source

theorem quasiIso_of_retractArrow {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c} {f : K ⟶ L} {f' : K' ⟶ L'} (h : CategoryTheory.RetractArrow f f') [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), K'.HasHomology i] [∀ (i : ι), L'.HasHomology i] [QuasiIso f'] :

QuasiIso f

source

instance HomologicalComplex.quasiIsoAt_map_of_preservesHomology {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [CategoryTheory.Category.{u_4, u_2} C₁] [CategoryTheory.Category.{u_5, u_3} C₂] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L) (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [F.PreservesHomology] (i : ι) [K.HasHomology i] [L.HasHomology i] [((F.mapHomologicalComplex c).obj K).HasHomology i] [((F.mapHomologicalComplex c).obj L).HasHomology i] [hφ : QuasiIsoAt φ i] :

QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i

source

theorem HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [CategoryTheory.Category.{u_4, u_2} C₁] [CategoryTheory.Category.{u_5, u_3} C₂] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L) (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [F.PreservesHomology] (i : ι) [K.HasHomology i] [L.HasHomology i] [((F.mapHomologicalComplex c).obj K).HasHomology i] [((F.mapHomologicalComplex c).obj L).HasHomology i] [F.ReflectsIsomorphisms] :

QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i

source

instance HomologicalComplex.quasiIso_map_of_preservesHomology {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [CategoryTheory.Category.{u_4, u_2} C₁] [CategoryTheory.Category.{u_5, u_3} C₂] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L) (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [F.PreservesHomology] [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i] [∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i] [hφ : QuasiIso φ] :

QuasiIso ((F.mapHomologicalComplex c).map φ)

source

theorem HomologicalComplex.quasiIso_map_iff_of_preservesHomology {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [CategoryTheory.Category.{u_4, u_2} C₁] [CategoryTheory.Category.{u_5, u_3} C₂] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L) (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [F.PreservesHomology] [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i] [∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i] [F.ReflectsIsomorphisms] :

QuasiIso ((F.mapHomologicalComplex c).map φ) ↔ QuasiIso φ

source

def HomologicalComplex.quasiIso {ι : Type u_1} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology C] :

CategoryTheory.MorphismProperty (HomologicalComplex C c)

The morphism property on HomologicalComplex C c given by quasi-isomorphisms.

Equations

HomologicalComplex.quasiIso C c f = QuasiIso f

Instances For

source

@[simp]

theorem HomologicalComplex.mem_quasiIso_iff {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} [CategoryTheory.CategoryWithHomology C] (f : K ⟶ L) :

quasiIso C c f ↔ QuasiIso f

source

instance HomologicalComplex.instIsMultiplicativeQuasiIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} [CategoryTheory.CategoryWithHomology C] :

(quasiIso C c).IsMultiplicative

source

instance HomologicalComplex.instHasTwoOutOfThreePropertyQuasiIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} [CategoryTheory.CategoryWithHomology C] :

(quasiIso C c).HasTwoOutOfThreeProperty

source

instance HomologicalComplex.instIsStableUnderRetractsQuasiIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} [CategoryTheory.CategoryWithHomology C] :

(quasiIso C c).IsStableUnderRetracts

source

instance HomologicalComplex.instRespectsIsoQuasiIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} [CategoryTheory.CategoryWithHomology C] :

(quasiIso C c).RespectsIso

source

instance instQuasiIsoHom {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (e : HomotopyEquiv K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :

QuasiIso e.hom

source

instance instQuasiIsoInv {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (e : HomotopyEquiv K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :

QuasiIso e.inv

source

theorem homotopyEquivalences_le_quasiIso {ι : Type u_1} (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (c : ComplexShape ι) [CategoryTheory.CategoryWithHomology C] :

HomologicalComplex.homotopyEquivalences C c ≤ HomologicalComplex.quasiIso C c

Documentation

Mathlib.Algebra.Homology.QuasiIso

Quasi-isomorphisms #