Showing some object is initial

111 Views Asked by At

This is a problem from logic. I'll first phrase it in general categorical terms since it is rather obscure, and then with context.

Let $\mathcal{E}$ be a regular category where all epi's are regular. If $f: V \to X$ factors through $\bot \to X$ where the latter morphism is the mono part of the factorization $0 \to \bot \to X$, is then $V$ initial?

Context

I am trying to prove iv of the soundness of Kripke-Joyal semantics. By iii and the definition $\neg N = N \implies \bot$ where $\implies$ is the Heyting implication and $\bot$ is the bottom element in the subobject poset of $X$, it is enough to show that for $V \xrightarrow{g} U \xrightarrow{\alpha} X$ we have that $g$ factors through $\bot \to X$ if and only if $V$ is initial.

1

There are 1 best solutions below

2
On BEST ANSWER

The answer to the question you asked is no. For one thing, not every regular category has an initial object. But putting that issue aside, the category of groups is a regular category with an initial object in which all epis are regular. For any groups $G$ and $H$, we have the trivial homomorphism $f\colon G\to H$ which factors through the trivial group as $G\to 0 \to H$. This does not imply that $G$ is initial (trivial).

On the other hand, as Mark Kamsma suggests in the comments, this is true in any coherent category, and therefore in any elementary topos.

Recall that a coherent category is a regular category such that for every object $X$, the poset $\text{Sub}(X)$ has finite joins (including the empty join $\bot_X$) and these joins are preserved by pullbacks. Now any coherent category has a strict initial object $0$, and $0 = \bot_1$, the smallest subobject of the terminal object (see Lemma A1.4.1 in the Elephant).

Since the empty join is stable under pullback, we can pull back the arrow $0 = \bot_1 \to 1$ along the unique arrow $X\to 1$ to obtain $\bot_X\to X$. But then $\bot_X$ admits an arrow to $0$ (one side of the pullback square), and since $0$ is strict initial, $\bot_X\cong 0$.

Now for any $V\to X$ which factors through $\bot_X\to X$, $V$ admits an arrow to $0$, so also $V\cong 0$ and $V$ is initial.