If models of set theory can be construed as categories, can notions of forcing be construed as functors?

Question

Consider the following passage from Blass and Scedrov's paper "Complete topoi representing models of set theory"(Annals of Pure and Applied Logic, vol. 57 (1992),PP. 1-26) where 'set theory' in this case means ZFA and a model of set theory means a Boolean-valued model of ZFA which contains a copy of the ordinary universe of two-valued, pure sets as a transitive subclass--ZFA means Zermelo-Frankel set theory allowing atoms, this paraphrased from Blass and Scedrov's abstract:

"Any model M of set theory gives rise to a category, also called M, as follows. Objects are the sets of M, those x$\in$ M which are definitely not atoms, i.e. for which ||x$\in$A||=0. Morphisms from x to y are those f$\in$M for which ||f is a function from x to y||=1. The composite of f and g is the unique h such that ||h=f$\circ$g||=1, where $\circ$ refers to the usual definition of composition of functions in set theory. Note that the patching property [see pg 2 of the paper for their definition of this--my comment] of M is needed to ensure the existence of h as well as the existence of identity morphisms. It is straightforward to check (using patching repeatedly) that the category M is a topos. For example, the power object of x is the unique y such that ||y is the set of all subsets of x||=1. In particular, the truth value object of this topos is $\hat2'$ [I will use $\hat a'$ for any a that needs a check-mark over it--my comment], whose global sections (elements x$\in$M with ||x=$\hat0'$ or x=$\hat1'$||=1) are identified with the elements of $\mathscr B$ (x being identified with ||x=$\hat1'$||). M has a natural numbers object, namely $\hat{\omega^{'}}$. Our smallness requirements on M ensure, as indicated above, that each object x has only a set of points 1$\rightarrow$x; applying this with x=$a^{b}$, we find that there are only a set of morphisms b$\rightarrow$a, so that the category M has small hom-sets."

That ordinary models of ZF (and ZFC), that is, Scott-Solovay models $V^{\mathscr B}$(A) of ZFA where $\mathscr B$ is the two-valued Boolean algebra and A=$\emptyset$ is shown by the following, from G.P. Monro's paper "A Category-Theoretic Approach To Boolean-Valued Models Of Set Theory" (Journal of Pure and Applied Algebra, vol 42 (1986) pp.245-274):

"If we have an ordinary (2-valued) model M of set theory [set theory in this case can still be ZFA with or without Choice--my comment], there is a standard procedure for turning it into a category: the category has M as its set of objects and the set {f$\in$M: M$\vDash$"f is a function"} as its set of arrows (pg. 253)."

Considering for the moment only the categories formed from the ordinary 2-valued models of set theory, it seems reasonable to infer from the above and from the fact that functors are mappings from category to category that notions of forcing are, in fact, functors from the ground model M to the forcing extension M[G].

My questions are these: i) what properties must a functor F have to be a notion of forcing that from a ground model M of set theory, F:M$\rightarrow$M[G], and ii) how can one reconstrue the major notions of forcing in terms of functors?

Answer 1

The straightforward answer to your question is: sure, but they're not very interesting.

If we view a (2-valued) model $M\models ZF$ (I use $ZF$ for simplicity) as a category whose objects are sets in $M$ and whose morphisms are functions in $M$, as you do, then - whenever we have an end-extension $N\supseteq M$ - the inclusion map is a functor from $M$ to $N$.

An end-extension is just a model $N\supseteq M$ where, for $x\in M$, we have $\{y\in N: N\models y\in x\}=\{y\in M: M\models y\in x\}$, that is, elements of $M$ don't gain new elements in $N$. I suspect we don't need to restrict attention to end-extensions, but I don't know much about non-end-extensions, so I'm not going there. Note that every forcing extension is an end-extension: also, note that end-extensions need not get "taller" despite the name and despite what end-extensions of arithmetic do - extensions which add no new elements of old rank are called "top-extensions."

Note that even if $N$ is assumed to be a very nice extension of $M$ - say, a forcing extension - this inclusion map will not be full: e.g., adding a real is the same as adding a new morphism from $\omega$ to 2. In fact, this functor is full iff $N\supseteq M$ is a top extension, which forcing extensions never are (since forcing adds no new ordinals).

A more interesting kind of functor arising from forcing notions might be: if we have a definable forcing notion $\mathbb{P}$, we can view it as an endofunctor on any "reasonable" category of Boolean-valued models of $ZF$. (We need to use Boolean-valued models instead of classical models, since generic filters aren't unique; on classical models we might get an anafunctor http://ncatlab.org/nlab/show/anafunctor, but even that is't clear to me.) These functors might have interesting properties; I don't know very much about them.