Grothendieck's Approach to Equality [pdf] | Hacker News Reader

Grothendieck's Approach to Equality [pdf]

ma.ic.ac.uk

137 pointsmathgenius37 comments

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.

> 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.

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.

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.

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

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...

The slide on Homotopy type theory seems glib and misses the point: Yes, ℕ and ℤ are equal in HoTT, but only if you ignore structure. ℕ and ℤ 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.

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 ℕ and ℤ are equal, but structured as addition semirings in the conventional way they are different.

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.

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.

Any recommendation for a (short) introduction to HoTT for a working mathematician?

This comes to mind:

https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf

Thank you very much!

Awodey has a shortish introduction here: https://arxiv.org/abs/1701.02024

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.

In the book Fields Medallists' Lectures by M. Atiyah, there is a short (4 pp.) article written by Jean Dieudonné 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.

Thanks for the recommendation, I will definitely check it out.

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...

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.

Yep, though Grothendieck's perspective was more abstract. To him, affine schemes succinctly described coslice categories over a ring (with only localization maps). Adding equivalences back into the mix leads to his theory of stacks/descent. Adding more general localizations leads to his étale, fppf, fpqc results. His work has a more categorical than ring theoretic flavor.

See my comment to a sibling.

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

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?

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

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.

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.

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?

That's a valid and good question.

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.

> 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.

You can handwave equality, but you need to specify which equality. same with "isomorphism". same form or equal form? how is the equality specified there? canonical has a precise definition, but the paper doesn't come close.

eg array-equal as in lisp, vs eqc vs equal vs eq. list of atoms with the same order and same values. or list of equal atoms. (ie same pointers). or if the values are same, or all the other atom properties need to be the same.

without a precise definition of equality everything is just handwaving.

in perl "" equals 0 equals !!0. so are they equal, and if so which equality? same with JavaScript, python and PHP with completely handwave equality definitions. in the end it all comes to Greenspun, all the lisp equalities.

Grothendiek is lucky to ignore pointers. for him all natural numbers can be equal. 1 === 1. for us eg with python higher numbers with the same value are sometimes not eq. This would have driven Grothendiek even more nuts.

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

What is the definition of 'canonical' then?

I've often found the label 'canonical' to be rather arbitrary.

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.

'Canonical' means constructible from the definition (the axioms) of the structure alone. A canonical isomorphism is not necessarily unique.

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.

Deligne was his student: https://youtu.be/WfDcrN5_1wA

Reply on news.ycombinator.com