ETCS and existence of complements of sets

81 Views Asked by At

In An Elementary Theory of the Category of Sets Lawvere argues in Theorem 5 that

Given any subset $A\stackrel{a}{\rightarrow}X$ there is a subset $A'\stackrel{a'}{\rightarrow}X$ such that $X\cong A+A'$ and $a$ and $a'$ are the two injections: thus $x\in a'$ iff $x\in X$ and $x\notin a$, and $a$ has a characteristic function $X\rightarrow 2$.

Basically he builds the family of sets not intersecting $a$ in the following way: he considers the arrow $$A\times1\rightarrow 1\stackrel{i_0}{\rightarrow}2$$

Where $i_0:1\rightarrow2$ is chosen to represent "false" and $i_1:1\rightarrow2$ represents "true". Then by exponential adjuction he gets an arrow $j_0:1\rightarrow 2^A$, that is an element $j_0\in 2^A$, and defines $\mu:\mathcal{A}\rightarrow2^X$ as the equalizer of the arrows $2^a:2^X\rightarrow 2^A$ and $2^X\rightarrow1\stackrel{j_0}{\rightarrow}2^A$; we can see this arrow $\mu$ as representing the family of subsets of $X$ which do not intersect $A$. He then builds the union of this family (which can be done by Theorem 4) and shows that indeed $A+A'\cong X$.

We know that each one of these subsets given by is "special", meaning it has a characteristic function. But how can we derive that $A$ also has a characteristic function?

EDIT: I guess it is sufficient to consider the arrows $$A\rightarrow1\stackrel{i_1}{\rightarrow}2$$ and $$A'\rightarrow1\stackrel{i_0}{\rightarrow}2$$ One gets a unique arrow $$A+A'\cong X\stackrel{\phi}{\rightarrow}2$$ And $\forall x\in X$, then $x\in A \Rightarrow \phi(x)=i_1$ and $x\notin A\Leftrightarrow x\in A' \Rightarrow \phi(x)=i_0$. But then $$\forall x\in X,\ x\in A\iff \phi(x)=i_1$$ which is exactly the definition of a characteristic function for $A$.