Theorems · Theorem · category theory

HomologicalComplex.exactAt_iff_exact_up_to_refinements

∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι),
  c.prev j = i →
    c.next j = k →
      (K.ExactAt j ↔
        ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
          CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0 →
            ∃ A' π,
              ∃ (_ : CategoryTheory.Epi π),
                ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ (K.d i j))

Defined in

Mathlib.Algebra.Homology.Refinements

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian