Theorems · Theorem · category theory

HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology

∀ {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C₂] [inst_2 : CategoryTheory.Preadditive C₁]
  [inst_3 : CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L)
  (F : CategoryTheory.Functor C₁ C₂) [inst_4 : F.Additive] [F.PreservesHomology] (i : ι) [inst_6 : K.HasHomology i]
  [inst_7 : L.HasHomology i] [inst_8 : ((F.mapHomologicalComplex c).obj K).HasHomology i]
  [inst_9 : ((F.mapHomologicalComplex c).obj L).HasHomology i] [F.ReflectsIsomorphisms],
  QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i

Defined in

Mathlib.Algebra.Homology.QuasiIso

Cited by

1 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.PreadditiveCategoryTheory.Functor.AdditiveCategoryTheory.Functor.PreservesHomologyHomologicalComplex.HasHomologyHomologicalComplex.HasHomologyHomologicalComplex.HasHomologyHomologicalComplex.HasHomologyCategoryTheory.Functor.ReflectsIsomorphisms