Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: topos theory

Topic: Forcing

Jem (Apr 25 2020 at 18:05):

I've tried to get an understanding of forcing and of Grothendieck topoi, and know they're linked but not how.

I think that for a poset $(P, \leq)$, the result of forcing over $P$ is the topos of ¬¬ sheaves in the classifying topos of the following theory:

• We have a type $\mathcal P$, for each $p:P$ a constant $p:\mathcal P$, a relation $\leq_{\mathcal P} \subseteq \mathcal P \times \mathcal P$, for each dense $D \subseteq P$ a predicate $D \subseteq \mathcal P$, and a predicate $G \subseteq \mathcal P$
• For each $p,q:P$, axioms asserting $p \leq q$ iff $p \leq_{\mathcal P} q$, and for each $p:P$ and each dense $D \subseteq P$, axioms asserting $p \in D$ iff $D(p)$
• $G$ is a filter
• $\leq_{\mathcal P}$ is a partial order
• $\vdash_{x:\mathcal P} \bigvee_{p:P} x=p$
• For each dense $D \subseteq P$, the axiom $\vdash \exists x:\mathcal P. G(x) \land D(x)$
  (because I think this would mean that geometric morphisms out of this classifying topos into $\mathcal E$ correspond to generic subsets of $P$ in $\mathcal E$, and taking double negation ensures that the topos is boolean)

This is mostly based on intuition though, and I'm not confident that this is how it works.

Is this how forcing works in the language of topos theory, or is it something else?

John Baez (Apr 25 2020 at 22:17):

I don't know enough about this. I assume you've read the nLab article? It's pretty sketchy but it's helpful in providing intuition, and it refers to Scedrov's short book Forcing and Classifying Topoi, and quotes Johnstone saying;

Until recently, logicians could have been forgiven for treating topos theory as a closed book, whose applications to logic (however interesting they might appear from the outside) were accessible only to insiders well schooled in the mysteries of category theory [...][...] [[ Ščedrov’s book makes ]] a very clear case for the advantages of the topos-theoretic approach to forcing namely, that it provides a clear conceptual view of what generic structures really are, as well as a workable mean [...][...] Although categorical ideas and terminology are inevitably present, they are handled so skilfully that the categoriphobic reader need have few qualms about them [...][...] Ščedrov’s work ought to go a long way towards demolishing the wall of incomprehension that has hitherto prevented many logicians from appreciating what topos theory has to offer their subject.

Mike Shulman (Apr 25 2020 at 23:22):

It's simpler than that: it's the topos of $\neg\neg$-sheaves of the presheaf topos on $P$. This is discussed at the nLab page on double-negation.

sarahzrf (Apr 25 2020 at 23:59):

does that classify anything?

Morgan Rogers (he/him) (Apr 26 2020 at 10:28):

The answer to this question is always yes (and technically lots of things, but we can at least reconstruct one).
The topos of presheaves on $P$ classifies flat functors with domain $P$. Since flat functors preserve any finite limits that exist, this means that all of the morphisms in $P$ must get sent to monomorphisms and any meets get sent to products. Since the inverse image functor of any geometric morphism $\mathcal{E} \to [P^{\mathrm{op}},\mathrm{Set}]$ must preserve the terminal object, we conclude that this topos classifies P-indexed collections of sub-terminal objects.

The subtopos of $\neg\neg$-sheaves classifies a quotient of this theory (those $P$-indexed diagrams of subterminals satisfying some extra constraints), and I'm sure with a little more work we could work out a nice expression for that.

John Baez (Apr 26 2020 at 15:53):

Morgan Rogers said:

Since flat functors preserve any finite limits that exist, this means that all of the morphisms in $P$ must get sent to monomorphisms and any meets get sent to products.

I'm being a bit slow apparently: "sent" by what?

John Baez (Apr 26 2020 at 15:56):

I'd like to understand in detail what the category of presheaves on P is the classifying topos for. I asked about it on the n-Category Cafe, and learned a lot from the answers, but I still don't get what you're saying.

Dan Doel (Apr 26 2020 at 17:02):

Flat functors from a preorder $P$ do that, I think.

sarahzrf (Apr 26 2020 at 18:49):

