Documentation

Mathlib.Algebra.Homology.QuasiIso

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 : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :

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
    theorem QuasiIsoAt.quasiIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {f : K L} {i : ι} [K.HasHomology i] [L.HasHomology i] [self : QuasiIsoAt f i] :
    instance quasiIsoAt_of_isIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) [CategoryTheory.IsIso f] (i : ι) [K.HasHomology i] [L.HasHomology i] :
    Equations
    • =
    theorem quasiIsoAt_iff' {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {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] :
    theorem quasiIsoAt_iff_exactAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] (hK : K.ExactAt i) :
    QuasiIsoAt f i L.ExactAt i
    theorem quasiIsoAt_iff_exactAt' {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] (hL : L.ExactAt i) :
    QuasiIsoAt f i K.ExactAt i
    instance instIsIsoHomologyMapOfQuasiIsoAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [hf : QuasiIsoAt f i] :
    Equations
    • =
    @[simp]
    theorem isoOfQuasiIsoAt_hom {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :
    noncomputable def isoOfQuasiIsoAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {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
      @[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 : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] {Z : C} (h : K.homology i Z) :
      @[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 : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] {Z : C} (h : L.homology i Z) :
      class QuasiIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :

      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
        theorem QuasiIso.quasiIsoAt {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {f : K L} [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [self : QuasiIso f] (i : ι) :
        theorem quasiIso_iff {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
        QuasiIso f ∀ (i : ι), QuasiIsoAt f i
        instance quasiIso_of_isIso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (f : K L) [CategoryTheory.IsIso f] [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
        Equations
        • =
        instance quasiIsoAt_comp {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : QuasiIsoAt φ i] [hφ' : QuasiIsoAt φ' i] :
        Equations
        • =
        instance quasiIso_comp {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K L) (φ' : L M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ] [hφ' : QuasiIso φ'] :
        Equations
        • =
        theorem quasiIsoAt_of_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {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] :
        theorem quasiIsoAt_iff_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : QuasiIsoAt φ i] :
        theorem quasiIso_iff_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K L) (φ' : L M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ] :
        theorem quasiIso_of_comp_left {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {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 φ φ')] :
        theorem quasiIsoAt_of_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {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] :
        theorem quasiIsoAt_iff_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ' : QuasiIsoAt φ' i] :
        theorem quasiIso_iff_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {M : HomologicalComplex C c} (φ : K L) (φ' : L M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ' : QuasiIso φ'] :
        theorem quasiIso_of_comp_right {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {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 φ φ')] :
        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 : HomologicalComplex C c} {L : HomologicalComplex C c} {K' : HomologicalComplex C c} {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] :
        theorem quasiIso_of_arrow_mk_iso {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} {K' : HomologicalComplex C c} {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 φ] :
        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 : HomologicalComplex C₁ c} {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
        Equations
        • =
        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 : HomologicalComplex C₁ c} {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
        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 : HomologicalComplex C₁ c} {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 φ)
        Equations
        • =
        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 : HomologicalComplex C₁ c} {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 φ
        instance instQuasiIsoHom {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (e : HomotopyEquiv K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
        QuasiIso e.hom
        Equations
        • =
        instance instQuasiIsoInv {ι : Type u_1} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {c : ComplexShape ι} {K : HomologicalComplex C c} {L : HomologicalComplex C c} (e : HomotopyEquiv K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
        QuasiIso e.inv
        Equations
        • =