====== Forcing is Sheafification ? ======

One day, my old labmate delivered an interesting quote from a professor that "//forcing is just a sheafification//". Many people in category theory tend to simplify mathematical concepts into technical constructions in category theory, but I often doubt whether such analogies really capture the underlying meanings; e.g., it is difficult to say "//inductive definitions are just initial algebras//'' to a student who wants to learn mathematical induction in their first mathematical logic class. However, I had to admit that the quote was catchy enough to make me investigate more about how forcing is a sheafification.

In this note, I will overview a proof in topos theory regarding the continuum hypothesis. The proof involves sheafification and corresponds to Cohen's proof using forcing techniques. Hence, I think this should be what the professor meant (though I have not asked). The purpose of this note is to introduce the brief shape of the overall proof and to show how sheafification is used.
This note is simply an excerpt and rephrasing of "Sheaves in Geometry and Logic" by Saunders Mac Lane and Ieke Moerdijk where all the missing details can be found. (Of course, the book contains more than just details.)

===== Overview =====

We will construct a topos, so-called Cohen topos, which is Boolean admitting the Axiom of Choice but at the same time invalidates the continuum hypothesis; i.e., in the topos, there is an object $X$ with strict cardinal inequality 
$$
\mathbf{N} < X < \mathcal{P}\mathbf{N}
$$
where $\mathbf{N}$ is the natural number object (nno) and $\mathcal{P}\mathbf{N}$ is the power object of the nno in the topos.

===== Cohen Poset =====

The proof starts with constructing a Cohen poset. Pick any very large set $B$ that strictly exceeds the cardinality of $\mathcal{P}\mathbf{N}$. For example, let $B = \mathcal{P}(\mathcal{P}\mathbf{N})$.
The idea is that we construct a mono $g : B \rightarrowtail \mathcal{P}\mathbf{N}$ and claim $\mathbf{N} < gB < \mathcal{P}\mathbf{N}$. In $\mathbf{Set}$, $\mathbf{N} = \mathbb{N}$, $\mathcal{P}\mathbf{N} = \{0,1\}^\mathbb{N}$ and such $g$ of course does not exist. However, believing as if it did exist, we can still define $\textit{finite approximations}$ of its transpose $f : B \times \mathbb{N} \to \{0,1\}$. Cohen poset $\mathbf{P}$ is on the set of finite mappings from $B \times \mathbb{N}$ to $\{0,1\}$ such that
$$
q\leq p :\!\!\iff \mathrm{dom}(p) \subseteq \mathrm{dom}(q) \text{ and }
q\restriction_{\mathrm{dom}(p)} = p.
$$
In words, $q$ is less than $p$ if as finite approximations, $q$ extends $p$.


===== Cohen topos =====

The Cohen topos $\mathbf{Sh}(\mathbf{P},\neg\neg)$ is the category of sheaves with the dense topology on the Cohen poset $\mathbf{P}$: a subset $S$ below $p$ is a cover if for any $q \leq p$, there is $r \leq q$ such that $r \in S$. Equivalently, 
it is the full subcategory of $\neg\neg$-sheaves of the presheaf topos $\mathbf{Set}^{\mathbf{P}^{op}}$. By taking the $\neg\neg$-topology, the Axiom of Choice holds in the Cohen topos.

Although it was not possible in $\mathbf{Set}$ to build the desired mono, in the presheaf topos $\mathbf{Set}^{\mathbf{P}^{op}}$ we can mimic something similar. Define a presheaf $A$ by 
$$
A(p) = \{(b, n) \mid p(b, n) = 0\}
$$
as a sub-functor of $\Delta (B \times \mathbb{N})$ the constant presheaf in $\mathbf{Set}^{\mathbf{P}^{op}}$. Then, we can even verify that the presheaf as a subobject is $\neg\neg$-closed: for the characteristic morphism $\chi : \Delta (B \times \mathbb{N}) \to \Omega$ of $A$ in the presheaf topos.
The pullback of the truth $\mathbf{1} \rightarrowtail \Omega$, where $\Omega$ is the truth object in $\mathbf{Set}^{\mathbf{P}^{op}}$, along $\neg\neg\circ \chi$ is again $A$.

