Defining along pullback preserves image in a regular category.

Question

In a regular category we can factor any morphism $A \xrightarrow{g} X$ as $A \xrightarrow{e} E \xrightarrow{m} X$ where $e$ is regular epi and $m$ is mono. This factorization is unique up to isomorphism and we call the subobject $E \xrightarrow{m} X$ represents the image of $f$ or $Im(f)$.

For an arrow $X \xrightarrow{f} Y$ and a subobject represented by $M \xrightarrow{m} Y$ we can make a pullback with some vertex $D$ that gives an arrow $D \xrightarrow{n} X$

We say $f^*(m) = n$.

The question is to prove

or equivalently, find a morphism $E \to C$ such that

commutes

I have trouble doing this. My thought was to use the uniqueness of factoring up to isomorphism, but the only suitable factorings are $A \xrightarrow{e} E \xrightarrow{fm} Y$ and $A \xrightarrow{B} C \xrightarrow{n} Y$, but $fm$ is not necessarily mono, so that didn't work out.

Answer 1

Factors $g=nc$ with $n$ image of $g$ and $c$ be a regular epimorphism. Consider the following commutative diagram where both squares are pullback: $\require{AMScd}$ \begin{CD} A@>>>B\\ @VeVV@VVcV\\ E@>>>C\\ @VmVV@VVnV\\ X@>>f>Y \end{CD} Then $m$ is a monomorphism, because pulling back preserves monomorphism and $e$ is a regular epimorphism because in a regular category pulling back preserves regular epimorphisms. By pullback pasting, the outer rectangle is a pullback as well. Consequently, you get a RegEpi-Mono factorization of $g'$. By uniqueness of RegEpi-Mono factorization, it follows that $m$ is the image of $g'$.

Answer 2

Here is another proof.

Let $p:\{(x,b):X\times B\mid f(x)=g(b)\}\to X$ be the obvious projection which corresponds to $g'$. The theorem to be proven is then $$\exists b:B.f(x)=g(b)\dashv\vdash\exists (x',b):\{(x',b):X\times B\mid f(x)=g(b)\}.x=x'$$ Each side of this inter-provability relation is a predicate on $X$. The left to right direction is easy to prove. If we know there exists a $b$ such that $f(x)=g(b)$ then $(x,b)$ is an element of $\{(x',b):X\times B\mid f(x)=g(b)\}$ and thus $x=x'$. The other direction is just as easy. If we know that there exists an $(x',b)$ such that $f(x')=g(b)$ and we know $x=x'$, then clearly we know that there exists a $b$ such that $f(x)=g(b)$. $\square$

Of course, the real work here is showing how the heck what all I just said relates to your original question. I mean, sure, everything I just said makes complete sense in $\mathbf{Set}$, but you're not working in $\mathbf{Set}$. This is the power of internal logic. It allows us to work as we "normally" do, but have the results hold in a much broader domain. In this case, we need to restrict ourselves to regular logic.

To just start to give a feel, let $P:R\rightarrowtail A\times B$ be a mono which we can think of as a predicate $P(a,b)$ where $a:A$ and $b:B$. Then $\exists b:B.P(a,b)$ is $Im(\pi_1\circ P)$ and is a subobject of $A$. In even just cartesian logic, we can identify an arrow with its graph (and see this, referenced therein). So we identify $g$ with the pullback of $id$ and $g$ which determines a subobject of $Y\times B$, and we take the image of the first projection which gives us the formula $\exists b:B.y=g(b)$. The pullback functor $f^*$ corresponds to substituting $f(x)$ for $y$ in the formula, i.e. $f^*(Im(g)) \equiv (\exists b:B.y=g(b))[f(x)/y] \equiv \exists b:B.f(x)=g(b)$. In fact, this is where the "real work" is. From this logical perspective, what pullback-stability states is that substitution commutes with existential quantification.

If we defined a regular category as a category which supports regular logic, then my proof above would be completely fine, and we could use similar reasoning to prove things like the existence and pullback-stability of images. On the other hand, if we define a regular category as a lex category with pullback-stable image factorizations, then my proof above would be circular. I want to show how image factorizations exist given this logical structure.

Clearly, the image of $f:X\to Y$ is $Im(f)\equiv\{y:Y\mid \exists x:X.f(x)=y\}$ which is a subobject, $m$, of $Y$. We need to show that there is a morphism $e:X\to Im(f)$ and that $f=m\circ e$. To do this, we use the graph of $f$, i.e. the relation on $X\times Y$, $f(x)=y$, and the relation $y=m(y')$ on $Y\times Im(f)$. We can then just relationally compose these to get the relation $\exists y:Y.f(x)=y\land y=m(y')$ or just $f(x)=m(y')$ defined on $X\times Im(f)$. We use the fact $m$ is a mono (i.e. $m(y)=m(y')\vdash y=y'$) to show that this relation is functional, and $y':Im(f)$ means $\exists x:X.f(x)=m(y')$ to show that it is total. From the result I mentioned before, this means there's an arrow $e:X\to Im(f)$ and we can easily show the relational composition of the graph of $e$ and the graph of $m$ (corresponding to their composition as morphisms) produces the graph of $f$. Minimality of the image is then $\exists x:X.f(x)=y\vdash P(y)$ where $P$ is some subobject of $Y$ such that $\vdash P(f(x))$ which obviously holds. $\square$

My point with the above is 1) to show how the internal logic/language can simplify things once its established and, in particular, allow us to use more familiar forms of reasoning, 2) to illustrate one of the perspectives that motivate certain categorical definitions that can otherwise seem unmotivated, and 3) many of these things have geometrical motivations as well which leads to an unexpected connection between logic and geometry casting new light on both.