6 ms·

Computing an integer using a Grothendieck topos

75 points by georgecmu 5y ago

jqgatsby 5y ago
"I particularly like the analogy with Euclidean geometry. If we remove the parallel postulate, we get absolute geometry, also known as neutral geometry. If after we remove the parallel postulate, we add a suitable axiom, we get hyperbolic geometry, but if we instead add a different suitable axiom we get elliptic geometry. Every theorem of neutral geometry is a theorem of these three geometries, and more geometries. So a neutral proof is more general." I thought elliptic geometry was not a subset of absolute geometry.
- ivanbakel 5y ago
  I tried to find a proof online one way or the other, but there seems to be no concrete consensus. It's possible that whether or not elliptic geometry is a subset of absolute geometry is a consequence of the formulation of the axioms - since you can modify any axiom involving the existence of parallel lines using something like "If parallel lines exist, then...". Certainly the way I learned it was that the parallel postulate is the only axiom which distinguishes the elliptic, Euclidean, and hyperbolic geometries.
- roywiggins 5y ago
  I believe elliptic geometry is a subset, it's spherical geometry that isn't (though it's closely related).
  - red_trumpet 5y ago
    Reading the Wikipedia entry about Hilbert's axioms [1], I think spherical geometry is not absolute, because two opposing points lie on many lines connecting the two (think north and south pole, connected by all the meridians). [1] https://en.wikipedia.org/wiki/Hilbert%27s_axioms https://en.wikipedia.org/wiki/Hilbert%27s_axioms
- jimhefferon 5y ago
  Euclidean has more axioms than absolute (one more). With more axioms you can prove more things (one of them being the axiom itself). So also, elliptic has more axioms than absolute.
- jesboat 5y ago
  Elliptic geometry is not a subset of absolute geometry (as absolute geometry is typically formalized). The problem isn't with Euclid's other postulates, it's with things that Euclid didn't formalize, specifically, betweenness. In absolute geometry, given any line containing three distinct points, exactly one of the points will be between the other two. There's no sensible way to define this in elliptic geometry. Intuitively, this makes sense; when you have three points on a line in elliptic geometry, you can travel from any of the three points to any other without passing by the third point. It's been a while since I've actively studied this, but my recollection is that all you have to do is replace the axioms for betweenness with axioms for separation, and you get a theory which is suitable for elliptic geometry. (Separation is an arity-4 relationship on points. Intuitively, given any four distinct and collinear points, A and C separate B and D if the order of the points on the line (traveling in either direction) is ABCD.) https://en.wikipedia.org/wiki/Foundations_of_geometry#Elliptic_geometry https://en.wikipedia.org/wiki/Foundations_of_geometry#Ellipt... appears to agree
KineticLensman 5y ago
> Johnstone's topological topos is very easy to describe: take the monoid of continuous endomaps of the one-point compactification of the discrete natural numbers, considered as a category, then take sheaves for the canonical coverage. I really wish technical authors wouldn't say "very easy" when they mean "readers will need a substantial intellectual investment such as a Ph.D".
- Twisol 5y ago
  That's pretty egregious, yeah. To be as fair as possible, the author did say "describe", not "understand", but that's small consolation. Perhaps more materially, HN is obviously(^) not the intended audience for this article! We get a hint of this early on, when the author talks about axioms that contradict LEM -- the phrase "of course" stands out pretty starkly. (^) Oh no, I did it too!
- bidirectional 5y ago
  It is very easy to describe, in the same way that some complicated computations can be neatly packaged into a one liner. Understanding it is a totally different thing.
- 6gvONxR4sf7o 5y ago
  This piece probably has a very specific intended audience.
  - omaranto 5y ago
    Yes, mathematicians.
- Twisol 5y ago
  Let's see how much I can extract from that description... (Okay, after having written this comment, I can say it's "not much", but at least I think I can identify which parts are more glue and reshaping than contain real content. I won't be upset if you hit that [-] to minimize this comment ;) ) > the monoid of continuous endomaps An "endomap" is a functions `T -> T` over the same base type `T`. You might call these "unary operators". The "continuous" adjective means that `T` is some kind of topological space -- which agrees, thank goodness, with the "topological" we see earlier in the quotation -- and that our functions preserve the extra properties possessed by these spaces. For the most part, that means that points have some sense of connectivity and continuity (though not necessarily "distance"). The "monoid" bit here doesn't actually add much; it's just highlighting some behavior that unary operators already have. Namely, you can compose two unary operators in sequence, and there's an operator that returns the output unchanged. There's some extra color around making sure the composition is continuous, but we can take the author on faith for now that things work out. > the one-point compactification of the discrete natural numbers This is the concrete `T` above. The "natural numbers" are hopefully clear; we can probably assume the author is including zero, but I don't think it actually matters. I think we just need a set of countably-infinite cardinality. Since we're talking about continuous maps, we need to consider the natural numbers as some kind of space, with some kind of concept of continuity. The "discrete" qualifier tells us that every natural number is its own island. (This is why I don't think it matters whether we have zero or not.) Any set of elements can be given the discrete topology, so it's not very interesting in its own right. Usually we're interested in what other mathematical widgets do at these boundary cases: since they're effectively contentless, we can better understand what those other widgets contribute purely on their own. The "one-point compactification" of a topological space is a lot harder to dissect. In a very small nutshell: some subspaces of a topological space can be "compact". If the whole space itself is not compact, there's often a way to turn it into a compact space by adding a single extra point. Compact spaces have some really nice properties, so if you have a space that isn't compact, sometimes it makes sense to move into a compactification of that space instead. But I don't understand this particular construction yet, so I can't explain concretely what space we end up with. Unfortunately, that also means I have no intuition for what maps `T -> T` we end up with on this compact space. That seems like a pretty key bit of information for the rest of the construction. > take the monoid of ... considered as a category, then take sheaves for the canonical coverage For the "considered as a category" part, every monoid is a category in a boring way. It's even more boring when your monoid is already made of maps `T -> T`: the one object of your category is `T`, and the arrows are the maps. This is purely a "perspective-shifting" statement, and the only reason you'd do that is to say something else that's easier to say in category theoretic terms. As for "take sheaves for the canonical coverage", I'm not even going to try to dissect that. It looks like a coverage is one way to define a topos, and Grothendieck toposes are defined by sheaves on a site, but we're rapidly falling down a rabbit hole here. Summary: they're building a topos in an apparently standard way from the monoid of endomaps we've built up to this point.
