While trying to understand set theory from categorical perspective i.e. elementary theory of category of sets (Thanks to Lawvere), I am confronted with the situation where I need to construct arbitrary functions between two sets. Up until now following axioms are considered:
- $\exists $ terminal object $1$.
- $\exists$ initial object $0$.
- $\nexists 1\rightarrow 0$
- 1 is a separator.
- Binary sum object exists for any two sets $A, B$.
One of the properties that we expect of sum object is that of exhaustivity. In general, following definition of exhaustivity of sum can be given.
Definition Let $C$ be a category, $S$ be sum of objects $A$ and $B$ with inclusion maps $i_A:A\rightarrow S$ and $i_B:B\rightarrow S$. Sum is said to be exhaustive iff $\forall$ objects $T\in C, \forall t_1, t_2:S\rightarrow T$
$$[(t_1\circ i_A=t_2\circ i_A) \wedge (t_1\circ i_B=t_2\circ i_B)]\Rightarrow (t_1=t_2)$$
That sum is exhaustive (1) in general follows from only the definition of sum. Please let me know, if you need to see proof of this.
But in category of sets, we expect more of exhaustivity:
$$\forall s:1\rightarrow S, s\subseteq i_A \vee s\subseteq i_B \ \ \ \ (2)$$
Where $\subseteq$ is defined as follows: Let $s_1:S_1\hookrightarrow A$ and $s_2:S_2\hookrightarrow A$. $s_1\subseteq s_2 \equiv \exists w:S_1\rightarrow S_2$ such that $s_2\circ w=s_1$.
An observation: (2) seems to be connected to (1). As if (2) is false, then that using the notion of arbitrary mappings, one can construct two mappings from sum object to an object with at least 2 points such that these mapping differ at only one point of sum object and that point is the one that is not included in any of the inclusion maps. Now, inclusion maps, in contradiction to (1), cannot differentiate these mappings. But, existence of such mappings/functions seems to be not guaranteed by the 5 axioms stated in the beginning. But this could be introduced as follows:
Definition of a function: A definition of a function (Lets call it $f$) comprises of following:
- A definition of its domain: $dom(f)$.
- A definition of its codomain: $cod(f)$.
- $\forall e:1\rightarrow dom(f)$, a defintion of $f\circ e$.
Function $f$ is said to be a 'defined function'.
Now one can state an axiom which stipulates existence of all defined function.
Axiom of existence of defined functions Let $f:A\rightarrow B$ be a defined function. $f$ exists iff $\forall a:1\rightarrow$, $\exists! b:1\rightarrow B$ such that $f\circ a = b$.
Now my question is basically this, is there any other way of ensuring existence of arbitrary mappings in this category of sets?
Please note, I am beginner of the beginners learning what I like. So, I ask another more general question pertaining to studying:
The axiom of existence of defined function seems to be an obvious one (and also an elegant one). But, I am also aware of Lawvere and Rosebrugh's book 'Sets for Mathematics', where they use intuition of arbitrary mappings as a guide rather than as an axiom. Why is that?
While trying to learn something, is it better to start with what is obvious, and hope that upon their study and observation, we will be lead to other further non-obvious, perhaps, equivalent or more general axioms, which can replace the previous ones? I agree that this is certainly more an opinion based question, but in any case, I certainly see it as helpful to others like me who are confused when learning things. However, if you do not want to share any opinion, I understand. No worries.
Thank you in advance for your attention and valuable time that you gave it to my small modest question.