For what it’s worth, subobject classifiers and power objects are not necessary to describe sets categorically. Most of the familiar properties of sets are already represented by a well-pointed pretopos; adding power objects then corresponds to assuming the powerset axiom in ZFC.

]]>Actually, the way that the internal logic of a topos gets built up by the interplay between the external (natural operations on subobject lattices) and internal (operations on $\Omega$) is already an excellent illustration of the Yoneda lemma in action. But that’s just one of a billion examples.

]]>There are various levels at which one can understand the Yoneda lemma. The proof is somewhat trivial. But one gradually appreciates its importance, eventually overwhelmingly so, when one encounters it every day of one’s life, at varying levels both conceptual and calculational. It truly is THE central result of category theory.

Surely the Yoneda lemma article can be much improved. I’m a little dumbstruck myself because it’s so deep in my blood and bones and soul that it’s very hard ever to feel I can do it proper justice. Perhaps I should jot down a note every time I use it, and accumulate these notes over time, and eventually cull the best ones and put them down as examples in the article. Not sure I’ll ever do that, though.

]]>The subobject classifier is the analog of truth values – the defining property of $\Omega$ is the correspondence between two ways of describing a property on elements of a set:

- As the subset of elements having the property
- As the predicate (i.e. truth-valued function) specifying whether an element has that property

I actually find the “finite limits” + “cartesian closed” + “truth values” description to be a very appealing characterization of toposes, since that basically says outright “a topos is a place where you can do basic logic and function manipulation in the familiar way”.

Any category, really, has a notion of set membership coming from the idea of generalized elements. However, for the purposes of describing toposes you could also work from the idea of “power object”, since (bound) set membership can be described as a property on $PX \times X$ for each $X$.

]]>It is a bit surprising that the direct approach to describing sets using category theory leads to subobject classifiers. It is not an obvious choice as an analog of set membership.

One thing I've noticed when teaching category theory is people ask about what the word "set" means in this context. I don't have an answer for them.

Of course we both "understand" Yoneda's lemma. My short write-up was an attempt to make it more approachable to newcomers by pretending I don't. ]]>

The best it can do to describe Set Theory is topos.

Well, this is not at all true (see Algebraic Set Theory for example), but mainly what I’d be worried about in this discussion is “attitude”, as in the use of phrases like “state of sin” and “the best it can do”. There are many people who frequent the nLab who understand (pace von Neumann) and who *could* explain the Yoneda lemma, but there may not be many who want to engage if it looks like it’s going to be an uphill climb. We’re kind of busy.

I never really got the issue with the size of homsets. Category theory is kind of in a state of sin for even bringing that up. The best it can do to describe Set Theory is topos. ]]>

As a generalization, to arbitrary categories, of this simple, readily understandable, special case:

Think of

( (a group G) acting on (a set X) ).

Then

(elements of the set X)

correspond bijectively to

( (orbits of the group G acting on X), which are precisely

( the G-natural transformations

from (the regular representation of G)

to (the G-set X) ) ).

Each (element x in X) generates

( (an orbit g -> xg), which might be called (the "extension" of x), and denoted (x hat) ;

thus (x hat) : G -> X : g -> g(x hat) = xg ).

Note that this amounts to transposing the action

from X_: G->[X,X] to tensor: X×G->X to hat : X->[G,X],

where we have chosen names of each of the arrows.

(This special case of the Yoneda lemma amounts to

(showing hat is injective and identifying its image) ).

That

( the orbits (x hat) ) are

( G-natural transformations from (the regular representation of G) to X )

is precisely equivalent to

( the action being associative) :

(forall x)(forall h)(forall g) (xg)h = x(gh)

iff (g(x hat))h = (gh)(x hat)

iff g(x hat)(X_h) = g(G_h)(x hat)

iff (x hat)(X_h) = (G_h)(x hat)

iff (x hat) is G-natural.

(Here we have denoted ( the (right) action of (h in G) ) (on X by X_h : X -> X)

and (on G itself by G_h : G -> G). )

Conversely,

given a ( natural transformation alpha from (the regular representation of G) to X ),

( evaluate alpha at (the unit element of the group) ), getting

( (an element of X), which might be called (the "restriction" of alpha) and denoted (alpha check) ).

These two operations are mutually inverse.

That

( (extension followed by restriction) is (the identity on X) )

is precisely equivalent to

(the identity axiom for the action).

That

( (restriction followed by extension) is the identity )

is precisely equivalent to

(associativity of the action), i.e. that

(orbits are natural).

So we have (alpha = alpha check hat), which shows that (alpha is an orbit).

So we have the claimed Yoneda bijection in this case.

Everything else is generalizations (mainly, going from a category with only one object, such as a group or monoid, to multi-object categories),

and spelling out details (mainly, "what is a natural transformation?").

Also, one must take care to avoid size issues on the hom "sets".

From this POV, (natural transformations out of representable functors) are (generalized orbits). ]]>

I scribbled some thoughts on the Yoneda lemma here. Feedback welcome.

]]>