Pseudoelements in abelian categories

A pseudoelement of an object X in an abelian category C is an equivalence class of arrows ending in X, where two arrows are considered equivalent if we can find two epimorphisms with a common domain making a commutative square with the two arrows. While the construction shows that pseudoelements are actually subobjects of X rather than "elements", it is possible to chase these pseudoelements through commutative diagrams in an abelian category to prove exactness properties. This is done using some "diagram-chasing metatheorems" proved in this file. In many cases, a proof in the category of abelian groups can more or less directly be converted into a proof using pseudoelements.

A classic application of pseudoelements are diagram lemmas like the four lemma or the snake lemma.

Pseudoelements are in some ways weaker than actual elements in a concrete category. The most important limitation is that there is no extensionality principle: If f g : X ⟶ Y, then ∀ x ∈ X, f x = g x does not necessarily imply that f = g (however, if f = 0 or g = 0, it does). A corollary of this is that we can not define arrows in abelian categories by dictating their action on pseudoelements. Thus, a usual style of proofs in abelian categories is this: First, we construct some morphism using universal properties, and then we use diagram chasing of pseudoelements to verify that is has some desirable property such as exactness.

It should be noted that the Freyd-Mitchell embedding theorem gives a vastly stronger notion of pseudoelement (in particular one that gives extensionality). However, this theorem is quite difficult to prove and probably out of reach for a formal proof for the time being.

Main results

We define the type of pseudoelements of an object and, in particular, the zero pseudoelement.

We prove that every morphism maps the zero pseudoelement to the zero pseudoelement (apply_zero) and that a zero morphism maps every pseudoelement to the zero pseudoelement (zero_apply).

Here are the metatheorems we provide:

• A morphism f is zero if and only if it is the zero function on pseudoelements.
• A morphism f is an epimorphism if and only if it is surjective on pseudoelements.
• A morphism f is a monomorphism if and only if it is injective on pseudoelements if and only if ∀ a, f a = 0 → f = 0.
• A sequence f, g of morphisms is exact if and only if ∀ a, g (f a) = 0 and ∀ b, g b = 0 → ∃ a, f a = b.
• If f is a morphism and a, a' are such that f a = f a', then there is some pseudoelement a'' such that f a'' = 0 and for every g we have g a' = 0 → g a = g a''. We can think of a'' as a - a', but don't get too carried away by that: pseudoelements of an object do not form an abelian group.

Notations

We introduce coercions from an object of an abelian category to the set of its pseudoelements and from a morphism to the function it induces on pseudoelements.

These coercions must be explicitly enabled via local instances: attribute [local instance] objectToSort homToFun

Implementation notes

It appears that sometimes the coercion from morphisms to functions does not work, i.e., writing g a raises a "function expected" error. This error can be fixed by writing (g : X ⟶ Y) a.

References

• [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]

def CategoryTheory.Abelian.app {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) (a : CategoryTheory.Over P) : CategoryTheory.Over Q

This is just composition of morphisms in C. Another way to express this would be (Over.map f).obj a, but our definition has nicer definitional properties.

Equations

• CategoryTheory.Abelian.app f a = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp a.hom f)

@[simp]

theorem CategoryTheory.Abelian.app_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (f : P ⟶ Q) (a : CategoryTheory.Over P) : (CategoryTheory.Abelian.app f a).hom = CategoryTheory.CategoryStruct.comp a.hom f

def CategoryTheory.Abelian.PseudoEqual {C : Type u} [CategoryTheory.Category.{v, u} C] (P : C) (f : CategoryTheory.Over P) (g : CategoryTheory.Over P) : Prop

Two arrows f : X ⟶ P and g : Y ⟶ P are called pseudo-equal if there is some object R and epimorphisms p : R ⟶ X and q : R ⟶ Y such that p ≫ f = q ≫ g.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Abelian.pseudoEqual_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} : Reflexive (CategoryTheory.Abelian.PseudoEqual P)

theorem CategoryTheory.Abelian.pseudoEqual_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} : Symmetric (CategoryTheory.Abelian.PseudoEqual P)

theorem CategoryTheory.Abelian.pseudoEqual_trans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} : Transitive (CategoryTheory.Abelian.PseudoEqual P)

Pseudoequality is transitive: Just take the pullback. The pullback morphisms will be epimorphisms since in an abelian category, pullbacks of epimorphisms are epimorphisms.

def CategoryTheory.Abelian.Pseudoelement.setoid {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) : Setoid (CategoryTheory.Over P)

The arrows with codomain P equipped with the equivalence relation of being pseudo-equal.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Abelian.Pseudoelement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) : Type (max u v)

A Pseudoelement of P is just an equivalence class of arrows ending in P by being pseudo-equal.

Equations

• CategoryTheory.Abelian.Pseudoelement P = Quotient (CategoryTheory.Abelian.Pseudoelement.setoid P)

