Regular Projective Objects in the Exact Completion of a Finitely Complete Category Everything I'm talking about is contained in the following:


*

*Carboni & Celia Magno, The free exact category on a left exact one;

*Carboni, Some free constructions in realizability and proof theory.
If $C$ is a finitely complete category, it can be embedded into an exact category $Ex(C)$, in such a way that this embedding $C\hookrightarrow Ex(C)$ preserves finte limits and is initial among all the possible finite limit preserving functors $C \to D$ where $D$ is an exact category.
The category $Ex(C)$ is defined as follows [$(1)-(2)-(2')-(3)-(4)$].
$(1)$ An object is a pseudo-equivalence relation $R \to X\times X$ in $C$. A pseudo equivalence relation is almost an equivalence relation, with the only difference that it is not required to be a monomorphism (in particular, if a pseudo-equivalence relation has a regular epi-mono factorization then its image is an equivalence relation).
$(2)$ An arrow between two pseudo-equivalence relations is an arrow of $C$ between their supports that agrees with the pseudo-equivalence relations. For instance, if $R \to X\times X$ and $S \to Y\times Y$ are pseudo-equivalence relations and $f$ is an arrow $X\to Y$, then $f$ is an arrow of $Ex(C)$ iff:
for every arrow $x=\langle x_1,x_2\rangle \colon I \to X\times X$, if $x$ factors through $R$ then the arrow $(f\times f)x=\langle fx_1,fx_2\rangle \colon I \to Y\times Y$ factors through $S$ (if we were talking about sets, this would mean that, whenever $(x_1,x_2)\in R$ then $(fx_1,fx_2)\in S$),
or, equivalently, iff:
there is an arrow $R \xrightarrow{f'} S$ (not necessarily unique) making the obvious square commute.
$(2')$ Actually, we consider equivalent two such arrow $f,g \colon X \to Y$ such that for every $x \colon I \to X$, the arrow $\langle fx,gx\rangle \colon I \to Y \times Y$ factors through $S$ (again, set-theoretically this means that $(fx,gx) \in S$ for every $x\in X$). This happens precisely when $\langle f,g\rangle$ factors through $S$. Hence an arrow of $Ex(C)$ is an equivalence class, modulo this relation, of equivalence relation preserving parallel arrows.
$(3)$ One can verify that this equivalence relation between arrows agrees with the composition of $C$, hence we can define the composition in $Ex(C)$ of two classes as the class of the composition in $C$ of their representatives.
$(4)$ The embedding $C \hookrightarrow Ex(C)$ sends every object $X$ of $C$ to the trivial (pseudo-)equivalence relation $\langle 1_X,1_X\rangle \colon X \to X\times X$ and every arrow $X \to Y$ to itself. Obviously this defines an embedding and one can verify that it preserves finite limits.
One can prove that $Ex(C)$ is exact. In particular, the regular-epi mono factorization is obtained as follows: if $[f]$ is an arrow $(X,R) \to (Y,S)$, then its image is the arrow $(X,(f\times f)^*S)\to(Y,S)$ again represented by $f$, and the regular epimorphism $(X,R) \to (X,(f\times f)^*S)$ is the arrow represented by the identity $1_X$ (indeed, by the universal property of $(f\times f)^*S$, there is an arrow $R \to (f\times f)^*S$ making the obvious square commute - just consider the arrows $R \to X\times X$ and $f'$ in order to get it). Hence we know how the regular epimorphisms look like.
One can characterize the exact categories obtained through this procedure. Indeed if $D$ is an exact category with enough projective (means regular projective) objects and its full subcategory $P$ of its projective objects is closed under finite limits (that is, finitely complete) then $D \simeq Ex(P)$. Viceversa, if $C$ is a finitely complete category, then the inclusion of $C$ into $Ex(C)$ through the embedding $C \hookrightarrow Ex(C)$  verifies the following properties:
$(a)$ it is finitely complete (this is trivial because of $(4)$);
$(b)$ its objects are projective in $Ex(C)$ and the projective objects are enough;
$(c)$ its objects, up to isomorphism of $Ex(C)$, are precisely the projective objects of $Ex(C)$, that is, every projective object of $Ex(C)$ is in the essential image of $C \hookrightarrow Ex(C)$.
The only thing I can't prove is $\boldsymbol{(c)}$. Can someone help me working it out?
Maybe the proof that $Ex(C)$ has enough projectives can help: let $(X,R)$ be a pseudo equivalence relation over the object $X$ of $C$. After having proved that $(X,\langle 1_X,1_X\rangle)$ is projective, observe that the identity $1_X$ represents a regular epimorphism $(X,\langle 1_X,1_X\rangle) \to (X,R)$. I was trying to see if this is actually an isomorphism (i.e. a monomorphism - it's enough in such a category) assuming that $(X,R)$ is projective, but this doesn't seem to work.
 A: Solution by Fabio P.
Let $(X,R)$ be a projective object of $Ex(\mathcal{C})$. As we know, the identity $1_X$ represents a regular epimorphism $(X,\langle 1_X,1_X\rangle)\xrightarrow{c}(X,R)$. It is a wrong idea to try to prove that $c$ is an isomorphism. Indeed, $(X,R)$ turns out to be isomorphic to an object in the image of $\mathcal{C}\hookrightarrow Ex(\mathcal{C})$ which is not necessarily $(X,\langle 1_X,1_X\rangle)$.
As $(X,R)$ is projective, there is an arrow $X \xrightarrow{s}X$ of $\mathcal{C}$, representing a section $(X,R)\to (X,\langle 1_X,1_X\rangle)$ of $c$.
Let $(E,S)\xrightarrow{[e]}(X,\langle 1_X,1_X\rangle)$ be the equaliser of the couple $([s]c,[1_X])$ of arrows $(X,\langle 1_X,1_X\rangle)\to(X,\langle 1_X,1_X\rangle)$. Then $[e]$ is a monomorphism of $Ex(\mathcal{C})$, hence, up to precomposing by an isomorphism, we can assume (look at the exhibition we gave of the regular epi-mono factorisation in $Ex(\mathcal{C})$) that: $$S=(e\times e)^*\langle 1_X,1_X\rangle=\langle e^*1_X,e^*1_X\rangle=\langle 1_E,1_E\rangle.$$ Observe that the arrow $[s]$ equalises the pair $([s]c,[1_X])$. Hence, by the universal property of the arrow $[e]$, there is unique an arrow $(X,R)\xrightarrow{r}(E,\langle 1_E,1_E\rangle)$ such that $[e]r=[s]$.
We are done if $r$ is an isomorphism. This is indeed true, since:


*

*it is the case that $(c[e])r=c[s]=[1_X]=1_{(X,R)}$;

*it is the case that $[e]r(c[e])=[s]c[e]=[e]$, hence $r(c[e])=1_{(E,\langle 1_E,1_E\rangle)};$
that is, $c[e]$ is the inverse of $r$.
