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}
[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.
theorem
homotopy_equiv.to_quasi_iso_inv
{ι : 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)
(i : ι) :
(category_theory.as_iso ((homology_functor W c i).map e.hom)).inv = (homology_functor W c i).map e.inv
noncomputable
def
homological_complex.hom.to_single₀_cokernel_at_zero_iso
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : chain_complex W ℕ}
{Y : W}
(f : X ⟶ (chain_complex.single₀ W).obj Y)
[hf : quasi_iso f] :
category_theory.limits.cokernel (X.d 1 0) ≅ Y
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.
theorem
homological_complex.hom.to_single₀_cokernel_at_zero_iso_hom_eq
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : chain_complex W ℕ}
{Y : W}
(f : X ⟶ (chain_complex.single₀ W).obj Y)
[hf : quasi_iso f] :
(homological_complex.hom.to_single₀_cokernel_at_zero_iso f).hom = category_theory.limits.cokernel.desc (X.d 1 0) (f.f 0) _
theorem
homological_complex.hom.to_single₀_epi_at_zero
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : chain_complex W ℕ}
{Y : W}
(f : X ⟶ (chain_complex.single₀ W).obj Y)
[hf : quasi_iso f] :
category_theory.epi (f.f 0)
theorem
homological_complex.hom.to_single₀_exact_d_f_at_zero
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : chain_complex W ℕ}
{Y : W}
(f : X ⟶ (chain_complex.single₀ W).obj 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}
[category_theory.category W]
[category_theory.abelian W]
{X : chain_complex W ℕ}
{Y : W}
(f : X ⟶ (chain_complex.single₀ W).obj Y)
[hf : quasi_iso f]
(n : ℕ) :
noncomputable
def
homological_complex.hom.from_single₀_kernel_at_zero_iso
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : cochain_complex W ℕ}
{Y : W}
(f : (cochain_complex.single₀ W).obj Y ⟶ X)
[hf : quasi_iso f] :
category_theory.limits.kernel (X.d 0 1) ≅ Y
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₀_kernel_at_zero_iso_inv_eq
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : cochain_complex W ℕ}
{Y : W}
(f : (cochain_complex.single₀ W).obj Y ⟶ X)
[hf : quasi_iso f] :
(homological_complex.hom.from_single₀_kernel_at_zero_iso f).inv = category_theory.limits.kernel.lift (X.d 0 1) (f.f 0) _
theorem
homological_complex.hom.from_single₀_mono_at_zero
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : cochain_complex W ℕ}
{Y : W}
(f : (cochain_complex.single₀ W).obj Y ⟶ X)
[hf : quasi_iso f] :
category_theory.mono (f.f 0)
theorem
homological_complex.hom.from_single₀_exact_f_d_at_zero
{W : Type u_2}
[category_theory.category W]
[category_theory.abelian W]
{X : cochain_complex W ℕ}
{Y : W}
(f : (cochain_complex.single₀ W).obj Y ⟶ 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}
[category_theory.category W]
[category_theory.abelian W]
{X : cochain_complex W ℕ}
{Y : W}
(f : (cochain_complex.single₀ W).obj Y ⟶ X)
[hf : quasi_iso f]
(n : ℕ) :
theorem
category_theory.functor.quasi_iso_of_map_quasi_iso
{ι : Type u_1}
{c : complex_shape ι}
{A : Type u_2}
[category_theory.category A]
[category_theory.abelian A]
{B : Type u_4}
[category_theory.category B]
[category_theory.abelian B]
(F : A ⥤ B)
[F.additive]
[category_theory.limits.preserves_finite_limits F]
[category_theory.limits.preserves_finite_colimits F]
[category_theory.faithful F]
{C D : homological_complex A c}
(f : C ⟶ D)
(hf : quasi_iso ((F.map_homological_complex c).map f)) :