an1sotropy 5y ago
So what was the integer? 42?
bigbillheck 5y ago
As a mathematician, I have yet to encounter a reason as to why I should care about 'constructive mathematics' or 'neutral mathematics'. Bauer brings up non-Euclidean geometry but the thing there is about 40-ish years into it Beltrami and then Klein started showing why hyperbolic geometry is interesting and important (per Milnor[0]). Constructive mathematics is older than that by now ('Foundations of Constructive Analysis' came out in 1967, and the field was old even then), where are its applications to other fields of math? By 'application' I'm meaning stuff like, for example, how certain isometries of the plane (PSL2(R)) are connected to the Poincare disk. I'm even less impressed by 'neutral mathematics'. OK, you proved a well-known result without using excluded middle or choice, that's cool, I beat Doom with only the pistol. Tell me why that's not just stunts and gimmickry. [0]: https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society-new-series/volume-6/issue-1/Hyperbolic-geometry-The-first-150-years/bams/1183548588.full https://projecteuclid.org/journals/bulletin-of-the-american-... Also of note by the same author: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...
- Y_Y 5y ago
  You don't have do it because it might be useful somewhere else. There's definitely richness to the topic, and it attracts curiosity and answers questions at least some people thought were worth answering. It would be an anomaly if it never found some profound link with stone mainstream more applied field. All the same, when it does prove "useful" that will just be incidental. It won't be a pay-off or vindication or anything. (At least this is my half-baked mathematical philosophy, reasonably people may certainly differ.)
  - n4r9 5y ago
    > You don't have do it because it might be useful somewhere else. Agreed, and I think this is something mathematicians generally can relate to.
  - bigbillheck 5y ago
    > It would be an anomaly if it never found some profound link with stone mainstream more applied field. I'm not asking for a 'mainstream more applied field', I'm asking for some other flavor of math, no matter how abstract.
throwaway81523 5y ago
"Johnstone's topological topos is very easy to describe: take the monoid of continuous endomaps of the one-point compactification of the discrete natural numbers, considered as a category, then take sheaves for the canonical coverage." Wow cool, I never realized it was so simple! Thanks for this clear explanation! j/k.
- omaranto 5y ago
  Well it is simple for a description of a topos. If you know the definition of topos, you are likely to also know what the canonical coverage is and what sheaves are, etc.
kd0amg 5y ago
> The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean. Meanwhile, ACL2 has the excluded middle and can still prohibit defining non-computable things. It needs termination analysis in order to do so, but these type theories rely on that too. Is the forgoing the excluded middle really gaining you the guarantee of computability?
- fmihaila 5y ago
  > Is the forgoing the excluded middle really gaining you the guarantee of computability? It doesn't follow; that uncomputable things cannot be expressed in a constructive system doesn't mean that everything that is computable in principle is also computable, or even definable, in that system (unless by "guaranteeing computability" you meant something else).

