Theorems · Theorem · category theory

CategoryTheory.ShortComplex.quasiIso_iff_of_zeros

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  S₁.f = 0 →
    ∀ (hg₁ : S₁.g = 0),
      S₂.f = 0 →
        (CategoryTheory.ShortComplex.QuasiIso φ ↔
          { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ CategoryTheory.Mono φ.τ₂)

Given a morphism of short complexes φ : S₁ ⟶ S₂ in an abelian category, if S₁.f and S₁.g are zero (e.g. when S₁ is of the form 0 ⟶ S₁.X₂ ⟶ 0) and S₂.f = 0 (e.g when S₂ is of the form 0 ⟶ S₂.X₂ ⟶ S₂.X₃), then φ is a quasi-isomorphism iff the obvious short complex S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃ is exact and φ.τ₂ is a mono.

Defined in

Mathlib.Algebra.Homology.ShortComplex.Exact

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian