Documentation

Mathlib.Algebra.Homology.QuasiIso

Quasi-isomorphisms #

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

source
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.

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
    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).

      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.{v_1, u_2} C₁] [CategoryTheory.Category.{v_2, 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.{v_1, u_2} C₁] [CategoryTheory.Category.{v_2, 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.{v_1, u_2} C₁] [CategoryTheory.Category.{v_2, 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.{v_1, u_2} C₁] [CategoryTheory.Category.{v_2, 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
        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 HomotopyEquiv.quasiIsoAt_hom {ι : 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) (n : ι) [K.HasHomology n] [L.HasHomology n] :
          QuasiIsoAt e.hom n
          source
          instance HomotopyEquiv.quasiIsoAt_inv {ι : 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) (n : ι) [K.HasHomology n] [L.HasHomology n] :
          QuasiIsoAt e.inv n
          source
          instance HomotopyEquiv.quasiIso_hom {ι : 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) [∀ (n : ι), K.HasHomology n] [∀ (n : ι), L.HasHomology n] :
          QuasiIso e.hom
          source
          instance HomotopyEquiv.quasiIso_inv {ι : 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) [∀ (n : ι), K.HasHomology n] [∀ (n : ι), L.HasHomology n] :
          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