def CategoryTheory.Abelian.Pseudoelement.objectToSort {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CoeSort C (Type (max u v))

A coercion from an object of an abelian category to its pseudoelements.

Equations

• CategoryTheory.Abelian.Pseudoelement.objectToSort = { coe := fun (P : C) => CategoryTheory.Abelian.Pseudoelement P }

def CategoryTheory.Abelian.Pseudoelement.overToSort {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} : Coe (CategoryTheory.Over P) (CategoryTheory.Abelian.Pseudoelement P)

A coercion from an arrow with codomain P to its associated pseudoelement.

Equations

• CategoryTheory.Abelian.Pseudoelement.overToSort = { coe := Quot.mk (CategoryTheory.Abelian.PseudoEqual P) }

theorem CategoryTheory.Abelian.Pseudoelement.over_coe_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (a : Q ⟶ P) : Quot.mk (CategoryTheory.Abelian.PseudoEqual P) (CategoryTheory.Over.mk a) = ⟦CategoryTheory.Over.mk a⟧

theorem CategoryTheory.Abelian.Pseudoelement.pseudoApply_aux {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) (a : CategoryTheory.Over P) (b : CategoryTheory.Over P) : a ≈ b → CategoryTheory.Abelian.app f a ≈ CategoryTheory.Abelian.app f b

If two elements are pseudo-equal, then their composition with a morphism is, too.

def CategoryTheory.Abelian.Pseudoelement.pseudoApply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Abelian.Pseudoelement P → CategoryTheory.Abelian.Pseudoelement Q

A morphism f induces a function pseudoApply f on pseudoelements.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Abelian.Pseudoelement.homToFun {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} : CoeFun (P ⟶ Q) fun (x : P ⟶ Q) => CategoryTheory.Abelian.Pseudoelement P → CategoryTheory.Abelian.Pseudoelement Q

A coercion from morphisms to functions on pseudoelements.

Equations

• CategoryTheory.Abelian.Pseudoelement.homToFun = { coe := CategoryTheory.Abelian.Pseudoelement.pseudoApply }

theorem CategoryTheory.Abelian.Pseudoelement.pseudoApply_mk' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) (a : CategoryTheory.Over P) : CategoryTheory.Abelian.Pseudoelement.pseudoApply f ⟦a⟧ = ⟦CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp a.hom f)⟧

theorem CategoryTheory.Abelian.Pseudoelement.comp_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} {R : C} (f : P ⟶ Q) (g : Q ⟶ R) (a : CategoryTheory.Abelian.Pseudoelement P) : CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g) a = CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a)

Applying a pseudoelement to a composition of morphisms is the same as composing with each morphism. Sadly, this is not a definitional equality, but at least it is true.

theorem CategoryTheory.Abelian.Pseudoelement.comp_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} {R : C} (f : P ⟶ Q) (g : Q ⟶ R) : CategoryTheory.Abelian.Pseudoelement.pseudoApply g ∘ CategoryTheory.Abelian.Pseudoelement.pseudoApply f = CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.CategoryStruct.comp f g)

Composition of functions on pseudoelements is composition of morphisms.

In this section we prove that for every P there is an equivalence class that contains precisely all the zero morphisms ending in P and use this to define the zero pseudoelement.

theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} (Q : C) (f : CategoryTheory.Over P) : f ≈ CategoryTheory.Over.mk 0 ↔ f.hom = 0

The arrows pseudo-equal to a zero morphism are precisely the zero morphisms.

theorem CategoryTheory.Abelian.Pseudoelement.zero_eq_zero' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} {R : C} : ⟦CategoryTheory.Over.mk 0⟧ = ⟦CategoryTheory.Over.mk 0⟧

def CategoryTheory.Abelian.Pseudoelement.pseudoZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} : CategoryTheory.Abelian.Pseudoelement P

The zero pseudoelement is the class of a zero morphism.

Equations

• CategoryTheory.Abelian.Pseudoelement.pseudoZero = ⟦CategoryTheory.Over.mk 0⟧

instance CategoryTheory.Abelian.Pseudoelement.hasZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} : Zero (CategoryTheory.Abelian.Pseudoelement P)

Equations

• CategoryTheory.Abelian.Pseudoelement.hasZero = { zero := CategoryTheory.Abelian.Pseudoelement.pseudoZero }

instance CategoryTheory.Abelian.Pseudoelement.instInhabitedPseudoelement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} : Inhabited (CategoryTheory.Abelian.Pseudoelement P)

Equations

• CategoryTheory.Abelian.Pseudoelement.instInhabitedPseudoelement = { default := 0 }

theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} : 0 = ⟦CategoryTheory.Over.mk 0⟧

@[simp]

theorem CategoryTheory.Abelian.Pseudoelement.zero_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} : ⟦CategoryTheory.Over.mk 0⟧ = 0

theorem CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} (a : CategoryTheory.Over P) : Quot.mk (CategoryTheory.Abelian.PseudoEqual P) a = 0 ↔ a.hom = 0

The pseudoelement induced by an arrow is zero precisely when that arrow is zero.

@[simp]