75 points by georgecmu 5y ago

"I particularly like the analogy with Euclidean geometry. If we remove the parallel postulate, we get absolute geometry, also known as neutral geometry. If after we remove the parallel postulate, we add a suitable axiom, we get hyperbolic geometry, but if we instead add a different suitable axiom we get elliptic geometry. Every theorem of neutral geometry is a theorem of these three geometries, and more geometries. So a neutral proof is more general." I thought elliptic geometry was not a subset of absolute geometry.

ivanbakel 5y ago
I tried to find a proof online one way or the other, but there seems to be no concrete consensus. It's possible that whether or not elliptic geometry is a subset of absolute geometry is a consequence of the formulation of the axioms - since you can modify any axiom involving the existence of parallel lines using something like "If parallel lines exist, then...". Certainly the way I learned it was that the parallel postulate is the only axiom which distinguishes the elliptic, Euclidean, and hyperbolic geometries.
roywiggins 5y ago
I believe elliptic geometry is a subset, it's spherical geometry that isn't (though it's closely related).
- red_trumpet 5y ago
  Reading the Wikipedia entry about Hilbert's axioms [1], I think spherical geometry is not absolute, because two opposing points lie on many lines connecting the two (think north and south pole, connected by all the meridians). [1] https://en.wikipedia.org/wiki/Hilbert%27s_axioms https://en.wikipedia.org/wiki/Hilbert%27s_axioms
jimhefferon 5y ago
Euclidean has more axioms than absolute (one more). With more axioms you can prove more things (one of them being the axiom itself). So also, elliptic has more axioms than absolute.
jesboat 5y ago
Elliptic geometry is not a subset of absolute geometry (as absolute geometry is typically formalized). The problem isn't with Euclid's other postulates, it's with things that Euclid didn't formalize, specifically, betweenness. In absolute geometry, given any line containing three distinct points, exactly one of the points will be between the other two. There's no sensible way to define this in elliptic geometry. Intuitively, this makes sense; when you have three points on a line in elliptic geometry, you can travel from any of the three points to any other without passing by the third point. It's been a while since I've actively studied this, but my recollection is that all you have to do is replace the axioms for betweenness with axioms for separation, and you get a theory which is suitable for elliptic geometry. (Separation is an arity-4 relationship on points. Intuitively, given any four distinct and collinear points, A and C separate B and D if the order of the points on the line (traveling in either direction) is ABCD.) https://en.wikipedia.org/wiki/Foundations_of_geometry#Elliptic_geometry https://en.wikipedia.org/wiki/Foundations_of_geometry#Ellipt... appears to agree

KineticLensman 5y ago

> Johnstone's topological topos is very easy to describe: take the monoid of continuous endomaps of the one-point compactification of the discrete natural numbers, considered as a category, then take sheaves for the canonical coverage. I really wish technical authors wouldn't say "very easy" when they mean "readers will need a substantial intellectual investment such as a Ph.D".

Twisol 5y ago
That's pretty egregious, yeah. To be as fair as possible, the author did say "describe", not "understand", but that's small consolation. Perhaps more materially, HN is obviously(^) not the intended audience for this article! We get a hint of this early on, when the author talks about axioms that contradict LEM -- the phrase "of course" stands out pretty starkly. (^) Oh no, I did it too!
bidirectional 5y ago
It is very easy to describe, in the same way that some complicated computations can be neatly packaged into a one liner. Understanding it is a totally different thing.
6gvONxR4sf7o 5y ago
This piece probably has a very specific intended audience.
- omaranto 5y ago
  Yes, mathematicians.
Twisol 5y ago
Let's see how much I can extract from that description... (Okay, after having written this comment, I can say it's "not much", but at least I think I can identify which parts are more glue and reshaping than contain real content. I won't be upset if you hit that [-] to minimize this comment ;) ) > the monoid of continuous endomaps An "endomap" is a functions `T -> T` over the same base type `T`. You might call these "unary operators". The "continuous" adjective means that `T` is some kind of topological space -- which agrees, thank goodness, with the "topological" we see earlier in the quotation -- and that our functions preserve the extra properties possessed by these spaces. For the most part, that means that points have some sense of connectivity and continuity (though not necessarily "distance"). The "monoid" bit here doesn't actually add much; it's just highlighting some behavior that unary operators already have. Namely, you can compose two unary operators in sequence, and there's an operator that returns the output unchanged. There's some extra color around making sure the composition is continuous, but we can take the author on faith for now that things work out. > the one-point compactification of the discrete natural numbers This is the concrete `T` above. The "natural numbers" are hopefully clear; we can probably assume the author is including zero, but I don't think it actually matters. I think we just need a set of countably-infinite cardinality. Since we're talking about continuous maps, we need to consider the natural numbers as some kind of space, with some kind of concept of continuity. The "discrete" qualifier tells us that every natural number is its own island. (This is why I don't think it matters whether we have zero or not.) Any set of elements can be given the discrete topology, so it's not very interesting in its own right. Usually we're interested in what other mathematical widgets do at these boundary cases: since they're effectively contentless, we can better understand what those other widgets contribute purely on their own. The "one-point compactification" of a topological space is a lot harder to dissect. In a very small nutshell: some subspaces of a topological space can be "compact". If the whole space itself is not compact, there's often a way to turn it into a compact space by adding a single extra point. Compact spaces have some really nice properties, so if you have a space that isn't compact, sometimes it makes sense to move into a compactification of that space instead. But I don't understand this particular construction yet, so I can't explain concretely what space we end up with. Unfortunately, that also means I have no intuition for what maps `T -> T` we end up with on this compact space. That seems like a pretty key bit of information for the rest of the construction. > take the monoid of ... considered as a category, then take sheaves for the canonical coverage For the "considered as a category" part, every monoid is a category in a boring way. It's even more boring when your monoid is already made of maps `T -> T`: the one object of your category is `T`, and the arrows are the maps. This is purely a "perspective-shifting" statement, and the only reason you'd do that is to say something else that's easier to say in category theoretic terms. As for "take sheaves for the canonical coverage", I'm not even going to try to dissect that. It looks like a coverage is one way to define a topos, and Grothendieck toposes are defined by sheaves on a site, but we're rapidly falling down a rabbit hole here. Summary: they're building a topos in an apparently standard way from the monoid of endomaps we've built up to this point.

