Lambda the Ultimate

Have you tried "there is a monomorphism from A to B" as a starting point?

If you are interested in a CT version of Set Theory, try "Conceptual Mathematics" by Lawvere and Schanuel or "Sets for Mathematics" by Lawvere and Rosebrugh.

If I'm not wrong, this is the same as saying that there's a one-to-one function from A to B. What I can't get is how to ensure that f(A) = A.

Since I'm only a novice the choice of words may be lame, but it seems that I'm stuck at the "up-to-isomorphism" part.

Let A = {1, 2}, A' = {a, b}, B = {1, 2, 3}

Since we're talking in the function level, what's the difference between A and A'? We can always compose with the isomorphism {(1, a), (2, b)}

It seems to me that every property I try to use suffers from the same problem, how do I know that the monomorphism f keeps the elements within A and not in some isomorphic set?

how do I know that the monomorphism f keeps the elements within A and not in some isomorphic set?

Basically, the answer is that it doesn't matter, in CT or (with a little more subtlety) in Set Theory.

CT focuses on the mappings (morphisms) betweem objects rather than their contents. One of the insights one gets from the category Set is that the mapping behaviour of a set is determined up to iso by its cardinality.

In pure Set Theory (i.e. without distinguished ur-elements) this is equally true; whether the elements are labelled {a, b} or {1, 2} doesn't really change the structure of the set.

If you really needed to make a distinction for some reason, you could choose a distinguished set of labels and specify the mappings you want that preserve the labellings. Any set of labellings will still be iso any other with the same cardinality though.

This is actually a subtle question and, as Marc says, it doesn't really matter in practice, so don't get hung up on it. If you describe a subset in `pure CT', and then continue to use pure CT to manipulate your subsets (i.e., don't break the abstraction layer), then the question is moot anyway, since you can't distinguish isomorphic obejcts in pure CT (for a good definition of `pure CT' :).

About the closest you can get in pure CT and using a generic notion of Set Theory (and, possibly intuitionism and Choice are also relevant), is that a subset is iso to a `subobject', which is an equivalence class of monos. You can find this notion in Barr and Wells.

BTW, are your elements 1, 2, a and b ur-elements? Or are they encoded as sets? If the latter, you could force certain isos to be equality by representing 1 in the same way as a, for example. But you can't force every iso in Set to be an equality without breaking stuff like the Axiom of Foundation, I think.

Everyone else has talked about the very important issue of categorical thinking being up to isomorphism, but no one has shown you the relevant construction after you internalize that. I'll try to remedy that gap.

So, let's suppose suppose that we're in the category Set. Your question is, how do we talk about subset relationships (E is a subset of A) categorically? In the categorical style, we very rarely do things directly with objects, preferring to work with arrows between them. So the obvious thing to look for is an arrow that contains the information we want, and functions in Set are defined on the elements of a set. So, how do you you say "E is a subset of A" in terms of the elements of E and A? Well, that's the same as saying "forall x. (x in E) => (x in A)". Reading that as a function, the existence of an inclusion i: E -> A which takes each element of E to the same element in A means that E is a subset of A.

This is actually not the direction category theorists normally work from, because it makes the construction of the relevant universal property seem obscure and mysterious. So I will advise you to look up equalizers, and try to read the definition thinking of an equalizer as an inclusion function.

For those interested in a brief introduction to category theory, James Cheney has recently posted some PDF slides titled Category Theory for Dummies on his home page.

Suppose we are talking about the category Set. Then the initial object {} of any set is unique in the sense of common language. There is only one initial object in Set.

In many categories this wouldn't hold up. Like Vect, where the 0 vector is in every subspace, so is initial, but the 0 vector is unique only up to isomorphism with other vector spaces. So then only knowing that there are vector spaces with linear transformations between them, it becomes impossible to establish which 0 vector is being referred to. On the other hand, the zero vector behaves the same on vector space 0 + a = a, there is an -a such that a + -a = 0,
a dot 0 = 0 (as in the real number this time), so the idea of the structure being impossible to distinguish is there.

Is my synopsis of this idea correct?

Then my next question is what would an equalizer look like on Vect?
I believe the diagram above may be incorrect as 'u' points the wrong way. Here

E--eq-->X-----f------>
^ ^-----g------> Y
| |
| |
| m
| |
+-u-----O

Then f and g are linear transformations that have some universal property being equalized by eq. If we push through this diagram starting with O, then on one hand we are have a linear transformation from O -> X, on the other hand some other linear transformation m takes us to E, which taken before eq commutes with m. Then at the same time the whole diagram commutes so taking the transfomation f of m is the same as taking the transformation g of eq of u. This on an intuitive level seems to be related to the null space of a transformation, so the kernel of a linear transformation. Saying that f and g are injective is too strong, but perhaps they are equalized by having the same kernel or the same nullity in their kernel. Am I way off here?

my diagram looks nothing like what I typed. Wikipedia has better pictures anyway.