# mathlib3documentation

algebra.homology.quasi_iso

# Quasi-isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} {c : complex_shape ι} {C D : c} (f : C D) :
Prop

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} {c : complex_shape ι} {C D : c} (f : C D)  :
@[protected, instance]
def quasi_iso_comp {ι : Type u_1} {V : Type u} {c : complex_shape ι} {C D E : 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} {c : complex_shape ι} {C D E : 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} {c : complex_shape ι} {C D E : 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} {C D : c} (e : D) :

An homotopy equivalence is a quasi-isomorphism.

theorem homotopy_equiv.to_quasi_iso_inv {ι : Type u_1} {c : complex_shape ι} {W : Type u_2} {C D : c} (e : D) (i : ι) :
noncomputable def homological_complex.hom.to_single₀_cokernel_at_zero_iso {W : Type u_2} {X : } {Y : W} (f : X Y) [hf : quasi_iso f] :

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
theorem homological_complex.hom.to_single₀_cokernel_at_zero_iso_hom_eq {W : Type u_2} {X : } {Y : W} (f : X Y) [hf : quasi_iso f] :
theorem homological_complex.hom.to_single₀_epi_at_zero {W : Type u_2} {X : } {Y : W} (f : X Y) [hf : quasi_iso f] :
theorem homological_complex.hom.to_single₀_exact_d_f_at_zero {W : Type u_2} {X : } {Y : W} (f : X Y) [hf : quasi_iso f] :
category_theory.exact (X.d 1 0) (f.f 0)
theorem homological_complex.hom.to_single₀_exact_at_succ {W : Type u_2} {X : } {Y : W} (f : X Y) [hf : quasi_iso f] (n : ) :
category_theory.exact (X.d (n + 2) (n + 1)) (X.d (n + 1) n)
noncomputable def homological_complex.hom.from_single₀_kernel_at_zero_iso {W : Type u_2} {X : } {Y : W} (f : X) [hf : quasi_iso f] :

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
theorem homological_complex.hom.from_single₀_mono_at_zero {W : Type u_2} {X : } {Y : W} (f : X) [hf : quasi_iso f] :
theorem homological_complex.hom.from_single₀_exact_f_d_at_zero {W : Type u_2} {X : } {Y : W} (f : X) [hf : quasi_iso f] :
category_theory.exact (f.f 0) (X.d 0 1)
theorem homological_complex.hom.from_single₀_exact_at_succ {W : Type u_2} {X : } {Y : W} (f : X) [hf : quasi_iso f] (n : ) :
category_theory.exact (X.d n (n + 1)) (X.d (n + 1) (n + 2))
theorem category_theory.functor.quasi_iso_of_map_quasi_iso {ι : Type u_1} {c : complex_shape ι} {A : Type u_2} {B : Type u_4} (F : A B) [F.additive] {C D : c} (f : C D) (hf : quasi_iso ((F.map_homological_complex c).map f)) :