Refinements #

In order to prove injectivity/surjectivity/exactness properties for diagrams in the category of abelian groups, we often need to do diagram chases. Some of these can be carried out in more general abelian categories: for example, a morphism X ⟶ Y in an abelian category C is a monomorphism if and only if for all A : C, the induced map (A ⟶ X) → (A ⟶ Y) of abelian groups is a monomorphism, i.e. injective. Alternatively, the yoneda presheaf functor which sends X to the presheaf of maps A ⟶ X for all A : C preserves and reflects monomorphisms.

However, if p : X ⟶ Y is an epimorphism in C and A : C, (A ⟶ X) → (A ⟶ Y) may fail to be surjective (unless p is a split epimorphism).

In this file, the basic result is epi_iff_surjective_up_to_refinements which states that f : X ⟶ Y is a morphism in an abelian category, then it is an epimorphism if and only if for all y : A ⟶ Y, there exists an epimorphism π : A' ⟶ A and x : A' ⟶ X such that π ≫ y = x ≫ f. In order words, if we allow a precomposition with an epimorphism, we may lift a morphism to Y to a morphism to X. Following unpublished notes by George Bergman, we shall say that the precomposition by an epimorphism π ≫ y is a refinement of y. Then, we get that an epimorphism is a morphism that is "surjective up to refinements". (This result is similar to the fact that a morphism of sheaves on a topological space or a site is epi iff sections can be lifted locally. Then, arguing "up to refinements" is very similar to arguing locally for a Grothendieck topology (TODO: show that it corresponds to arguing for the canonical topology on the abelian category C by showing that a morphism in C is an epi iff the corresponding morphisms of sheaves for the canonical topology is an epi, and that the criteria epi_iff_surjective_up_to_refinements could be deduced from this equivalence.)

Similarly, it is possible to show that a short complex in an abelian category is exact if and only if it is exact up to refinements (see ShortComplex.exact_iff_exact_up_to_refinements).

As it is outlined in the documentation of the file CategoryTheory.Abelian.Pseudoelements, the Freyd-Mitchell embedding theorem implies the existence of a faithful and exact functor ι from an abelian category C to the category of abelian groups. If we define a pseudo-element of X : C to be an element in ι.obj X, one may do diagram chases in any abelian category using these pseudo-elements. However, using this approach would require proving this embedding theorem! Currently, mathlib contains a weaker notion of pseudo-elements CategoryTheory.Abelian.Pseudoelements. Some theorems can be obtained using this notion, but there is the issue that for this notion of pseudo-elements a morphism X ⟶ Y in C is not determined by its action on pseudo-elements (see also Counterexamples/Pseudoelement). On the contrary, the approach consisting of working up to refinements does not require the introduction of other types: we only need to work with morphisms A ⟶ X in C which we may consider as being "sort of elements of X". One may carry diagram-chasing by tracking these morphisms and sometimes introducing an auxiliary epimorphism A' ⟶ A.

References #