Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.sub_of_eq_image

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  (x y : CategoryTheory.Abelian.Pseudoelement P),
  CategoryTheory.Abelian.Pseudoelement.pseudoApply f x = CategoryTheory.Abelian.Pseudoelement.pseudoApply f y →
    ∃ z,
      CategoryTheory.Abelian.Pseudoelement.pseudoApply f z = 0 ∧
        ∀ (R : C) (g : P ⟶ R),
          CategoryTheory.Abelian.Pseudoelement.pseudoApply g y = 0 →
            CategoryTheory.Abelian.Pseudoelement.pseudoApply g z = CategoryTheory.Abelian.Pseudoelement.pseudoApply g x

If two pseudoelements x and y have the same image under some morphism f, then we can form their "difference" z. This pseudoelement has the properties that f z = 0 and for all morphisms g, if g y = 0 then g z = g x.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian