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}
[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)
:
A chain map is a quasi-isomorphism if it induces isomorphisms on homology.
- isIso : ∀ (i : ι), CategoryTheory.IsIso ((homology'Functor V c i).toPrefunctor.map f)
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]
:
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]
:
Equations
- (_ : QuasiIso' (CategoryTheory.CategoryStruct.comp f g)) = (_ : QuasiIso' (CategoryTheory.CategoryStruct.comp f 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)]
:
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)]
:
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 ((homology'Functor W c i).toPrefunctor.map e.hom)).inv = (homology'Functor W c i).toPrefunctor.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).toPrefunctor.obj Y)
[hf : QuasiIso' f]
:
CategoryTheory.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.
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}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : ChainComplex W ℕ}
{Y : W}
(f : X ⟶ (ChainComplex.single₀ W).toPrefunctor.obj Y)
[hf : QuasiIso' f]
:
(HomologicalComplex.Hom.toSingle₀CokernelAtZeroIso f).hom = CategoryTheory.Limits.cokernel.desc (X.d 1 0) (f.f 0) (_ : CategoryTheory.CategoryStruct.comp (X.d 1 0) (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).toPrefunctor.obj Y)
[hf : QuasiIso' f]
:
CategoryTheory.Epi (f.f 0)
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).toPrefunctor.obj Y)
[hf : QuasiIso' f]
:
CategoryTheory.Exact (X.d 1 0) (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).toPrefunctor.obj Y)
[hf : QuasiIso' f]
(n : ℕ)
:
CategoryTheory.Exact (X.d (n + 2) (n + 1)) (X.d (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).toPrefunctor.obj Y ⟶ X)
[hf : QuasiIso' f]
:
CategoryTheory.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
- 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}
[CategoryTheory.Category.{u_3, u_2} W]
[CategoryTheory.Abelian W]
{X : CochainComplex W ℕ}
{Y : W}
(f : (CochainComplex.single₀ W).toPrefunctor.obj Y ⟶ X)
[hf : QuasiIso' f]
:
(HomologicalComplex.Hom.fromSingle₀KernelAtZeroIso f).inv = CategoryTheory.Limits.kernel.lift (X.d 0 1) (f.f 0) (_ : CategoryTheory.CategoryStruct.comp (f.f 0) (X.d 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).toPrefunctor.obj Y ⟶ X)
[hf : QuasiIso' f]
:
CategoryTheory.Mono (f.f 0)
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).toPrefunctor.obj Y ⟶ X)
[hf : QuasiIso' f]
:
CategoryTheory.Exact (f.f 0) (X.d 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).toPrefunctor.obj Y ⟶ X)
[hf : QuasiIso' f]
(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 : 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).toPrefunctor.map f))
:
class
QuasiIsoAt
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L 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 : CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).toPrefunctor.map f)
Instances
theorem
quasiIsoAt_iff
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
:
QuasiIsoAt f i ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).toPrefunctor.map f)
instance
quasiIsoAt_of_isIso
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
[CategoryTheory.IsIso f]
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
:
QuasiIsoAt f i
Equations
- (_ : QuasiIsoAt f i) = (_ : QuasiIsoAt f i)
theorem
quasiIsoAt_iff'
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
(j : ι)
(k : ι)
(hi : ComplexShape.prev c j = i)
(hk : ComplexShape.next c j = k)
[HomologicalComplex.HasHomology K j]
[HomologicalComplex.HasHomology L j]
[CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K i j k)]
[CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' L i j k)]
:
QuasiIsoAt f j ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C c i j k).toPrefunctor.map f)
theorem
quasiIsoAt_iff_isIso_homologyMap
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
:
theorem
quasiIsoAt_iff_exactAt
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
(hK : HomologicalComplex.ExactAt K i)
:
QuasiIsoAt f i ↔ HomologicalComplex.ExactAt L i
theorem
quasiIsoAt_iff_exactAt'
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
(hL : HomologicalComplex.ExactAt L i)
:
QuasiIsoAt f i ↔ HomologicalComplex.ExactAt K i
instance
instIsIsoHomologyHomologyMap
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[hf : QuasiIsoAt f i]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
isoOfQuasiIsoAt_hom
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[QuasiIsoAt f i]
:
(isoOfQuasiIsoAt f i).hom = HomologicalComplex.homologyMap f i
noncomputable def
isoOfQuasiIsoAt
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[QuasiIsoAt f 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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[QuasiIsoAt f i]
{Z : C}
(h : HomologicalComplex.homology K i ⟶ Z)
:
@[simp]
theorem
isoOfQuasiIsoAt_hom_inv_id
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[QuasiIsoAt f i]
:
@[simp]
theorem
isoOfQuasiIsoAt_inv_hom_id_assoc
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[QuasiIsoAt f i]
{Z : C}
(h : HomologicalComplex.homology L i ⟶ Z)
:
@[simp]
theorem
isoOfQuasiIsoAt_inv_hom_id
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[QuasiIsoAt f i]
:
theorem
CochainComplex.quasiIsoAt₀_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K : CochainComplex C ℕ}
{L : CochainComplex C ℕ}
(f : K ⟶ L)
[HomologicalComplex.HasHomology K 0]
[HomologicalComplex.HasHomology L 0]
[CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K 0 0 1)]
[CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' L 0 0 1)]
:
QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso
((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).toPrefunctor.map f)
theorem
ChainComplex.quasiIsoAt₀_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K : ChainComplex C ℕ}
{L : ChainComplex C ℕ}
(f : K ⟶ L)
[HomologicalComplex.HasHomology K 0]
[HomologicalComplex.HasHomology L 0]
[CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' K 1 0 0)]
[CategoryTheory.ShortComplex.HasHomology (HomologicalComplex.sc' L 1 0 0)]
:
QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso
((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).toPrefunctor.map f)
class
QuasiIso
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L 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 : ι), QuasiIsoAt f i
Instances
theorem
quasiIso_iff
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
:
QuasiIso f ↔ ∀ (i : ι), QuasiIsoAt f i
instance
quasiIso_of_isIso
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(f : K ⟶ L)
[CategoryTheory.IsIso f]
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
:
QuasiIso f
instance
quasiIsoAt_comp
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[HomologicalComplex.HasHomology M i]
[hφ : QuasiIsoAt φ i]
[hφ' : QuasiIsoAt φ' i]
:
Equations
- (_ : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i) = (_ : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i)
instance
quasiIso_comp
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology M i]
[hφ : QuasiIso φ]
[hφ' : QuasiIso φ']
:
Equations
- (_ : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')) = (_ : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ'))
theorem
quasiIsoAt_of_comp_left
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[HomologicalComplex.HasHomology M i]
[hφ : QuasiIsoAt φ i]
[hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i]
:
QuasiIsoAt φ' i
theorem
quasiIsoAt_iff_comp_left
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[HomologicalComplex.HasHomology M i]
[hφ : QuasiIsoAt φ i]
:
QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ' i
theorem
quasiIso_iff_comp_left
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology M i]
[hφ : QuasiIso φ]
:
QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ QuasiIso φ'
theorem
quasiIso_of_comp_left
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology M i]
[hφ : QuasiIso φ]
[hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')]
:
QuasiIso φ'
theorem
quasiIsoAt_of_comp_right
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[HomologicalComplex.HasHomology M i]
[hφ' : QuasiIsoAt φ' i]
[hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i]
:
QuasiIsoAt φ i
theorem
quasiIsoAt_iff_comp_right
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[HomologicalComplex.HasHomology M i]
[hφ' : QuasiIsoAt φ' i]
:
QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ i
theorem
quasiIso_iff_comp_right
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology M i]
[hφ' : QuasiIso φ']
:
theorem
quasiIso_of_comp_right
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology M i]
[hφ : QuasiIso φ']
[hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')]
:
QuasiIso φ
theorem
quasiIso_iff_of_arrow_mk_iso
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{K' : HomologicalComplex C c}
{L' : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : K' ⟶ L')
(e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ')
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology K' i]
[∀ (i : ι), HomologicalComplex.HasHomology L' i]
:
theorem
quasiIso_of_arrow_mk_iso
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
{K' : HomologicalComplex C c}
{L' : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : K' ⟶ L')
(e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ')
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology K' i]
[∀ (i : ι), HomologicalComplex.HasHomology L' i]
[hφ : QuasiIso φ]
:
QuasiIso φ'
instance
HomologicalComplex.quasiIsoAt_map_of_preservesHomology
{ι : Type u_2}
{c : ComplexShape ι}
{C₁ : Type u_3}
{C₂ : Type u_4}
[CategoryTheory.Category.{u_5, u_3} C₁]
[CategoryTheory.Category.{u_6, u_4} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K : HomologicalComplex C₁ c}
{L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.PreservesHomology F]
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj K) i]
[HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj L) i]
[hφ : QuasiIsoAt φ i]
:
QuasiIsoAt ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ) i
Equations
- (_ : QuasiIsoAt ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ) i) = (_ : QuasiIsoAt ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ) i)
theorem
HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology
{ι : Type u_2}
{c : ComplexShape ι}
{C₁ : Type u_3}
{C₂ : Type u_4}
[CategoryTheory.Category.{u_5, u_3} C₁]
[CategoryTheory.Category.{u_6, u_4} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K : HomologicalComplex C₁ c}
{L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.PreservesHomology F]
(i : ι)
[HomologicalComplex.HasHomology K i]
[HomologicalComplex.HasHomology L i]
[HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj K) i]
[HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj L) i]
[CategoryTheory.ReflectsIsomorphisms F]
:
QuasiIsoAt ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ) i ↔ QuasiIsoAt φ i
instance
HomologicalComplex.quasiIso_map_of_preservesHomology
{ι : Type u_2}
{c : ComplexShape ι}
{C₁ : Type u_3}
{C₂ : Type u_4}
[CategoryTheory.Category.{u_5, u_3} C₁]
[CategoryTheory.Category.{u_6, u_4} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K : HomologicalComplex C₁ c}
{L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.PreservesHomology F]
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj K) i]
[∀ (i : ι), HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj L) i]
[hφ : QuasiIso φ]
:
QuasiIso ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ)
Equations
- (_ : QuasiIso ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ)) = (_ : QuasiIso ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ))
theorem
HomologicalComplex.quasiIso_map_iff_of_preservesHomology
{ι : Type u_2}
{c : ComplexShape ι}
{C₁ : Type u_3}
{C₂ : Type u_4}
[CategoryTheory.Category.{u_5, u_3} C₁]
[CategoryTheory.Category.{u_6, u_4} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K : HomologicalComplex C₁ c}
{L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.PreservesHomology F]
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
[∀ (i : ι), HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj K) i]
[∀ (i : ι), HomologicalComplex.HasHomology ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.obj L) i]
[CategoryTheory.ReflectsIsomorphisms F]
:
QuasiIso ((CategoryTheory.Functor.mapHomologicalComplex F c).toPrefunctor.map φ) ↔ QuasiIso φ
def
HomologicalComplex.quasiIso
{ι : Type u_2}
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(c : ComplexShape ι)
[CategoryTheory.CategoryWithHomology C]
:
The morphism property on HomologicalComplex C c given by quasi-isomorphisms.
Equations
- HomologicalComplex.quasiIso C c f = QuasiIso f
Instances For
@[simp]
theorem
HomologicalComplex.mem_quasiIso_iff
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
[CategoryTheory.CategoryWithHomology C]
(f : K ⟶ L)
:
HomologicalComplex.quasiIso C c f ↔ QuasiIso f
instance
instQuasiIsoPreadditiveHasZeroMorphismsHom
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(e : HomotopyEquiv K L)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
:
QuasiIso e.hom
instance
instQuasiIsoPreadditiveHasZeroMorphismsInv
{ι : Type u_2}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K : HomologicalComplex C c}
{L : HomologicalComplex C c}
(e : HomotopyEquiv K L)
[∀ (i : ι), HomologicalComplex.HasHomology K i]
[∀ (i : ι), HomologicalComplex.HasHomology L i]
:
QuasiIso e.inv
Equations
- (_ : QuasiIso e.inv) = (_ : QuasiIso (HomotopyEquiv.symm e).hom)
theorem
homotopyEquivalences_subset_quasiIso
{ι : Type u_2}
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(c : ComplexShape ι)
[CategoryTheory.CategoryWithHomology C]
: