Giraud's axioms imply balanced

Question

I'm stuck on the following. Let $\mathcal{E}$ be a category satisfying the Giraud axioms: namely $\mathcal{E}$

1. is locally presentable,
2. has universal colimits,
3. has disjoint coproducts, and
4. has effective equivalence relations.

Using only this, prove that all epimorphisms in $\mathcal{E}$ are effective.

My strategy so far has gone as follows. First, I found this way to prove all epimorphisms are effective given that I can prove that $\mathcal{E}$ has epi-mono factorization systems, has stable pullbacks and is balanced.

From Moerdijk-Maclane Page 577, we can construct a epi-mono factorization of any morphism $f : X \to Y$ in $\mathcal{E}$ using the regular co-image, i.e. the coequalizer of the kernel pair $ X \times_Y X \rightrightarrows X \to \text{coim}(f)$. Universal colimits implies that epimorphisms are stable under pullback (I think). But how do I prove that $\mathcal{E}$ is balanced? I was trying to use the epi-mono factorization system, but it seems to me that it is not unique in the sense that I need.

In other words, it seems that the Moerdijk-Maclane construction is only unique in the sense of an (effective epi, mono)-factorization system. If I can factor $f$ by an effective epi followed by a mono, then I can prove its iso to the coimage, but what if it is just factored as an epi followed by a mono? Then I can't seem to prove anything.

Any help would be appreciated.

Answer 1

Here is what I think is the simplest strategy. I'm only giving a sequence of lemma which lead to the result and I think they are all easy enough, but maybe a little teddious to write down (but let me know if something is not as easy as I thought! note that extensivity is used in many places)

Lemma 1: IF $A \subset X$ is a subobject and $R \subset A \times A$ is an equivalence relation on $A$, then $R \cup \Delta_X$ is an equivalence relation on $X$.

Lemma 2: In the setting of the previous lemma $X \to X/(R \cup \Delta_X)$ is the pushout of $A \to A/R$.

Lemma 3: For any object $U \coprod U \to U$ is the quotient of $U \coprod U$ by the relation

$$U \coprod U \coprod U \coprod U \to (U \coprod U)^2 = U^2 \coprod U^2 \coprod U^2 \coprod U^2$$

Lemma 4: For any monomorphism $U \to X$,the pushout $X \coprod_U X$ is the quotient of $X \coprod X$ by an equivalence relation that can be written as

$$ X \coprod U \coprod X \coprod U \to (X \coprod X)^2 = X^2 \coprod X^2 \coprod X^2 \coprod X^2 $$

Hint: use that $X \coprod X \to X \coprod_U X $ is a pushout of $U \coprod U \to U$ and all the lemmas above.

Lemma 5: $U$ is the equalizer of the two maps $X \rightrightarrows X \coprod_U X$.

Hint: Lemma 4 and effectiveness of equivalence relations lets you compute the pullback of $X \coprod X \to X \coprod_U X$ with itself. From there you can deduce this other limit using formal manipulation of limits.

Conclusion: We have shown that an arbitrary monomorphism can be written as an equalizer. In particular it is a regular monomorphisms. This implies that the category is balanced.

Why I think (but could be wrong) there isn't a simplest proof: If I'm not mistaken, an exact category need not be balanced. For example the category of commutative rings is exact but not balanced, so the sort of argument you were doing using only quotient and pullback will not work. You really need to also use coproducts and extensivity in the proof, and I don't see another way to do this.

What is probably a simpler way to do this I assumed you wanted a direct diagramatic proof. But at this point I feel like at this point it is simpler to prove some form of Giraud's theorem and use it. Even without assuming local presentability, by (the proof of) Giraud's theorem any finite diagram in your category can be lifted to some Grothendieck topos T with a functor $T \to \mathcal{E}$ preserving colimits and finite limits. One can then just proves the theorem in a Grothendieck topos, i.e. a category of sheaves, where everything becomes a lot simpler, even doing the argument above, and you can go even quicker by showing there is a subobject classifier.