[HN Gopher] Grothendieck's Approach to Equality [pdf]
___________________________________________________________________
Grothendieck's Approach to Equality [pdf]
Author : mathgenius
Score : 117 points
Date : 2022-05-30 10:17 UTC (12 hours ago)
(HTM) web link (www.ma.ic.ac.uk)
(TXT) w3m dump (www.ma.ic.ac.uk)
| amboo7 wrote:
| Deligne was his student: https://youtu.be/WfDcrN5_1wA
| black_knight wrote:
| The slide on Homotopy type theory seems glib and misses the
| point: Yes, N and Z are equal in HoTT, but only if you ignore
| structure. N and Z are not equal as semi-rings for instance.
|
| I don't think the usage of "canonical" can be made any more
| precise than in Homotopy type theory.
| black_knight wrote:
| I saw some other comments mentioning the need for context, and
| I think the notion of structure captures this. The context for
| an equality is the kind of structures we are considering at the
| moment. As types N and Z are equal, but structured as addition
| semirings in the conventional way they are different.
| Koshkin wrote:
| Well, the "modern" way to speak about _structure_ is in
| category theory terms, specifically in terms of morphisms and
| universal properties; similarly, the fuzzy idea of a
| _context_ , in the article, is replaced with a restriction on
| the set of assertions you allow as making sense to begin
| with.
| black_knight wrote:
| One of the cool features of HoTT is that you can look at
| types and compute what "isomorphism" should mean even
| before you put a category structure on it. For instance for
| groups, you can see what as isomorphism of groups is just
| by looking at the type of groups as the type of tuples with
| carrier, operation, neutral element and laws.
|
| Some times you can even chose two different category
| structures for the same types, as long as the two agree on
| what the isomorphism are. This happens with graphs for
| instance, where there are several coherent notions of maps
| of graphs.
| k0k0r0 wrote:
| Any recommendation for a (short) introduction to HoTT for
| a working mathematician?
| Koshkin wrote:
| This comes to mind:
|
| https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pd
| f
| k0k0r0 wrote:
| Thank you very much!
| mjreacher wrote:
| I'm always surprised to see higher level mathematics on the front
| page here considering I doubt the majority of the people upvoting
| this would understand much of it, nevertheless given the state of
| how the average person views mathematics I guess more
| popularization can't be a bad thing regardless.
|
| On the topic of document, quite a few times I've seen
| mathematicians say work on theorem provers and the sort are a
| waste of time and there's nothing to be learnt and blah blah blah
| and I think this is an excellent example of why this isn't the
| case. Kevin found a deficiency in his knowledge in algebraic
| geometry and upon spending some time on it related it to some
| wider topics in the foundations of mathematics (the notion of
| equality between set theory and homotopy type theory, for example
| see https://mathoverflow.net/questions/263024/does-equality-
| betw...). I would think there are many other things that we will
| discover that have been otherwise assumed or taken for granted
| when more mathematics is formalized by theorem provers and other
| tools.
| guerrilla wrote:
| > I doubt the majority of the people upvoting this would
| understand much of it
|
| It only has 62 upvotes and there are already 16 competent
| comments here.
| mjreacher wrote:
| Based on my own experience running forums that aggregate
| content I have tended to find that a specific group of people
| vote on content based on what they like and think looks
| interesting rather than having a situation where people only
| vote on topics they are competent in.
| layer8 wrote:
| Supporting your point: I sometimes upvote submissions
| because I want to see more discussion on them, for my own
| educational benefit.
|
| Really, a rational upvoter will upvote for the purpose of
| giving the submission higher visibility, to either promote
| awareness of the topic or of the existing discussion, or to
| engender more discussion. Neither reason necessarily
| correlates with agreement or understanding of the topic.
| Koshkin wrote:
| But the set of all functions that do not vanish on _D(f)_ is not
| limited to _R[1 /f]_. So, _P(D(f))_ is not a statement about
| _D(f)_ alone. What am I missing?
| k0k0r0 wrote:
| That's a valid and good question.
| pierrebai wrote:
| That's not the point. The point was it was true for R[1/g] but
| not for D(g), so you cannot substitute, so you cannot claim
| that f and g are equal.
|
| As someone totally outside of the maths field, it seems to me
| that the definition of equality needs a context. You can't say
| that two things are equal without specifying the larger context
| in which you are claiming the equality.
| dkarl wrote:
| > it seems to me that the definition of equality needs a
| context
|
| That's precisely it. Mathematicians are often casual with
| terminology even when being completely precise inside their
| context. I did not get beyond introductory graduate-level
| mathematics, but I distinctly remember a professor announcing
| this in the third or fourth lecture of an algebra class:
|
| "From today until the end of the semester, when I say 'ring'
| I will mean a commutative ring, except on occasion when it
| will be obvious that the ring is not commutative."
|
| Some professors/authors were more fastidious about using
| unambiguous terminology, but many preferred to slap the
| easiest word possible on whatever relationship felt the most
| important in the context. So one professor would say "what
| we're really interested in is the quotients modulo 10," and
| another would say "12 is equal to 2" and expect you to
| understand the same thing from it.
| k0k0r0 wrote:
| TL;DR
|
| To objects/sets are equal if and only if there is a canonical
| isomorphism/bijection between them. What that is is not
| necessarily clear, but there is an exception regarding abelian
| groups accotiated to a field, where the canonical isomorphism is
| clear up to a minus sign by the main theorem of global class
| theory[0].
|
| [0] https://en.m.wikipedia.org/wiki/Class_field_theory
| ur-whale wrote:
| What is the definition of 'canonical' then?
|
| I've often found the label 'canonical' to be rather arbitrary.
| Koshkin wrote:
| 'Canonical' means constructible from the definition (the
| axioms) of the structure alone. A canonical isomorphism is
| not necessarily unique.
| k0k0r0 wrote:
| That's maybe true in some fields of mathematics. In others
| that's misleading, and the usual understanding of canonical
| as unprecisely defined "obvious choice" is definitely more
| helpful.
| k0k0r0 wrote:
| Exactly that the point. It's not clear. Except for whenever
| the main theorem of global class theory applies. Then it's
| clear up to a minus sign.
| aosaigh wrote:
| For the non-mathematicians here (like myself) there was an
| article in the most recent New Yorker on Grothendieck that was
| quite interesting:
|
| https://www.newyorker.com/magazine/2022/05/16/the-mysterious...
| ironSkillet wrote:
| I have a PhD in math, but in a different area. I wish I had time
| to dive into Grothendieck's work to understand how/why it was so
| unique and revolutionary. Seems like it's still being mined for
| insights into modern problems.
| cpp_frog wrote:
| In the book _Fields Medallists ' Lectures_ by M. Atiyah, there
| is a short (4 pp.) article written by Jean Dieudonne where he
| succinctly explains the specific contributions that made
| Grothendieck so famous, after a brief background on the state
| of algebra and its problems before him.
| ironSkillet wrote:
| Thanks for the recommendation, I will definitely check it
| out.
| k0k0r0 wrote:
| See my comment to a sibling.
| mathgenius wrote:
| I'm no expert but I think one of the big ones is Grothendieck's
| identification of affine schemes with the dual (categorical
| opposite) of commutative rings. That is, a "space" is just a
| commutative ring (of functions on it), but you think about it
| backwards. So a map of "spaces" A->B, is a map of commutative
| rings A<-B. John Baez has a bunch of TWF's about this stuff
| that I highly recommend. Also [1].
|
| [1] https://qchu.wordpress.com/2009/11/24/spectra-of-rings-of-
| co...
| k0k0r0 wrote:
| Yeah, that's somewhat correct but misses the intention. Back
| than classical algebraic geometry started to get extremely
| messy and mathematicians got lost in a maze. And would prove
| wrong theorems and stuff, a lot of notions they used were not
| (possible to be) properly defined. Redefinig the geometrical
| aspect of algebraic geometry in purely algebraic terms using
| rings clearified the previously used notions and provided a
| firm basis for the mathematics that already had been studied.
| Furthermore, it provided a way out of the algebraic geometry
| mess mathematicians had been doing and lead to completely new
| insights.
|
| Before, we mathematicians considered spaces like R^n or
| rather preferably C^n and then vanishing sets of polynomials
| in them, which form nice geometrical objects. E.g. The set of
| points (x,y) in R^2 such that x^2 + y^2 = 0, which gives a
| circe. At least if we only consider real values for x and y,
| but just that you know mostly people from algebraic geometry
| prefer the complex numbers C. Then, we asked questions about
| intersections of those, about what function one might define
| on them using algebraic terms, and how many straight lines
| they contain. The geometrical aspect of this provided a great
| intuition for this kind of mathematics, but it started to get
| really messy and mathematicians started to get stuff wrong.
|
| Then, Grothendieck came along and turned everything upside
| down. He stopped talking about for example the circe, which
| is described by the algebraic equation x^2+ y^2 = 0, as the
| geometric object. Instead, he said: from now on our geometric
| object of considerations is the set of prime ideals in the
| polynomial ring in two variables that contain the polynomial
| x^2 + y^2. And together with some more structure that's what
| is today known as an affine scheme.
|
| For the sake of this explaination its not really important
| what a prime ideal is, and you might want to look that up
| later, cause its actually a very simple thing. Also any
| further definitions would rather confuse any reader, that is
| not familiar with the subject. From now one the theory gets
| surprisingly abstract. For example, polynomials and
| polynomial rings quickly get replaced by arbitrary ring. The
| main point is: Now, the circle was replaced by an object that
| was defined in purely algebraic terms. From now on, in the
| field of algebraic geometry even the geometry was purely
| algebraic.
|
| On the first glance, that algebraic object seems to have
| nothing or little to do with the geometric object of the
| circle. And definitely the theory seems to be overkill, even
| when you have a look from the insight. However, grothendieck
| was suddenly able to explain a lot of the mess other
| mathematiciam where doing up till then, and even more, he
| proved theorems in algebraic geometry that where completely
| out of reach for any mathematicians before him. With
| Grothendiek in algebraic geometry a turning-point was
| reached.
|
| At that time people were hungry for answers and hungry for
| abstraction. They absorbed his theory as thirsty plants
| absorb long awaited rain. The nice properties of rings
| allowed to develop a massive machinery of abstract
| mathematics. That's what most of algebraic geometry had
| turned into after Grothendieck.
|
| I find its a beautiful theory and a lot of it is still very
| close to geometry. For anybody interested, there is this nice
| book about the huge field of toric varieties (a subfield of
| algebraic geometry) for example. Its from Cox, Little and
| Schenk. Even though it covers basically the whole subfield it
| also assumes no or very little familiarity with algebraic
| geometry from the reader. However, one needs to get through
| that abstract basics of algebraic geometry. You wont get far
| in algebraic geometry without it. Countless mathematician
| have tried and failed miserably, before Grothendieck came
| along with his fancy theory.
| layer8 wrote:
| It seems to me that there are cases where there exist different
| "maximal" isomorphisms, even structurally different ones, hence I
| don't think that a general (always applicable) definition of
| equality as a "canonical" isomorphism is possible. You need to
| choose the equality you're interested in and tell your theorem
| prover.
| vitriol83 wrote:
| This is fairly obscure but the problem he highlights can be
| overcome easily by localising at the saturation of S_f, for
| D(f)=D(g) if and only if the saturations are equal, and
| localising at saturation is an isomorphism
| adament wrote:
| I understood the presentation to be on the distinction between
| equality and isomorphism and when an isomorphism "is an
| equality". From the slide on homotopy type theory I get the
| impression that he finds it unsatisfactory to simply consider
| all isomorphisms as equalities.
|
| But I might have misunderstood your objection?
| vitriol83 wrote:
| So many times it's necessary to 'identify' two more objects
| which are isomorphic, and the 'canonical' is supposed to
| justify why this doesn't cause a problem.
|
| The reason it is necessary here is that the mapping D(f) ->
| A_f is a priori multi valued, and we need it to be single
| valued.
|
| However it's fairly easy to make a definition which is
| trivially single valued , so I don't think it's a very
| instructive example of the phenomenon.
|
| Probably more pertinent is an n-fold tensor product with
| different bracket ordering
| edflsafoiewq wrote:
| It seems though that we would want the computer to be able to
| do this kind of reasoning itself, and not rely on humans "pre-
| resolving" all such problems.
| Animats wrote:
| I went down this road a long time ago, for a different reason.
| There are classic "axioms" for arrays, first written down by John
| McCarthy.[1][2] Those are classically considered to be axioms.
| But I set out to prove them via constructive means.
|
| I was using the Boyer-Moore theorem prover, which starts from
| something close to Peano arithmetic and builds up number theory
| from there. In Boyer-Moore theory, everything is represented as a
| LISP S-expression. Equality is defined as as the expressions
| being identical.
|
| So, in Boyer-Moore theory, you have ordered lists, but not sets.
| A set, remember, can be informally defined as a collection in
| which each item appears exactly once. The order of the items
| doesn't matter.
|
| In Boyer-Moore theory, short of forcing in a new axiom, which
| risks soundness, there's no way to say "the order of the items
| doesn't matter". At startup, there's no notion of a "set". But
| you can build one up via definitions and theorems.
|
| So I started by defining an array as an list of (subscript,
| value) tuples, ordered by subscript. Two arrays are equal if they
| are both valid and identical.
|
| So, given that definition, we can write the classic "axioms" for
| arrays as statements to be proven. First, we define
| "storea(A,I,V)" as the function that stores into an array in a
| functional sense - it creates a new array where element I has
| been replaced with V. And we define the predicate "arrayp", which
| tests whether an array is properly constructed.
|
| The key "axiom" for arrays, in Boyer-Moore notation, reads:
| (PROVE-LEMMA SELECT-OF-STORE (REWRITE) (IMPLIES (AND
| (arrayp A) (NUMBERP I) (NUMBERP J)) (EQUAL
| (selecta (storea A I V) J) (IF (EQUAL I
| J) V (selecta A J)))))
|
| That means, if A is an array, and I and J are integers, then, for
| all A, I, and J: storea(A,I,V)[J] = (if i=j then
| V else A[J])
|
| So that's McCarthy's key axiom for arrays.
|
| It's not an axiom here. It's a lemma to be proven. It turns out
| that with the right sequence of lemmas, that statement can be
| proved as a theorem. Here's that sequence.[3] I wrote that around
| 1981, and it went through the Boyer-Moore theorem prover. So we
| could then load those statements into the Oppen-Nelson simplifier
| (what today is called a SAT solver) as safely proven rewrite
| rules. This established that the array theory was both sound and
| consistent between the two provers.
|
| A few years back, I revived the original Boyer-Moore theorem
| prover, converted it to GNU Common LISP, and put it on Github.[4]
| You can download it, run it, and run the set of rules in [3]
| through it to get the proofs. (That took about 45 minutes of VAX
| time in 1981. Now it takes about a second.)
|
| The proofs are long, because there's a lot of case analysis.
| Arrays are ordered lists of tuples in this theory, and there's a
| lot of detail about maintaining that order. We had to prove
| (PROVE-LEMMA STORE-IS-PROPER (REWRITE) (EQUAL (arrayp (storea A I
| V)) T))
|
| which proves that the storing operation always produces a validly
| ordered array. That's essentially a code proof of correctness for
| a recursive function The Boyer-Moore prover was able to grind out
| a proof of that without help. That was a long proof, too.
|
| I submitted this to JACM. It was rejected, mostly for uglyness.
| The concept that you needed all this heavy machine-driven case
| analysis to prove a nice simple "axiom" upset mathematicians.
| Today it would be less of an issue. People are now more used to
| proofs that take a lot of grinding through cases.
|
| You could build up set theory this way, via ordered lists, if you
| wanted.
|
| So that's a classic of what happens if you take "equal"
| seriously.
|
| [1] http://www-formal.stanford.edu/jmc/towards.pdf
|
| [2] https://theory.stanford.edu/~arbrad/papers/arrays.pdf
|
| [3] https://github.com/John-
| Nagle/pasv/blob/master/src/work/temp...
|
| [4] https://github.com/John-Nagle/nqthm
___________________________________________________________________
(page generated 2022-05-30 23:01 UTC)