Quasi-isomorphisms #

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

Future work #

Define the derived category as the localization at quasi-isomorphisms? (TODO @joelriou)

class QuasiIso' {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) :

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

Instances
theorem QuasiIso'.isIso {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {f : C D} [self : ] (i : ι) :
@[instance 100]
instance quasiIso'_of_iso {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) :
Equations
• =
instance quasiIso'_comp {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : C D) [] (g : D E) [] :
Equations
• =
theorem quasiIso'_of_comp_left {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : C D) [] (g : D E) :
theorem quasiIso'_of_comp_right {ι : Type u_1} {V : Type u} {c : } {C : } {D : } {E : } (f : C D) (g : D E) [] :
theorem HomotopyEquiv.toQuasiIso' {ι : Type u_1} {c : } {W : Type u_2} [] {C : } {D : } (e : ) :
QuasiIso' e.hom

A homotopy equivalence is a quasi-isomorphism.

theorem HomotopyEquiv.toQuasiIso'_inv {ι : Type u_1} {c : } {W : Type u_2} [] {C : } {D : } (e : ) (i : ι) :
(CategoryTheory.asIso (().map e.hom)).inv = ().map e.inv
noncomputable def HomologicalComplex.Hom.toSingle₀CokernelAtZeroIso {W : Type u_2} [] {X : } {Y : W} (f : X .obj Y) [hf : ] :

If a chain map f : X ⟶ Y[0] is a quasi-isomorphism, then the cokernel of the differential d : X₁ → X₀ is isomorphic to Y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem HomologicalComplex.Hom.toSingle₀CokernelAtZeroIso_hom_eq {W : Type u_2} [] {X : } {Y : W} (f : X .obj Y) [hf : ] :
= CategoryTheory.Limits.cokernel.desc (X.d 1 0) (f.f 0)
theorem HomologicalComplex.Hom.to_single₀_epi_at_zero {W : Type u_2} [] {X : } {Y : W} (f : X .obj Y) [hf : ] :
theorem HomologicalComplex.Hom.to_single₀_exact_d_f_at_zero {W : Type u_2} [] {X : } {Y : W} (f : X .obj Y) [hf : ] :
CategoryTheory.Exact (X.d 1 0) (f.f 0)
theorem HomologicalComplex.Hom.to_single₀_exact_at_succ {W : Type u_2} [] {X : } {Y : W} (f : X .obj Y) [hf : ] (n : ) :
CategoryTheory.Exact (X.d (n + 2) (n + 1)) (X.d (n + 1) n)
noncomputable def HomologicalComplex.Hom.fromSingle₀KernelAtZeroIso {W : Type u_2} [] {X : } {Y : W} (f : .obj Y X) [hf : ] :

