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?
@[class]
structure
quasi_iso
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f : C ⟶ D) :
Prop
- is_iso : ∀ (i : ι), category_theory.is_iso ((homology_functor V c i).map f)
A chain map is a quasi-isomorphism if it induces isomorphisms on homology.
Instances of this typeclass
@[protected, instance]
def
quasi_iso_of_iso
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
{c : complex_shape ι}
{C D : homological_complex V c}
(f : C ⟶ D)
[category_theory.is_iso f] :
@[protected, instance]
def
quasi_iso_comp
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
{c : complex_shape ι}
{C D E : homological_complex V c}
(f : C ⟶ D)
[quasi_iso f]
(g : D ⟶ E)
[quasi_iso g] :
theorem
quasi_iso_of_comp_left
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
{c : complex_shape ι}
{C D E : homological_complex V c}
(f : C ⟶ D)
[quasi_iso f]
(g : D ⟶ E)
[quasi_iso (f ≫ g)] :
theorem
quasi_iso_of_comp_right
{ι : Type u_1}
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
[category_theory.limits.has_cokernels V]
{c : complex_shape ι}
{C D E : homological_complex V c}
(f : C ⟶ D)
(g : D ⟶ E)
[quasi_iso g]
[quasi_iso (f ≫ g)] :
theorem
homotopy_equiv.to_quasi_iso
{ι : Type u_1}
{c : complex_shape ι}
{W : Type u_2}
[category_theory.category W]
[category_theory.preadditive W]
[category_theory.limits.has_cokernels W]
[category_theory.limits.has_images W]
[category_theory.limits.has_equalizers W]
[category_theory.limits.has_zero_object W]
[category_theory.limits.has_image_maps W]
{C D : homological_complex W c}
(e : homotopy_equiv C D) :
An homotopy equivalence is a quasi-isomorphism.