Theorems · Theorem · category theory

CochainComplex.isKInjective_of_injective_aux

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) (α : CochainComplex.HomComplex.Cochain K L (-1)) (n m : ℤ),
  n + 1 = m →
    HomologicalComplex.ExactAt K m →
      ∀ [CategoryTheory.Injective (L.X m)],
        (CochainComplex.HomComplex.δ (-1) 0 α).EqUpTo (CochainComplex.HomComplex.Cochain.ofHom f) n →
          ∃ h,
            (CochainComplex.HomComplex.δ (-1) 0 (α + CochainComplex.HomComplex.Cochain.single h (-1))).EqUpTo
              (CochainComplex.HomComplex.Cochain.ofHom f) m

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.Injective