If a cochain map f : Y[0] ⟶ X is a quasi-isomorphism, then the kernel of the differential d : X₀ → X₁ is isomorphic to Y.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem HomologicalComplex.Hom.fromSingle₀KernelAtZeroIso_inv_eq {W : Type u_2} [] {X : } {Y : W} (f : .obj Y X) [hf : ] :
= CategoryTheory.Limits.kernel.lift (X.d 0 1) (f.f 0)
theorem HomologicalComplex.Hom.from_single₀_mono_at_zero {W : Type u_2} [] {X : } {Y : W} (f : .obj Y X) [hf : ] :
theorem HomologicalComplex.Hom.from_single₀_exact_f_d_at_zero {W : Type u_2} [] {X : } {Y : W} (f : .obj Y X) [hf : ] :
CategoryTheory.Exact (f.f 0) (X.d 0 1)
theorem HomologicalComplex.Hom.from_single₀_exact_at_succ {W : Type u_2} [] {X : } {Y : W} (f : .obj Y X) [hf : ] (n : ) :
CategoryTheory.Exact (X.d n (n + 1)) (X.d (n + 1) (n + 2))
theorem CategoryTheory.Functor.quasiIso'_of_map_quasiIso' {ι : Type u_1} {c : } {A : Type u_2} [] {B : Type u_3} [] (F : ) [F.Additive] [F.Faithful] {C : } {D : } (f : C D) (hf : QuasiIso' ((F.mapHomologicalComplex c).map f)) :
class QuasiIsoAt {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (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.

• quasiIso :
Instances
theorem QuasiIsoAt.quasiIso {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {f : K L} {i : ι} [K.HasHomology i] [L.HasHomology i] [self : ] :
theorem quasiIsoAt_iff {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
instance quasiIsoAt_of_isIso {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
Equations
• =
theorem quasiIsoAt_iff' {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (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_isIso_homologyMap {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
theorem quasiIsoAt_iff_exactAt {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] (hK : K.ExactAt i) :
L.ExactAt i
theorem quasiIsoAt_iff_exactAt' {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] (hL : L.ExactAt i) :
K.ExactAt i
instance instIsIsoHomologyMapOfQuasiIsoAt {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [hf : ] :
Equations
• =
@[simp]
theorem isoOfQuasiIsoAt_hom {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [] :
().hom =
noncomputable def isoOfQuasiIsoAt {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology 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_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [] {Z : C} (h : K.homology i Z) :
@[simp]
theorem isoOfQuasiIsoAt_hom_inv_id {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [] :
@[simp]
theorem isoOfQuasiIsoAt_inv_hom_id_assoc {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [] {Z : C} (h : L.homology i Z) :
@[simp]
theorem isoOfQuasiIsoAt_inv_hom_id {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) (i : ι) [K.HasHomology i] [L.HasHomology i] [] :
theorem CochainComplex.quasiIsoAt₀_iff {C : Type u} {K : } {L : } (f : K L) [().HasHomology] [().HasHomology] :
theorem ChainComplex.quasiIsoAt₀_iff {C : Type u} {K : } {L : } (f : K L) [().HasHomology] [().HasHomology] :
class QuasiIso {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (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).

• quasiIsoAt : ∀ (i : ι),
Instances
theorem QuasiIso.quasiIsoAt {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {f : K L} [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [self : ] (i : ι) :
theorem quasiIso_iff {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
∀ (i : ι),
instance quasiIso_of_isIso {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
Equations
• =
instance quasiIsoAt_comp {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : ] [hφ' : QuasiIsoAt φ' i] :
Equations
• =
instance quasiIso_comp {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : ] [hφ' : QuasiIso φ'] :
Equations
• =
theorem quasiIsoAt_of_comp_left {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : ] [hφφ' : ] :
theorem quasiIsoAt_iff_comp_left {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ : ] :
theorem quasiIso_iff_comp_left {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : ] :
theorem quasiIso_of_comp_left {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : ] [hφφ' : ] :
theorem quasiIsoAt_of_comp_right {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ' : QuasiIsoAt φ' i] [hφφ' : ] :
theorem quasiIsoAt_iff_comp_right {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) (i : ι) [K.HasHomology i] [L.HasHomology i] [M.HasHomology i] [hφ' : QuasiIsoAt φ' i] :
theorem quasiIso_iff_comp_right {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : 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_2} {C : Type u} {c : } {K : } {L : } {M : } (φ : K L) (φ' : L M) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), M.HasHomology i] [hφ : QuasiIso φ'] [hφφ' : ] :
theorem quasiIso_iff_of_arrow_mk_iso {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {K' : } {L' : } (φ : K L) (φ' : K' L') (e : ) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), K'.HasHomology i] [∀ (i : ι), L'.HasHomology i] :
theorem quasiIso_of_arrow_mk_iso {ι : Type u_2} {C : Type u} {c : } {K : } {L : } {K' : } {L' : } (φ : K L) (φ' : K' L') (e : ) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] [∀ (i : ι), K'.HasHomology i] [∀ (i : ι), L'.HasHomology i] [hφ : ] :
instance HomologicalComplex.quasiIsoAt_map_of_preservesHomology {ι : Type u_2} {c : } {C₁ : Type u_3} {C₂ : Type u_4} [] [] {K : } {L : } (φ : K L) (F : ) [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 ((F.mapHomologicalComplex c).map φ) i
Equations
• =
theorem HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology {ι : Type u_2} {c : } {C₁ : Type u_3} {C₂ : Type u_4} [] [] {K : } {L : } (φ : K L) (F : ) [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
instance HomologicalComplex.quasiIso_map_of_preservesHomology {ι : Type u_2} {c : } {C₁ : Type u_3} {C₂ : Type u_4} [] [] {K : } {L : } (φ : K L) (F : ) [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 ((F.mapHomologicalComplex c).map φ)
Equations
• =
theorem HomologicalComplex.quasiIso_map_iff_of_preservesHomology {ι : Type u_2} {c : } {C₁ : Type u_3} {C₂ : Type u_4} [] [] {K : } {L : } (φ : K L) (F : ) [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 φ)
def HomologicalComplex.quasiIso {ι : Type u_2} (C : Type u) (c : ) :

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

Equations
Instances For
@[simp]
theorem HomologicalComplex.mem_quasiIso_iff {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (f : K L) :
instance instQuasiIsoHom {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (e : ) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
QuasiIso e.hom
Equations
• =
instance instQuasiIsoInv {ι : Type u_2} {C : Type u} {c : } {K : } {L : } (e : ) [∀ (i : ι), K.HasHomology i] [∀ (i : ι), L.HasHomology i] :
QuasiIso e.inv
Equations
• =
theorem homotopyEquivalences_le_quasiIso {ι : Type u_2} (C : Type u) (c : ) :