Theorems · Theorem · category theory

CochainComplex.quasiIso_truncGEMap_iff

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i]
  (n : ℤ), QuasiIso (CochainComplex.truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

Defined in

Mathlib.Algebra.Homology.Embedding.CochainComplex

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroObjectHomologicalComplex.HasHomologyHomologicalComplex.HasHomology