theorem CategoryTheory.Abelian.Pseudoelement.apply_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : CategoryTheory.Abelian.Pseudoelement.pseudoApply f 0 = 0

Morphisms map the zero pseudoelement to the zero pseudoelement.

@[simp]

theorem CategoryTheory.Abelian.Pseudoelement.zero_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} (Q : C) (a : CategoryTheory.Abelian.Pseudoelement P) : CategoryTheory.Abelian.Pseudoelement.pseudoApply 0 a = 0

The zero morphism maps every pseudoelement to 0.

theorem CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) → f = 0

An extensionality lemma for being the zero arrow.

theorem CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) → 0 = f

theorem CategoryTheory.Abelian.Pseudoelement.eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : f = 0 ↔ ∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0

theorem CategoryTheory.Abelian.Pseudoelement.pseudo_injective_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Mono f] : Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)

A monomorphism is injective on pseudoelements.

theorem CategoryTheory.Abelian.Pseudoelement.zero_of_map_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) → ∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0

A morphism that is injective on pseudoelements only maps the zero element to zero.

theorem CategoryTheory.Abelian.Pseudoelement.mono_of_zero_of_map_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0) → CategoryTheory.Mono f

A morphism that only maps the zero pseudoelement to zero is a monomorphism.

theorem CategoryTheory.Abelian.Pseudoelement.pseudo_surjective_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) [CategoryTheory.Epi f] : Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)

An epimorphism is surjective on pseudoelements.

theorem CategoryTheory.Abelian.Pseudoelement.epi_of_pseudo_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) : Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) → CategoryTheory.Epi f

A morphism that is surjective on pseudoelements is an epimorphism.

theorem CategoryTheory.Abelian.Pseudoelement.pseudo_exact_of_exact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} {R : C} {f : P ⟶ Q} {g : Q ⟶ R} (h : CategoryTheory.Exact f g) : (∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a) = 0) ∧ ∀ (b : CategoryTheory.Abelian.Pseudoelement Q), CategoryTheory.Abelian.Pseudoelement.pseudoApply g b = 0 → ∃ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = b

Two morphisms in an exact sequence are exact on pseudoelements.

theorem CategoryTheory.Abelian.Pseudoelement.apply_eq_zero_of_comp_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} {R : C} (f : Q ⟶ R) (a : P ⟶ Q) : CategoryTheory.CategoryStruct.comp a f = 0 → CategoryTheory.Abelian.Pseudoelement.pseudoApply f (Quot.mk (CategoryTheory.Abelian.PseudoEqual Q) (CategoryTheory.Over.mk a)) = 0

theorem CategoryTheory.Abelian.Pseudoelement.exact_of_pseudo_exact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} {R : C} (f : P ⟶ Q) (g : Q ⟶ R) : ((∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a) = 0) ∧ ∀ (b : CategoryTheory.Abelian.Pseudoelement Q), CategoryTheory.Abelian.Pseudoelement.pseudoApply g b = 0 → ∃ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = b) → CategoryTheory.Exact f g

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

theorem CategoryTheory.Abelian.Pseudoelement.sub_of_eq_image {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : C} {Q : C} (f : P ⟶ Q) (x : CategoryTheory.Abelian.Pseudoelement P) (y : CategoryTheory.Abelian.Pseudoelement P) : CategoryTheory.Abelian.Pseudoelement.pseudoApply f x = CategoryTheory.Abelian.Pseudoelement.pseudoApply f y → ∃ (z : CategoryTheory.Abelian.Pseudoelement P), 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.

theorem CategoryTheory.Abelian.Pseudoelement.pseudo_pullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasPullbacks C] {P : C} {Q : C} {R : C} {f : P ⟶ R} {g : Q ⟶ R} {p : CategoryTheory.Abelian.Pseudoelement P} {q : CategoryTheory.Abelian.Pseudoelement Q} : CategoryTheory.Abelian.Pseudoelement.pseudoApply f p = CategoryTheory.Abelian.Pseudoelement.pseudoApply g q → ∃ (s : CategoryTheory.Abelian.Pseudoelement (CategoryTheory.Limits.pullback f g)), CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.pullback.fst s = p ∧ CategoryTheory.Abelian.Pseudoelement.pseudoApply CategoryTheory.Limits.pullback.snd s = q

If f : P ⟶ R and g : Q ⟶ R are morphisms and p : P and q : Q are pseudoelements such that f p = g q, then there is some s : pullback f g such that fst s = p and snd s = q.

Remark: Borceux claims that s is unique, but this is false. See Counterexamples/Pseudoelement.lean for details.

theorem CategoryTheory.Abelian.Pseudoelement.ModuleCat.eq_range_of_pseudoequal {R : Type u_1} [CommRing R] {G : ModuleCat R} {x : CategoryTheory.Over G} {y : CategoryTheory.Over G} (h : CategoryTheory.Abelian.PseudoEqual G x y) : LinearMap.range x.hom = LinearMap.range y.hom

In the category Module R, if x and y are pseudoequal, then the range of the associated morphisms is the same.