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 '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 '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 '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 '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 '19 at 17:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.