Forcing over a partial order $P$ can be viewed in a category theoretic sense as constructing the presheaf topos ${\bf Set}^{P^{op}}$ over the partial order (viewed as a category) then passing through the double negation transformation to recover a Boolean topos instead of an intuitionistic one, as explained by Sridhar Ramesh in the comments here.

It is not entirely clear to me whether this process is (pseudo-)functorial, i.e. if there is a (pseudo-) functor $\mathsf{Force}:{\bf Pos}\to\mathfrak{Top}$ which takes a poset to the double negation of its presheaf topos. In particular I believe all we would need is for $\neg\neg$ to be functorial. This leads me to two questions:

  1. Is $\neg\neg$ functorial?
  2. If the answer to 1 is yes, does $\mathsf{Force}:{\bf Pos}\to\mathfrak{Top}$ have a left or right adjoint?

Below is a suggestion of how $\mathsf{Force}$ might be constructed, apologies if any glaring errors are made. The Yoneda embedding $y_P$ takes a poset $P$ to the subcategory $y_P(P)\hookrightarrow{\bf Set}^{P^{op}}$ of representable presheaves, so we can take a functor $F:P\to P'$ between poset categories to a functor $y_F:y_P(P)\to y_{P'}(P')$ between these subcategories by defining $$y_F\big({\bf Hom}_P(-,X)\big)={\bf Hom}_{P'}(-,F(X)),$$ $$y_F\big({\bf Hom}_P(-,f)\big)={\bf Hom}_{P'}(-,F(f)).$$ ${\bf Set}^{P^{op}}$ is presentable as colimits over $y_P(P)$, so I believe this functor extends to a functor (up to iso) $\overline y_F:{\bf Set}^{P^{op}}\to{\bf Set}^{P'^{op}}$ given by representing each presheaf $G\in{\bf Ob}_{{\bf Set}^{P^{op}}}$ as a colimit of some functor $G^\star:\mathcal{G}\to y_P(P)$ over representable presheaves $$G=\varinjlim_{X\in{\bf Ob}_\mathcal{G}}G^\star(X)$$ and then sending $G$ to the colimit of the image of these representable presheaves under $y_F$, $$\overline y_F(G)=\varinjlim_{X\in{\bf Ob}_\mathcal{G}}y_F(G^\star(X)),$$ and sending a natural transformation $\alpha:G\Rightarrow G'\in{\bf Hom}_{{\bf Set}^{P^{op}}}$ to the natural transformation $\overline y_F(\alpha):\overline y_F(G)\Rightarrow \overline y_F(G')$ given by $$\overline y_F (\alpha)=[\{\alpha_Z\circ\nu^X_Z\}_{Z\in{\bf Ob}_P}]_{X\in{\bf Ob}_P}:\varinjlim_{X\in{\bf Ob}_\mathcal{G}}y_F(G^\star(X))\Longrightarrow\varinjlim_{Y\in{\bf Ob}_{\mathcal{G}'}}y_F(G'^\star(Y)),$$ where $\nu^X_Z:y_F(G^\star(X))(Z)\to\varinjlim_{X\in{\bf Ob}_P}y_F(G^\star(X))(Z)$ is the coprojection for $y_F(G^\star(X))(Z)$.

I believe we thusly have a functor $y:{\bf Pos}\to\mathfrak{Top}$ given by $$y(P)={\bf Set}^{P^{op}},$$ $$y(F:P\to P')=\overline y_F,$$ so if $\neg_\mathcal{E}\neg_\mathcal{E}:\Omega\to\Omega$ in a topos $\mathcal{E}$ extends to an endofunctor $(\neg\neg)_\mathcal{E}:\mathcal{E}\to\mathcal{E}$ we may be able to extend to an endofunctor $\neg\neg:\mathfrak{Top}\to\mathfrak{Top}$ and define $\mathsf{Force}=\neg\neg\circ y$. Does this work out?

  • 3
    $\begingroup$ Have you had a look at MacLane and Moerdijk's "Sheaves in geometry and logic"? They have a whole sectin about this. $\endgroup$ – Andrej Bauer Jan 19 at 8:45
  • 1
    $\begingroup$ Page 277, section VI.2 on the Cohen topos. You should also look up (somewhere) the fact that the construction $C \mapsto \mathbf{Set}^{C^\mathrm{op}}$ is functorial in the site $C$ (so you don't have to do that part with your bare hands). After that it's "obvious" that the construction is functorial. $\endgroup$ – Andrej Bauer Jan 19 at 9:19
  • 2
    $\begingroup$ @AndrejBauer huh, so $P \mapsto (P,\neg\neg)$ is a functor from posets to sites? Nice. I do wonder if it's more generally true for non-posetal categories. However, Alec was probably wanting something like a functor $\neg\neg\colon Topos \to Topos$. I can see how this is likely true for logical functors of toposes, but for geometric morphisms? $\endgroup$ – David Roberts Jan 19 at 10:43
  • 1
    $\begingroup$ But it is common knowledge that it is functorial, which is precisely why you shouldn't trust the rumours. $\endgroup$ – Andrej Bauer Jan 19 at 11:11
  • 2
    $\begingroup$ Well, anyway, the lack of a functorial Borel map selecting generic filters for the countable models of set theory is interesting. It shows that the quotient step you mention is inherently difficult to achieve in a uniform way. $\endgroup$ – Joel David Hamkins Jan 19 at 17:29

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.