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 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, you can see the actual Lean code here.
