Regular Projective Objects in the Exact Completion of a Finitely Complete Category

Question

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.

Answer 1

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$.