[HN Gopher] Computing an integer using a Grothendieck topos
___________________________________________________________________
Computing an integer using a Grothendieck topos
Author : georgecmu
Score : 67 points
Date : 2021-05-19 12:19 UTC (10 hours ago)
(HTM) web link (math.andrej.com)
(TXT) w3m dump (math.andrej.com)
| an1sotropy wrote:
| So what was the integer? 42?
| jqgatsby wrote:
| "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.
| jimhefferon wrote:
| 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 wrote:
| 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#Ellipt...
| appears to agree
| roywiggins wrote:
| I believe elliptic geometry is a subset, it's spherical
| geometry that isn't (though it's closely related).
| red_trumpet wrote:
| 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
| ivanbakel wrote:
| 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.
| bigbillheck wrote:
| 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-...
|
| Also of note by the same author:
| https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...
| ufo wrote:
| In the context of programming languages, constructive
| mathematics maps well to type systems.
|
| There are type systems that correspond to non constructive
| logics, but those are the weirder ones.
| zozbot234 wrote:
| https://en.wikipedia.org/wiki/Synthetic_differential_geometr...
| is worth mentioning. It builds on topos theory which as OP says
| is closely linked to non-classical mathematics.
| Y_Y wrote:
| 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 wrote:
| > 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.
| KineticLensman wrote:
| > 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".
| anon_tor_12345 wrote:
| I wish people would stop being so entitled. This isn't the
| nytimes or something. It's somebody's research blog. Your
| comment is analogous to demanding that Japanese speakers write
| in English so that you may be able to read their writing. If
| you don't want to invest the time then simply move on.
| Twisol wrote:
| 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!
| Twisol wrote:
| 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.
| bidirectional wrote:
| 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 wrote:
| This piece probably has a very specific intended audience.
| omaranto wrote:
| Yes, mathematicians.
| throwaway81523 wrote:
| "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.
___________________________________________________________________
(page generated 2021-05-19 23:01 UTC)