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.
Racky Dichminky (Sep 29 2022 at 00:34):To tell the truth, I don't really understand what all the presheaf stuff tells us about the geometric side of things? Can we actually go from meaningful statements about logics to meaningful statements about topological/geometric structures through topoi?
Like can we go from Lindstrom's theorem to something meaningful about topologies maybe?
so i haven't really gone far enough into topos theory to have a satisfactory answer to this question but
first of all like the reason topos theory was invented is that the category of sheaves over a space contains a lot of information about it, not just from a theoretical point of view that you can practically reconstruct it but from the practical point of view that sheaf cohomology, which is a crucial algebraic invariant which tells you a lot of stuff, already requires you in some sense to pass through the topos. so the fact that this category has a rich internal logic should be helpful somehow.
Second, it is sometimes less important that topos logic is an intuitionistic logic than that it is a modal logic. It is a kind of modal logic with respect to the Kripke frame of open subsets of the topological space, and it is naturally equipped with a certain modal operator , "locally", i.e. it is locally the case that P
I think that historical arguments in geometry about a "generic point" in a variety can likely be interpreted as a kind of forcing argument in the sheaf of functions over the stalk
but this is a very broad statement with a lot of details missing and I don't have a lot of examples
https://rawgit.com/iblech/internal-methods/master/notes.pdf
Ingo Blechschmidt's PhD thesis is the main work i know of in applications of logic to geometry through topos theory
so anyone have an to answer this question?
Zhen Lin Low (Sep 29 2022 at 06:30):I have never seen any convincing examples. But there are some easy correspondences. For example, if the internal logic is boolean then the underlying locale is extremally disconnected.
Racky Dichminky (Sep 29 2022 at 06:58):Zhen Lin Low said:
I have never seen any convincing examples. But there are some easy correspondences. For example, if the internal logic is boolean then the underlying locale is extremally disconnected.
I have another question aside until someone maybe provides a convincing example (if it does exist) for the first initial question.
does topos theory address definability and such?
this is something i don't know if i want to get into, honestly i can't say much but like, you can construct various functions on the natural numbers and people have probably worked out what the class of definable functions N -> N is
all of them would be Turing computable but not all Turing computable functions would be definable this way
if you throw away the subobject classifier then you would essentially have Godel's system T
this is not really definability in the model theoretic sense tho
Morgan Rogers (he/him) (Sep 29 2022 at 07:29):Racky Dichminky said:
To tell the truth, I don't really understand what all the presheaf stuff tells us about the geometric side of things?
Is there context I'm missing here?
Racky Dichminky (Sep 29 2022 at 07:45):Morgan Rogers (he/him) said:
Racky Dichminky said:
To tell the truth, I don't really understand what all the presheaf stuff tells us about the geometric side of things?
Is there context I'm missing here?
it occurs to me that the first non-trival topos you probably see is sSet although I've never heard anything about it's internal logic
https://mathoverflow.net/questions/159989/internal-logic-of-the-topos-of-simplicial-sets
presheaf category is a topos but precisely not a grothendeick topoi ( maybe sheaf cat i thinkor like. any groth topoi is a sheaf category somehow are )
if u define a functor by mapping open sets U to the category of sheaves on U then u can show that this functor is pretty much a sheaf
so u map an open set U to the sheaf cat on U
U mapsto Sh(U)
and then arrows in O(X)op are inclusion U>V whcih get mapped to the restriction map of sheaf F|U -> F|U
then like roughly you have a bunch of sheaves defined on the elements of an open cover such that they agree on overlaps then there is a unique sheaf that collates them (like in the regular sheaf definition)! so its almost a sheaf
I think this is what stacks are for
A stack is a sheaf of categories rather than a sheaf of sets. So there's a stack of sheaves over a topological space
Similarly there's a stack of vector bundles over a manifold or something like this because you can glue together two vector bundles over two open subsets U and V by giving an isomorphism between the restrictions to U \cap V
and as long as these isomorphisms satisfy the Cech cocycle condition you get a vector bundle over the whole space
Racky Dichminky (Sep 29 2022 at 07:47):also a presheaf over a topological space X is a structure F which assigns to each open set U \subset X a set F(U), thought of as a set of functions on U, and which assigns to each inclusion V \subset U a restriction-of-domain function F(U) -> F(V).
A sheaf is a presheaf satisfying the "gluing" axiom. If U is an open set and {U_i} is a cover of U, and { f_i } are a family of elements of the F(U_i) that agree pairwise in the sense that f_i = f_j on the intersection U_i \cap U_j, there should be exactly one function f defined on U which "amalgamates" all the f_i so that f | U_i = f_i.
It is fairly straightforward how to extend the definition of a presheaf on a topological space to a presheaf on a category, once you think of the lattice of opens of a topological space as a poset category. A presheaf on a category C is then just a contravariant functor C^op -> Sets.
However it is not so obvious how to define sheaves, because it is not clear how to adapt the gluing axiom to an arbitrary category.
A grothendieck topology on a category C is extra structure which allows you to formulate the gluing condition for a presheaf on C. A grothendieck says, for each object c in C, what the "covers" of c are in terms of the other objects in C and their maps into c.
A site is a category equipped with a Grothendieck topology.
Morgan Rogers (he/him) (Sep 29 2022 at 08:10):Racky Dichminky said:
Can we actually go from meaningful statements about logics to meaningful statements about topological/geometric structures through topoi?
Yes. First of all, there are examples like @Zhen Lin Low gave, where general features of the internal logic of a topos of sheaves on a space correspond to properties of that space. The other one that is well-studied is the weaker property of the internal logic being "de Morgan" (no relation). Contrary to what Zhen Lin said, it's actually this property that corresponds to extremal disconnectedness. The topos of sheaves on a space is Boolean if and only if the space is discrete. Further properties of the internal logic constrain subobject lattices, and for toposes of sheaves on spaces, it's typically necessary and sufficient to consider the impact on the lattice of subterminals.
Second, there is another face of logic in topos theory, which is only tangentially related to the internal language: the theory of classifying topos. This face of logic is used to construct instances of locales (spaces) with no points; I can try and convince you of the importance of these if you like.
Like can we go from Lindstrom's theorem to something meaningful about topologies maybe?
Since Lindström's theorem concerns properties of models of theories in first-order logic, it would more properly be interpreted via classifying toposes, although you would need to talk about functors which preserve the structure needed to interpret first-order logic (which is distinct from the structure interpreting geometric logic), and so you're already outside the realm of what's been extensively examined in topos theory there.
Morgan Rogers (he/him) (Sep 29 2022 at 08:14):Racky Dichminky said:
it occurs to me that the first non-trival topos you probably see is sSet although I've never heard anything about it's internal logic
https://mathoverflow.net/questions/159989/internal-logic-of-the-topos-of-simplicial-sets
I hadn't seen that question before, that's a nice source of fresh examples for me! I hope it at least indicates what kinds of axioms can hold in the internal language which extend intuitionistic logic?
presheaf category is a topos but precisely not a grothendeick topoi ( maybe sheaf cat i thinkor like. any groth topoi is a sheaf category somehow are )
This is a misunderstanding. Presheaf toposes are a special case of sheaf toposes (where the Grothendieck topology involved is the "trivial" one). Note that "sheaves" can be defined over sites more general than those defined from spaces, which may be where the confusion comes from.
Morgan Rogers (he/him) (Sep 29 2022 at 08:15):Racky Dichminky said:
It is fairly straightforward how to extend the definition of a presheaf on a topological space to a presheaf on a category, once you think of the lattice of opens of a topological space as a poset category. A presheaf on a category C is then just a contravariant functor C^op -> Sets.
However it is not so obvious how to define sheaves, because it is not clear how to adapt the gluing axiom to an arbitrary category.
A grothendieck topology on a category C is extra structure which allows you to formulate the gluing condition for a presheaf on C. A grothendieck says, for each object c in C, what the "covers" of c are in terms of the other objects in C and their maps into c.
A site is a category equipped with a Grothendieck topology.
I'm glad you're working all of this out, but I don't think you need to write it all out here :sweat_smile:
Racky Dichminky (Sep 29 2022 at 09:07):about what @Zhen Lin Low said, How many schemes of interest to algebraic geometers are you aware of which are extremally disconnected as topological spaces? How many of the historical arguments in algebraic geometry about a generic point in a varierty are about varieties which are extremally disconnected. Every open set is dense, right! For every predicate P defining an open subset, either \lnot P is equivalent to the tautology or \lnot\lnot P is. This is not true of any Boolean algebra with more than two elements.
Morgan Rogers (he/him) (Sep 29 2022 at 10:13):See Example 2.30 of my paper with @Jens Hemelaer: a space with a dense point is automatically extremally disconnected, so affine schemes are extremally disconnected, but they are only ever discrete in trivial cases.
Naso (Sep 29 2022 at 13:10):Morgan Rogers (he/him) said:
Racky Dichminky said:
it occurs to me that the first non-trival topos you probably see is sSet although I've never heard anything about it's internal logic
https://mathoverflow.net/questions/159989/internal-logic-of-the-topos-of-simplicial-setsI hadn't seen that question before, that's a nice source of fresh examples for me! I hope it at least indicates what kinds of axioms can hold in the internal language which extend intuitionistic logic?
A nice discussion about internal logic in the topos of graphs https://mathoverflow.net/questions/124991/what-can-be-expressed-in-and-proved-with-the-internal-logic-of-a-topos
Jonas Frey (Sep 29 2022 at 21:03):Morgan Rogers (he/him) said:
See Example 2.30 of my paper with Jens Hemelaer: a space with a dense point is automatically extremally disconnected, so affine schemes are extremally disconnected
Haha, that's really counterintuitive :-)
Morgan Rogers (he/him) (Sep 29 2022 at 21:18):It's a bad name for sure :upside_down:
Zhen Lin Low (Sep 29 2022 at 23:14):Did you mean _irreducible_ rather than affine?
Jonas Frey (Sep 30 2022 at 00:12):Ahh right, it has to be irreducible. That's equivalent to having a dense point pretty much by definition.
Morgan Rogers (he/him) (Sep 30 2022 at 05:56):Probably, thanks. I was specifically thinking of Spec(R), affine schemes are indeed far too generic