The truth object $\Omega_{\neg\neg}$ of the Cohen topos $\mathbf{Sh}(\mathbf{P},\neg\neg)$, as it is the topos of $\neg\neg$-sheaves in the presheaf topos, is the equalizer $e : \Omega_{\neg\neg} \to \Omega$ of the identity morphism $\mathrm{id}_\Omega : \Omega\to\Omega$ and $\neg\neg : \Omega \to\Omega$. Since $A$ is $\neg\neg$-closed, $\neg\neg\circ\chi = \chi$. Hence, there is a unique morhpism 
$$
f : \Delta B \times \Delta \mathbb{N} \to \Omega_{\neg\neg}
$$
such that $e\circ f = \chi$.
We take $\Delta B \times \Delta \mathbb{N} \cong  \Delta (B \times \mathbb{N})$ implicitly.
Taking its transpose, we obtain 
$$
g: \Delta B   \to \Omega_{\neg\neg}^{\Delta\mathbb{N}}
$$
which we can further prove that it is a mono in $\mathbf{Set}^{\mathbf{P}^{op}}$. Here, to prove the mono, the definition of the Cohen poset is used importantly. In other words, the Cohen poset is defined precisely for this reason to make $g$ mono.


===== Sheafification =====

Sheafification is a functor 
$$
\mathbf{a} : \mathbf{Set}^{\mathbf{P}^{op}} \to \mathbf{Sh}(\mathbf{P},\neg\neg)
$$
that is a left adjoint to the trivial inclusion functor. It is left exact, preserving monos. Hence, sheafifying $g$, we get a mono 
$$
\mathbf{a}g : \mathbf{a}\Delta B   \rightarrowtail \mathbf{a}\Omega_{\neg\neg}^{\Delta\mathbb{N}}.
$$
Applying some fancy techniques, including the Yoneda lemma, we obtain an isomorphism $\mathbf{a}\Omega_{\neg\neg}^{\Delta\mathbb{N}} \cong \Omega_{\neg\neg}^{\mathbf{a}\Delta\mathbb{N}}$ and constitute a mono:
$$
m : \mathbf{a}\Delta B   \rightarrowtail \Omega_{\neg\neg}^{\mathbf{a}\Delta\mathbb{N}}
$$
in $\mathbf{Sh}(\mathbf{P},\neg\neg)$.

The sheafified $\mathbf{a}\Delta\mathbb{N}$ is a natural number object in $\mathbf{Sh}(\mathbf{P},\neg\neg)$. Hence, $\Omega_{\neg\neg}^{\mathbf{a}\Delta\mathbb{N}}$ indeed denotes the power object of natural numbers in $\mathbf{Sh}(\mathbf{P},\neg\neg)$. 
The huge set $B$ is $\textit{forced}$ to be inside the power object $\Omega_{\neg\neg}^{\mathbf{a}\Delta\mathbf{N}}$. This is because the new power object in $\mathbf{Sh}(\mathbf{P},\neg\neg)$ is much larger than what is computed in $\mathbf{Set}$.

Let us write $\widehat{X}$ for $\mathbf{a}\Delta X$. Since we have 
$$
\mathbb{N} \rightarrowtail \{0,1\}^\mathbb{N} \rightarrowtail B
$$
that are strict in $\mathbf{Set}$, after a long argument to prove that the sheafification preserves strict cardinal inequalities, which we omit here, together with $m$ above, we have strict monos
$$
\widehat{\mathbb{N}} \rightarrowtail \widehat{\{0,1\}^\mathbb{N}} 
\rightarrowtail \Omega_{\neg\neg}^{\widehat{\mathbb{N}}}
$$
in the Cohen topos. Here, for the preservation of the strict cardinal inequality, having $\neg\neg$-sheafification is important which makes the Cohen topos Boolean and have the Souslin property. To summarize, in the Cohen topos, the sheafified power object is the evidence that violates the continuum hypothesis while being Boolean accepting the Axiom of Choice.

{{tag>[incomplete]}}