Let $\mathcal{A}$ be an abelian category, and let $X$ an object of $\mathcal{A}$. Recall that a *pseudoelement* of $X$ is an equivalence class of arrows $X\_1 \to X$, where $x\_1 \colon X\_1 \to X$ and $x\_2 \colon X\_2 \to X$ are equivalent if there is an object $P$ and *epimorphisms* $p\_1 \colon P \to X\_1$ and $p\_2 \colon P \to X\_2$ such that $x\_1 \circ p\_1= x\_2 \circ p\_2$. We write $x \in^\ast X$ to denote that $x$ is a pseudoelement of $X$. If $x \in^\ast X$ and $f \colon X \to Y$, then $f(x) \in^\ast Y$ is obtained by composition.


Pseudoelements are pretty nice, for example a morphism is equal to $0$ if and only if it sends all pseudoelements to $0$, and we can characterize monomorphisms (resp. epimorphisms) in terms of pseudoelements, as one expects. Similarly we can check if a sequence is exact by testing exactness on pseudoelements. Of course there are limitations, for example we can not test if two morphisms are equal on pseudoelements (in contrast with the Freyd–Mitchell embedding theorem).


A natural problem is what happens with pullbacks. Let $f \colon X \to Z$ and $g \colon Y \to Z$ be morphisms, and let $x \in^\ast X$ and $y \in^\ast Y$ such that $f(x) = g(y)$. It's easy to construct $s \in^\ast X \times\_Z Y$ such that $\pi\_1(s) = x$ and $\pi\_2(s) = y$, by universal property of the pullback. Now, we would like $s$ to be unique, and indeed Francis Borceux in his "Handbook of Categorical Algebra: Volume 2", Proposition 1.9.5, claims so. The proof is only sketched, and essentially Borceux says "All the relevant epimorphisms can, by successive pullbacks, be replaced by epimorphisms with the same domain, from which the claim follows". It's not completely clear how to write down the details, see for example [this](https://math.stackexchange.com/questions/3609374/replacing-a-family-of-epimorphisms-by-epimorphisms-with-the-same-domain-by-formi) stackexchange question, with a partial answer.


I've tried to prove the theorem by myself, essentially following Borceux's idea of constructing several pullbacks, but I am unable to finish the proof. To simplify the notation, let's consider the case of the product, so $Z=0$ in the above discussion. Let $a \colon A \to X \times Y \in^\ast X \times Y$ and $b \colon B \to X \times Y \in^\ast X \times Y$ be such that $\pi\_1(a)=\pi\_1(b)$ and $\pi\_2(a)=\pi\_2(b)$. So there are epimorphisms $a\_1 \colon Z\_1 \to A$, $b\_1 \colon Z\_1 \to B$, $a\_2 \colon Z\_2 \to A$ and $b\_2 \colon Z\_2 \to B$ such that $\pi\_1 \circ a \circ a\_1 = \pi\_1 \circ b \circ b\_1$ and $\pi\_2 \circ a \circ a\_2 = \pi\_2 \circ b \circ b\_2$. To construct the required epimorphisms we consider $P\_a = Z\_1 \times\_A Z\_2$ and $P\_b = Z\_1 \times\_B Z\_2$. We finally set $P = P\_a \times\_{Z\_1} P\_b$, where $P\_a \to Z\_1$ and $P\_b \to Z\_1$ are the first projections. We write $f\_a : P \to A := a\_1 \circ \pi\_1 \circ \pi\_1$ (two different $\pi\_1$) and $f\_b : P \to B := b\_1 \circ \pi\_1 \circ \pi\_2$. Then $f\_a$ and $f\_b$ are epimorphisms. We need to prove that $a \circ f\_a= b \circ f\_b$ and it is enough to prove that $\pi\_1 \circ a \circ f\_a= \pi\_1 \circ b \circ f\_b$ and $\pi\_2 \circ a \circ f\_a= \pi\_2 \circ b \circ f\_b$. The first one follows immediately by $\pi\_1 \circ a \circ a\_1 = \pi\_1 \circ b \circ b\_1$ and the commuting square of the pullback. I don't see how to prove the second equality, I tried essentially all the combinations of the two equalities we have and all the pullback squares, but it didn't work.


Of course one can try to construct different epimorphisms, but all the constructions I tried (even those more symmetric then the one above) end up with exactly the same equality to prove.


Does someone know a complete proof of this result? Thanks!


PS: I realized I am not able to prove it trying to formalize the result in Lean, in a lemma for the [Liquid Tensor Experiment](https://github.com/leanprover-community/lean-liquid/), you can see the actual Lean code [here](https://github.com/leanprover-community/lean-liquid/blob/ed8f03da6f8cdde28f936aeab8c0c21c457e45a7/src/for_mathlib/derived/les.lean#L84).



Pullback and pseudoelements
**The claim stated in the question is false, and the statement of Lemma 1.9.5 in Borceux is unclear, but seems wrong.** To be clear, the claim in this question is that for any Abelian category $\newcommand{\A}{\mathcal{A}}\A$, and maps $f:X \to Z$, $g : Y \to Z$, and pseudo-elements $[x]$, $[y]$ such that $f[x] = g[y]$, there is a $unique$ pseudo-element $[p]$ of $X \times\_Z Y$ with $\pi\_1[p] = [x]$, $\pi\_2[p]=[y]$. More concisely, the claim is that the “pseudo-elements” functor $\A \to \mathrm{Set}$ preserves pullbacks. (Borceux Lemma 1.9.5 claims that $[p]$ is “pseudo-unique”; from the “proof” sketch, I agree it seems like he intends this to mean “unique, as a pseudo-element”, but conceivably he had something else in mind.)


Work for concreteness in $\newcommand{\Ab}{\mathrm{Ab}}\Ab$. Then maps $x\_1 \colon X\_1 \to X$, $x\_2 \colon X\_2 \to X$ are equivalent as pseudo-elements if and only if they have the same image. (The “only if” direction is clear; for the “if”, note that in this case the projections $X\_1 \times\_X X\_2 \to X\_i$ are epi.) So **pseudo-elements of $X$ correspond to subobjects/subgroups of $X$**. Borceux notes this fact in the closing discussion of §1.9.


But now it’s easy to see this doesn’t preserve pullbacks. For instance, it doesn’t preserve the product $\newcommand{\Q}{\mathbb{Q}} \Q \times \Q$: the subgroups $\{ (x,x) | x \in \Q \}$ and $\{ (x,2x) | x \in \Q \}$ have the same images under each projection, but are not the same. In terms of pseudo-elements, the maps $s\_1, s\_2 : \Q \to \Q \times \Q$ given by $s\_i(x)=(x,ix)$ are not equal as pseudo-elements of $\Q \times \Q$, but their images under each projection are equal as pseudo-elements of $\Q$.


