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
QuasiIso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasEqualizers V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
[CategoryTheory.Limits.HasCokernels V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
:
- isIso : ∀ (i : ι), CategoryTheory.IsIso ((homologyFunctor V c i).map f)
A chain map is a quasi-isomorphism if it induces isomorphisms on homology.
Instances
instance
quasiIso_of_iso
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasEqualizers V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
[CategoryTheory.Limits.HasCokernels V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
(f : C ⟶ D)
[CategoryTheory.IsIso f]
:
QuasiIso f
instance
quasiIso_comp
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasEqualizers V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
[CategoryTheory.Limits.HasCokernels V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
{E : HomologicalComplex V c}
(f : C ⟶ D)
[QuasiIso f]
(g : D ⟶ E)
[QuasiIso g]
:
theorem
quasiIso_of_comp_left
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasEqualizers V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
[CategoryTheory.Limits.HasCokernels V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
{E : HomologicalComplex V c}
(f : C ⟶ D)
[QuasiIso f]
(g : D ⟶ E)
[QuasiIso (CategoryTheory.CategoryStruct.comp f g)]
:
QuasiIso g
theorem
quasiIso_of_comp_right
{ι : Type u_1}
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
[CategoryTheory.Limits.HasEqualizers V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
[CategoryTheory.Limits.HasCokernels V]
{c : ComplexShape ι}
{C : HomologicalComplex V c}
{D : HomologicalComplex V c}
{E : HomologicalComplex V c}
(f : C ⟶ D)
(g : D ⟶ E)
[QuasiIso g]
[QuasiIso (CategoryTheory.CategoryStruct.comp f g)]
:
QuasiIso f
theorem
HomotopyEquiv.toQuasiIso
{ι : Type u_1}
{c : ComplexShape ι}
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasCokernels W]
[CategoryTheory.Limits.HasImages W]
[CategoryTheory.Limits.HasEqualizers W]
[CategoryTheory.Limits.HasImageMaps W]
{C : HomologicalComplex W c}
{D : HomologicalComplex W c}
(e : HomotopyEquiv C D)
:
QuasiIso e.hom
A homotopy equivalence is a quasi-isomorphism.
theorem
HomotopyEquiv.toQuasiIso_inv
{ι : Type u_1}
{c : ComplexShape ι}
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Preadditive W]
[CategoryTheory.Limits.HasCokernels W]
[CategoryTheory.Limits.HasImages W]
[CategoryTheory.Limits.HasEqualizers W]
[CategoryTheory.Limits.HasImageMaps W]
{C : HomologicalComplex W c}
{D : HomologicalComplex W c}
(e : HomotopyEquiv C D)
(i : ι)
:
(CategoryTheory.asIso ((homologyFunctor W c i).map e.hom)).inv = (homologyFunctor W c i).map e.inv
noncomputable def
HomologicalComplex.Hom.toSingle₀CokernelAtZeroIso
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : ChainComplex W ℕ}
{Y : W}
(f : X ⟶ (ChainComplex.single₀ W).obj Y)
[hf : QuasiIso 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.
Instances For
theorem
HomologicalComplex.Hom.toSingle₀CokernelAtZeroIso_hom_eq
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : ChainComplex W ℕ}
{Y : W}
(f : X ⟶ (ChainComplex.single₀ W).obj Y)
[hf : QuasiIso f]
:
(HomologicalComplex.Hom.toSingle₀CokernelAtZeroIso f).hom = CategoryTheory.Limits.cokernel.desc (HomologicalComplex.d X 1 0) (HomologicalComplex.Hom.f f 0)
(_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.d X 1 0) (HomologicalComplex.Hom.f f 0) = 0)
theorem
HomologicalComplex.Hom.to_single₀_epi_at_zero
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : ChainComplex W ℕ}
{Y : W}
(f : X ⟶ (ChainComplex.single₀ W).obj Y)
[hf : QuasiIso f]
:
theorem
HomologicalComplex.Hom.to_single₀_exact_d_f_at_zero
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : ChainComplex W ℕ}
{Y : W}
(f : X ⟶ (ChainComplex.single₀ W).obj Y)
[hf : QuasiIso f]
:
CategoryTheory.Exact (HomologicalComplex.d X 1 0) (HomologicalComplex.Hom.f f 0)
theorem
HomologicalComplex.Hom.to_single₀_exact_at_succ
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : ChainComplex W ℕ}
{Y : W}
(f : X ⟶ (ChainComplex.single₀ W).obj Y)
[hf : QuasiIso f]
(n : ℕ)
:
CategoryTheory.Exact (HomologicalComplex.d X (n + 2) (n + 1)) (HomologicalComplex.d X (n + 1) n)
noncomputable def
HomologicalComplex.Hom.fromSingle₀KernelAtZeroIso
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : CochainComplex W ℕ}
{Y : W}
(f : (CochainComplex.single₀ W).obj Y ⟶ X)
[hf : QuasiIso 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.
Instances For
theorem
HomologicalComplex.Hom.fromSingle₀KernelAtZeroIso_inv_eq
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : CochainComplex W ℕ}
{Y : W}
(f : (CochainComplex.single₀ W).obj Y ⟶ X)
[hf : QuasiIso f]
:
(HomologicalComplex.Hom.fromSingle₀KernelAtZeroIso f).inv = CategoryTheory.Limits.kernel.lift (HomologicalComplex.d X 0 1) (HomologicalComplex.Hom.f f 0)
(_ : CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f 0) (HomologicalComplex.d X 0 1) = 0)
theorem
HomologicalComplex.Hom.from_single₀_mono_at_zero
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : CochainComplex W ℕ}
{Y : W}
(f : (CochainComplex.single₀ W).obj Y ⟶ X)
[hf : QuasiIso f]
:
theorem
HomologicalComplex.Hom.from_single₀_exact_f_d_at_zero
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : CochainComplex W ℕ}
{Y : W}
(f : (CochainComplex.single₀ W).obj Y ⟶ X)
[hf : QuasiIso f]
:
CategoryTheory.Exact (HomologicalComplex.Hom.f f 0) (HomologicalComplex.d X 0 1)
theorem
HomologicalComplex.Hom.from_single₀_exact_at_succ
{W : Type u_2}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : CochainComplex W ℕ}
{Y : W}
(f : (CochainComplex.single₀ W).obj Y ⟶ X)
[hf : QuasiIso f]
(n : ℕ)
:
CategoryTheory.Exact (HomologicalComplex.d X n (n + 1)) (HomologicalComplex.d X (n + 1) (n + 2))
theorem
CategoryTheory.Functor.quasiIso_of_map_quasiIso
{ι : Type u_1}
{c : ComplexShape ι}
{A : Type u_2}
[CategoryTheory.Category.{u_4, u_2} A]
[CategoryTheory.Abelian A]
{B : Type u_3}
[CategoryTheory.Category.{u_5, u_3} B]
[CategoryTheory.Abelian B]
(F : CategoryTheory.Functor A B)
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Limits.PreservesFiniteLimits F]
[CategoryTheory.Limits.PreservesFiniteColimits F]
[CategoryTheory.Faithful F]
{C : HomologicalComplex A c}
{D : HomologicalComplex A c}
(f : C ⟶ D)
(hf : QuasiIso ((CategoryTheory.Functor.mapHomologicalComplex F c).map f))
:
QuasiIso f