ah https://ncatlab.org/nlab/show/Diaconescu%27s+theorem#statement

sarahzrf (Apr 26 2020 at 18:50):

so a mapping $P \to \mathcal E$ that's always subterminal is sort of like an "$\mathcal E$-valued subset of $P$", right?

sarahzrf (Apr 26 2020 at 18:52):

and i'm pretty sure i remember that flat functors categorify filters...

sarahzrf (Apr 26 2020 at 18:52):

so that's like saying an "$\mathcal E$-valued filter on P", maybe? 🤯

Jens Hemelaer (Apr 26 2020 at 19:46):

sarahzrf said:

so that's like saying an "$\mathcal E$-valued filter on P", maybe? 🤯

Yes, I agree. The definition of flat functor makes this formal.
In practice it is difficult to give a concrete description of what the flat functors are. It becomes easier when the poset P has meets, because then by Corollary 2.4 of https://ncatlab.org/nlab/show/flat+functor a functor $F : P \to \mathcal{E}$ is flat if and only if it preserves finite limits.
So for example: if $P$ has two elements 0 and 1, with 0 < 1, then the topos of presheaves over $P$ classifies subterminal objects, i.e. flat functors $P \to \mathcal{E}$ are the same as subobjects of the terminal object in $\mathcal{E}$. By the way, the topos of presheaves in this case is equivalent to the topos of sheaves on the Sierpinski space.
If $P$ has four elements 0,1,a,b with 0 < a < 1 and 0 < b < 1, then taking a flat functors $P \to \mathcal{E}$ is the same as taking a pair of subobjects of the terminal object of $\mathcal{E}$.
For more difficult posets, the characterization in terms of flat functors is probably the best you can do.
(At least if you want to study flat functors $F : P \to \mathcal{E}$ for $\mathcal{E}$ arbitrary.)

Mike Shulman (Apr 26 2020 at 22:44):

There's a monograph by Scedrov called Forcing and classifying topoi. I'm pretty sure that the topos of double-negation sheaves on a poset classifies the theory of Generic filters on that poset.

sarahzrf (Apr 26 2020 at 23:33):

isn't that basically what the original post was suggesting? :)

Mike Shulman (Apr 27 2020 at 03:44):

Oh, I see now that that's what the OP was getting at. It could be that that description is actually correct. But it really is simpler than that: it's a propositional geometric theory, so you can present it with no sorts at all and one atomic proposition $G_p$ for each $p\in P$ (representing the statement "$p\in G$").

Jens Hemelaer (Apr 27 2020 at 09:12):

Mike Shulman said:

There's a monograph by Scedrov called Forcing and classifying topoi. I'm pretty sure that the topos of double-negation sheaves on a poset classifies the theory of Generic filters on that poset.

Do you know how to make this kind of statement precise (or a reference)? Something like a procedure of turning the axioms for the Set-theoretic models (in this case the generic filters) into the right axioms for the geometric theory.

It seems that multiple sets of axioms can give the same set-theoretic models but different geometric theories, and that you have to do a lot of computations to check that you picked the right set of axioms.

sarahzrf (Apr 27 2020 at 14:20):

so given a grothendieck topos, you can "embed P into it as a constant object" right? by applying the left adjoint of global sections to ${\le} \subseteq P^2$ in Set

sarahzrf (Apr 27 2020 at 14:22):

then is an internal-language statement like "a filter on constant-object P" what is classified by PSh(P)? you definitely get a subobject of constant-object P

sarahzrf (Apr 27 2020 at 14:22):

is that the meaning of "internally flat"?

Mike Shulman (Apr 27 2020 at 23:06):

@Jens Hemelaer Since, as you say, different geometric theories can have the same category of models in a classical Set (the most blatant example being a theory that has no models in a classical Set but has models in nonclassical toposes), there can't really be a general procedure in that direction. But in this particular case, I think you can really just write down the explicit theory of flat cover-preserving functors on P (which is propositional, since P is a poset) and observe that its models in Set are generic filters on P.

Jens Hemelaer (Apr 28 2020 at 07:31):

@Mike Shulman Thanks for giving your take on this, it takes away my confusion.