an1sotropy 5y ago

So what was the integer? 42?

bigbillheck 5y ago

As a mathematician, I have yet to encounter a reason as to why I should care about 'constructive mathematics' or 'neutral mathematics'. Bauer brings up non-Euclidean geometry but the thing there is about 40-ish years into it Beltrami and then Klein started showing why hyperbolic geometry is interesting and important (per Milnor[0]). Constructive mathematics is older than that by now ('Foundations of Constructive Analysis' came out in 1967, and the field was old even then), where are its applications to other fields of math? By 'application' I'm meaning stuff like, for example, how certain isometries of the plane (PSL2(R)) are connected to the Poincare disk. I'm even less impressed by 'neutral mathematics'. OK, you proved a well-known result without using excluded middle or choice, that's cool, I beat Doom with only the pistol. Tell me why that's not just stunts and gimmickry. [0]: https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society-new-series/volume-6/issue-1/Hyperbolic-geometry-The-first-150-years/bams/1183548588.full https://projecteuclid.org/journals/bulletin-of-the-american-... Also of note by the same author: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...

Y_Y 5y ago
You don't have do it because it might be useful somewhere else. There's definitely richness to the topic, and it attracts curiosity and answers questions at least some people thought were worth answering. It would be an anomaly if it never found some profound link with stone mainstream more applied field. All the same, when it does prove "useful" that will just be incidental. It won't be a pay-off or vindication or anything. (At least this is my half-baked mathematical philosophy, reasonably people may certainly differ.)
- n4r9 5y ago
  > You don't have do it because it might be useful somewhere else. Agreed, and I think this is something mathematicians generally can relate to.
- bigbillheck 5y ago
  > It would be an anomaly if it never found some profound link with stone mainstream more applied field. I'm not asking for a 'mainstream more applied field', I'm asking for some other flavor of math, no matter how abstract.

throwaway81523 5y ago

"Johnstone's topological topos is very easy to describe: take the monoid of continuous endomaps of the one-point compactification of the discrete natural numbers, considered as a category, then take sheaves for the canonical coverage." Wow cool, I never realized it was so simple! Thanks for this clear explanation! j/k.

omaranto 5y ago
Well it is simple for a description of a topos. If you know the definition of topos, you are likely to also know what the canonical coverage is and what sheaves are, etc.

kd0amg 5y ago

> The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean. Meanwhile, ACL2 has the excluded middle and can still prohibit defining non-computable things. It needs termination analysis in order to do so, but these type theories rely on that too. Is the forgoing the excluded middle really gaining you the guarantee of computability?

fmihaila 5y ago
> Is the forgoing the excluded middle really gaining you the guarantee of computability? It doesn't follow; that uncomputable things cannot be expressed in a constructive system doesn't mean that everything that is computable in principle is also computable, or even definable, in that system (unless by "guaranteeing computability" you meant something else).