Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.exact_of_pseudo_exact

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

If two morphisms are exact on pseudoelements, they are exact.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian