Quasi-isomorphisms #
A chain map is a quasi-isomorphism if it induces isomorphisms on homology.
class
QuasiIsoAt
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology 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).map f)
Instances
theorem
quasiIsoAt_iff
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
:
QuasiIsoAt f i ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor C c i).map f)
instance
quasiIsoAt_of_isIso
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
[CategoryTheory.IsIso f]
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
:
QuasiIsoAt f i
Equations
- ⋯ = ⋯
theorem
quasiIsoAt_iff'
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i j k : ι)
(hi : c.prev j = i)
(hk : c.next j = k)
[K.HasHomology j]
[L.HasHomology j]
[(K.sc' i j k).HasHomology]
[(L.sc' i j k).HasHomology]
:
QuasiIsoAt f j ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C c i j k).map f)
theorem
quasiIsoAt_iff_isIso_homologyMap
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
:
theorem
quasiIsoAt_iff_exactAt
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
(hK : K.ExactAt i)
:
QuasiIsoAt f i ↔ L.ExactAt i
theorem
quasiIsoAt_iff_exactAt'
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
(hL : L.ExactAt i)
:
QuasiIsoAt f i ↔ K.ExactAt i
instance
instIsIsoHomologyMapOfQuasiIsoAt
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[hf : QuasiIsoAt f i]
:
Equations
- ⋯ = ⋯
noncomputable def
isoOfQuasiIsoAt
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[QuasiIsoAt f i]
:
K.homology i ≅ L.homology 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
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[QuasiIsoAt f i]
:
(isoOfQuasiIsoAt f i).hom = HomologicalComplex.homologyMap f i
@[simp]
theorem
isoOfQuasiIsoAt_hom_inv_id
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[QuasiIsoAt f i]
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i) (isoOfQuasiIsoAt f i).inv = CategoryTheory.CategoryStruct.id (K.homology i)
@[simp]
theorem
isoOfQuasiIsoAt_hom_inv_id_assoc
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[QuasiIsoAt f i]
{Z : C}
(h : K.homology i ⟶ Z)
:
@[simp]
theorem
isoOfQuasiIsoAt_inv_hom_id
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[QuasiIsoAt f i]
:
CategoryTheory.CategoryStruct.comp (isoOfQuasiIsoAt f i).inv (HomologicalComplex.homologyMap f i) = CategoryTheory.CategoryStruct.id (L.homology i)
@[simp]
theorem
isoOfQuasiIsoAt_inv_hom_id_assoc
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[QuasiIsoAt f i]
{Z : C}
(h : L.homology i ⟶ Z)
:
theorem
CochainComplex.quasiIsoAt₀_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K L : CochainComplex C ℕ}
(f : K ⟶ L)
[HomologicalComplex.HasHomology K 0]
[HomologicalComplex.HasHomology L 0]
[(HomologicalComplex.sc' K 0 0 1).HasHomology]
[(HomologicalComplex.sc' L 0 0 1).HasHomology]
:
QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map f)
theorem
ChainComplex.quasiIsoAt₀_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K L : ChainComplex C ℕ}
(f : K ⟶ L)
[HomologicalComplex.HasHomology K 0]
[HomologicalComplex.HasHomology L 0]
[(HomologicalComplex.sc' K 1 0 0).HasHomology]
[(HomologicalComplex.sc' L 1 0 0).HasHomology]
:
QuasiIsoAt f 0 ↔ CategoryTheory.ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map f)
class
QuasiIso
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology 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_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
:
QuasiIso f ↔ ∀ (i : ι), QuasiIsoAt f i
instance
quasiIso_of_isIso
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(f : K ⟶ L)
[CategoryTheory.IsIso f]
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
:
QuasiIso f
Equations
- ⋯ = ⋯
instance
quasiIsoAt_comp
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[M.HasHomology i]
[hφ : QuasiIsoAt φ i]
[hφ' : QuasiIsoAt φ' i]
:
Equations
- ⋯ = ⋯
instance
quasiIso_comp
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), M.HasHomology i]
[hφ : QuasiIso φ]
[hφ' : QuasiIso φ']
:
Equations
- ⋯ = ⋯
theorem
quasiIsoAt_of_comp_left
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[M.HasHomology i]
[hφ : QuasiIsoAt φ i]
[hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i]
:
QuasiIsoAt φ' i
theorem
quasiIsoAt_iff_comp_left
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[M.HasHomology i]
[hφ : QuasiIsoAt φ i]
:
QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ' i
theorem
quasiIso_iff_comp_left
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), M.HasHomology i]
[hφ : QuasiIso φ]
:
QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ QuasiIso φ'
theorem
quasiIso_of_comp_left
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), M.HasHomology i]
[hφ : QuasiIso φ]
[hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')]
:
QuasiIso φ'
theorem
quasiIsoAt_of_comp_right
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[M.HasHomology i]
[hφ' : QuasiIsoAt φ' i]
[hφφ' : QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i]
:
QuasiIsoAt φ i
theorem
quasiIsoAt_iff_comp_right
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[M.HasHomology i]
[hφ' : QuasiIsoAt φ' i]
:
QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i ↔ QuasiIsoAt φ i
theorem
quasiIso_iff_comp_right
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), M.HasHomology i]
[hφ' : QuasiIso φ']
:
theorem
quasiIso_of_comp_right
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L M : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : L ⟶ M)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), M.HasHomology i]
[hφ : QuasiIso φ']
[hφφ' : QuasiIso (CategoryTheory.CategoryStruct.comp φ φ')]
:
QuasiIso φ
theorem
quasiIso_iff_of_arrow_mk_iso
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L K' L' : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : K' ⟶ L')
(e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ')
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), K'.HasHomology i]
[∀ (i : ι), L'.HasHomology i]
:
theorem
quasiIso_of_arrow_mk_iso
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L K' L' : HomologicalComplex C c}
(φ : K ⟶ L)
(φ' : K' ⟶ L')
(e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ')
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), K'.HasHomology i]
[∀ (i : ι), L'.HasHomology i]
[hφ : QuasiIso φ]
:
QuasiIso φ'
instance
HomologicalComplex.quasiIsoAt_map_of_preservesHomology
{ι : Type u_1}
{c : ComplexShape ι}
{C₁ : Type u_2}
{C₂ : Type u_3}
[CategoryTheory.Category.{u_4, u_2} C₁]
[CategoryTheory.Category.{u_5, u_3} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[F.Additive]
[F.PreservesHomology]
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[((F.mapHomologicalComplex c).obj K).HasHomology i]
[((F.mapHomologicalComplex c).obj L).HasHomology i]
[hφ : QuasiIsoAt φ i]
:
QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i
Equations
- ⋯ = ⋯
theorem
HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology
{ι : Type u_1}
{c : ComplexShape ι}
{C₁ : Type u_2}
{C₂ : Type u_3}
[CategoryTheory.Category.{u_4, u_2} C₁]
[CategoryTheory.Category.{u_5, u_3} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[F.Additive]
[F.PreservesHomology]
(i : ι)
[K.HasHomology i]
[L.HasHomology i]
[((F.mapHomologicalComplex c).obj K).HasHomology i]
[((F.mapHomologicalComplex c).obj L).HasHomology i]
[F.ReflectsIsomorphisms]
:
QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i
instance
HomologicalComplex.quasiIso_map_of_preservesHomology
{ι : Type u_1}
{c : ComplexShape ι}
{C₁ : Type u_2}
{C₂ : Type u_3}
[CategoryTheory.Category.{u_4, u_2} C₁]
[CategoryTheory.Category.{u_5, u_3} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[F.Additive]
[F.PreservesHomology]
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i]
[∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i]
[hφ : QuasiIso φ]
:
QuasiIso ((F.mapHomologicalComplex c).map φ)
Equations
- ⋯ = ⋯
theorem
HomologicalComplex.quasiIso_map_iff_of_preservesHomology
{ι : Type u_1}
{c : ComplexShape ι}
{C₁ : Type u_2}
{C₂ : Type u_3}
[CategoryTheory.Category.{u_4, u_2} C₁]
[CategoryTheory.Category.{u_5, u_3} C₂]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
{K L : HomologicalComplex C₁ c}
(φ : K ⟶ L)
(F : CategoryTheory.Functor C₁ C₂)
[F.Additive]
[F.PreservesHomology]
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
[∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i]
[∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i]
[F.ReflectsIsomorphisms]
:
def
HomologicalComplex.quasiIso
{ι : Type u_1}
(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_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
[CategoryTheory.CategoryWithHomology C]
(f : K ⟶ L)
:
HomologicalComplex.quasiIso C c f ↔ QuasiIso f
instance
instQuasiIsoHom
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(e : HomotopyEquiv K L)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
:
QuasiIso e.hom
Equations
- ⋯ = ⋯
instance
instQuasiIsoInv
{ι : Type u_1}
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{c : ComplexShape ι}
{K L : HomologicalComplex C c}
(e : HomotopyEquiv K L)
[∀ (i : ι), K.HasHomology i]
[∀ (i : ι), L.HasHomology i]
:
QuasiIso e.inv
Equations
- ⋯ = ⋯
theorem
homotopyEquivalences_le_quasiIso
{ι : Type u_1}
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(c : ComplexShape ι)
[CategoryTheory.CategoryWithHomology C]
: