We're given the following diagram:
We assume the category has products and equalizers. Given $E, p_1, p_2$ as a pullback here, we seek to prove that $E,e$ form an equalizer of $f \circ \pi_1$ and $g \circ \pi_2$.
(The assumption that the category has products and the use of $A \times B$ as an object comes from this being the converse of a theorem if you're at all curious.)
I'm mostly wanting to check whether the following would prove that.
(Note: I'm not providing the full, formal proof. This is more a sketch proof; in this post, I'm mostly checking whether I understand what I need to prove, rather than outright proving it. I probably can prove all of these myself, I just want to make sure that these lead to the desired conclusion, if that makes any sense. I'm also a little lost at the very end of the proof as I note when appropriate.)
So what I think I need to prove and the order in which I do:
First, we assume that $E, p_1, p_2$ is a pullback in the given diagram.
Through this assumption, we prove $(f \circ \pi_1) \circ e$ = $(g \circ \pi_2) \circ e$, one of the properties of an equalizer.
We introduce a second pullback $Z, z_1, z_2$ with arrow $z : Z \rightarrow A \times B$ given by the pullback and unique, and establish the same property as before, i.e. $(f \circ \pi_1) \circ z$ = $(g \circ \pi_2) \circ z$
At this point I'm a bit lost. I'm debating over which I need to show...
- ... there exists a unique arrow $u : Z \rightarrow E$ ...
- ... or that the triangle in the diagram below commutes, i.e. $e \circ u = z$
I feel like both might be easy enough to prove with the assumption that equalizer arrows, i.e. $e$, are monomorphisms, though I also feel that is too much of an assumption given we haven't proven $E,e$ are really an equalizer at this point yet.
I guess my sticking point is invoking the universal property. Part of me is also saying I can invoke it right now - since we have $E, e$ and $Z, z$ equalizing the pair of arrows - and just establish the arrow $u$ exists and is unique and makes the triangle commute immediately.
Anyone have any ideas?