The definition of monomorphism in Aluffi's book is:
A function $f: A \to B$ is a monomorphism if for all sets $Z$ and all functions $\alpha' \alpha'' : Z \to A$, $f \circ \alpha' = f \circ \alpha'' \implies \alpha' = \alpha''$.
The result I'm trying to follow the proof of is: $f$ is injective if and only if it is a monomorphism.
He proved earlier that if $A \neq \emptyset$, $f: A \to B$ is injective if and only if it has a left inverse. We need the assumption that $A$ is nonempty because for any $B \neq \emptyset$, $f: \emptyset \to B$ is vacuously injective, but there are no functions $B \to \emptyset$ and hence no left inverses.
In this proof, Aluffi makes no such assumptions about $A$ being nonempty, but immediately invokes the result that if $f$ is injective, it has a left inverse, which is true only if $A$ is nonempty. Whether I need the assumption boils down to how I should read this definition.
The first interpretation is: the result needn't be true for ALL sets $Z$, but only all sets $Z$ for which there is a function $\alpha: Z \to A$. If $A = \emptyset$, $f: A \to B$ is vacuously injective for any $B$, but the only function $\alpha: Z \to A$ I can define is the empty function where $Z = \emptyset$. So, vacuously, $\alpha' = \alpha''$: both are the empty function.
The other interpretation is that this has to be true for any set $Z$, including nonempty sets $Z$, so the fact that I can't define a function $f: Z \to \emptyset$ is a problem and requires that $A \neq \emptyset$ be built into the assumptions of the problem.
Which interpretation is correct?
Best Answer
The definition of monomorphism is for any set, including the empty set. But if there is no function $Z \rightarrow A$, then the condition
$$\forall\alpha,\alpha’:Z\rightarrow A:f\alpha = f\alpha‘\implies \alpha=\alpha‘$$
is trivially satisfied, hence $Z$ does not matter when determining monomorphicity. This is to say both interpretations are equivalent. In fact this explains, why the unique morphism $\emptyset\rightarrow X$ for some set $X$ is a monomorphism (which needn’t be true in an arbitrary category), since there are no morphisms from an inhabited set into $\emptyset$…