# 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: indeed,
show that it corresponds to the "refinements" topology on an
abelian category `C`

that is defined by saying that
a sieve is covering if it contains an epimorphism).

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 #

- George Bergman, A note on abelian categories – translating element-chasing proofs, and exact embedding in abelian groups (1974) http://math.berkeley.edu/~gbergman/papers/unpub/elem-chase.pdf