Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.pseudo_exact_of_exact

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ (b : CategoryTheory.Abelian.Pseudoelement S.X₂),
      CategoryTheory.Abelian.Pseudoelement.pseudoApply S.g b = 0 →
        ∃ a, CategoryTheory.Abelian.Pseudoelement.pseudoApply S.f a = b

Two morphisms in an exact sequence are exact on pseudoelements.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian