12 ms·

Grothendieck’s use of equality

178 points by golol 2y ago

fmap 2y ago
For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken... *) I'm going by second hand accounts here, please correct me if you think this statement is too strong.
- bumbledraven 2y ago
  For reference, the paper mentions the term "homotopy" exactly once, in this sentence: > The set-theoretic definition is too strong (Cauchy reals and Dedekind reals are certainly not equal as sets) and the homotopy type theoretic definition is too weak (things can be equal in more than one way, in contrast to Grothendieck’s usage of the term).
- cwzwarich 2y ago
  > For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. Arguably, Homotopy type theory still doesn't solve the problem, because while it strengthens the consequences of isomorphism it doesn't distinguish between "isomorphism" and "canonical isomorphism", whereas (some?) mathematicians informally seem to think that there's a meaningful difference. > The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken... In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory. It's far from established that this is possible at all with homotopy type theory, yet alone whether it would actually be easier or more economical to do so. And even if this state of affairs is permanent, homotopy type theory itself would still be an interesting topic of study like any other field of mathematics.
  - lupire 2y ago
    "Canonical" refers largely to the names we give to things, so that we maximize the extent to which an isomorphism maps the object named A in X to the object named A in Y. And also to choosing an isomorphism that embeds in a different isomorphism (of superstructures) that isn't strictly the topic of the current question. I don't think anyone thinks canonical isomorphisms are mathematically controversial (except some people having fun with studying scenarios where more than one isomorphism is equally canonical, and other meta studies), they are a convenient communication shorthand for avoiding boring details. https://en.m.wikipedia.org/wiki/Isomorphism_theorems https://en.m.wikipedia.org/wiki/Isomorphism_theorems
    - moomin 2y ago
      I think the original author makes a good case that a) the shorthand approach isn’t going to fly as we formalise b) different mathematicians mean different things by canonical and these details matter when trying to combining results and that therefore 3) it would be better to provide a proper definition of what you’re talking about and give it an unambiguous name.
    - euiq 2y ago
      let me guess: you haven't read the article, have you?
      - xigoi 2y ago
        > Please don't comment on whether someone read an article. "Did you even read the article? It mentions that" can be shortened to "The article mentions that". https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
  - fmap 2y ago
    > it doesn't distinguish between "isomorphism" and "canonical isomorphism" You can distinguish these concepts in (higher )category theory, where isomorphisms are morphisms in groupoids and canonical isomorphisms are contractible spaces of morphisms. These sound like complicated concepts, but in HoTT you can discover the same phenomena as paths in types (i.e., equality) and a simple definition of contractibility which looks and works almost exactly like unique existence. > In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory. The authors of Lean are brilliant and I'm extremely happy that more mathematicians are looking into formalisations and recognizing the additional challenges that this brings. At the same time, it's a little bit depressing that we had finally gotten a good answer to many (not all!) of these additional challenges only to then retreat back to familiar ground. Anyway, there were several responses to my original comment and instead of answering each individually, I'm just going to point to the article itself. The big example from section 5 is that of localisations of R-algebras. Here is how this whole discussion changes in HoTT: 1) We have a path R[1/f][1/g] = R[1/fg], therefore the original theorem is applicable in the case that the paper mentions. 2) The statements in terms of "an arbitrary localisation" and "for all particular localisations" are equivalent. 3) ...and this is essentially because in HoTT there is a way to define the localisation of an R-algebra at a multiplicative subset. This is a higher-inductive type and the problematic aspects of the definition in classical mathematics stem from the fact that this is not (automatically) a Set. A higher-inductive definition is a definition by a universal property, yet you can work with this in the same way as you would with a concrete construction and the theorems that the article mentions are provable. --- There is much more that can be said here and it's not all positive. The only point I want to make is that everybody who ever formalised anything substantial is well aware of the problem the article talks about: you need to pick the correct definitions to formalise, you can't just translate a random math textbook and expect it to work. Usually, you need to pick the correct generalisation of a statement which actually applies in all the cases where you need to use it. Type theory is actually especially difficult here, because equality in type theory lacks many of the nice properties that you would expect it to have, on top of issues around isomorphisms and equality that are left vague in many textbooks/papers/etc. HoTT really does solve this issue. It presents a host of new questions and it's almost certain that we haven't found the best presentation of these ideas yet, but even the presentation we have solves the problems that the author talks about in this article.
- voxl 2y ago
  Classical versus non-classical has nothing to do with it. HoTT does not work to capture what a mathematician means by "unique isomorphism" because witnesses of equality in HoTT are very much not unique.
- jhanschoo 2y ago
  Can you elaborate more on how you think HoTT can solve the issue Buzzard mentions that when formalizing informal mathematics, the author frequently has a model (or, a particular construction) in mind and requires properties present in the model, and then claims that this is true for all "canonically equivalent" objects without actually spending time explicating the abstract nonsense required to properly specify the properties that canonically equivalent objects preserve, for their developement? (see: a product vs. the product) Edit: and furthermore, the situation where the obvious choice of universal property (read: level of isomorphism) was a poor one, in their attempt to formalize localizations.
- YetAnotherNick 2y ago
  I think 99.9% of the people talking about HoTT haven't used HoTT in practice. They just see isomorphism is equivalent to equivalence(or something similar), comes up with a mental model and think this is the main contribution of HoTT, whereas isomorphism is a well studied thing even before formal set theory was a thing. HoTT gets weird and anyone who has tried any tool to prove anything in HoTT knows this, and this is the reason why it didn't got adopted even though many leading tools like lean worked hard to implement it.
  - deleted 2y ago
    [deleted]
  - staunton 2y ago
    Have you used it? If yes, could you elaborate? Or if you haven't, can you point to any recent source on what it's like to be using HoTT in 2024?
    - YetAnotherNick 2y ago
      [1] is the only video which I would say I found any bit accessible. But to be honest even after spending days, I couldn't grok it. And in my observation, different implementations of HoTT are quite different from each other. [1]: https://www.youtube.com/watch?v=x4cz1OgpU3M https://www.youtube.com/watch?v=x4cz1OgpU3M
- nicklecompte 2y ago
  I think HOTT helps remove a lot of the footguns and computational hairiness around using type-theoretic mathematics. But the issues Buzzard is talking about are really more profound than that. This relates to a much deeper (but familiar and nontechnical) philosophical problem: you assign a symbol to a thing, and read two sentences that refer to the same symbol ("up to isomorphism"), but not necessarily the same thing. If the sentences contradict each other, is it because they disagree on the meaning of the symbol, or do they disagree on the essence of the thing? There is a strong argument that most debates about free will and consciousness are really about what poorly-understood thing(s) we are assigning to the symbol. Worse, this makes such debates ripe for bad faith, where flaws in an argument are defended by implicitly changing the meaning of the symbol. In the context of """simple""" mathematics, preverbal toddlers and chimpanzees clearly have an innate understanding of quantity and order. It's only after children fully develop this innate understanding that there's any point in teaching them "one," "two," "three," and thereby giving them the tools for handling larger numbers. I don't think it makes sense to say that toddlers understand the Peano axioms. Rather, Peano formulated the axioms based on his own (highly sophisticated) innate understanding of number. But given he spent decades of pondering the topic, it seems like Peano's abstract conception of "number" became different from (say) Kronecker's, or other constructivists/etc. Simply slapping the word "integer" on two different concepts and pointing out that they coincide for quantities we can comprehend doesn't actually do anything by itself to address the discrepancy in concept revealed by Peano allowing unbounded integers and Kronecker's skepticism. (The best argument against constructivism is essentially sociological and pragmatic, not "mathematically rational.") Zooming out a bit, I suspect we (scientifically-informed laypeople + many scientists) badly misunderstand the link between language and human cognition. It seems more likely to me that we have extremely advanced chimpanzee brains that make all sorts of sophisticated chimpanzee deductions, including the extremely difficult question of "what is a number?", but to be shared (and critically investigated) these deductions have to be squished into language, as a woefully insufficient compromise. And I think a lot of philosophical - and metamathematical - confusion can be understood as a discrepancy between our chimpanzee brains having a largely rigorous understanding of something, but running into limits with our Broca's and Wernicke's areas, limits which may or may not be fixed by "technological development" in human language. (Don't even get me started on GPT...)
- Ericson2314 2y ago
  The fact that Buzzard is writing this paper at all to me shows a much higher degree of respect than before --- see how humble the overview is. I think this is great progress!
- zozbot234 2y ago
  > It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. It's not that simple, Buzzard actually seems to be quite familiar with HoTT. The HoTT schtick of defining equality between types as isomorphism does 'handle' these issues for you in the sense that they are treated rigorously, but there's no free lunch in that. You still need to do all the usual work establishing compatibility of values, functions etc. with the relevant isomorphisms, so other than the presentation being somewhat more straightforward there is not much of a gain in usability.
  - zozbot234 2y ago
    Sorry about not providing a reference re: Kevin Buzzard's previously-stated thoughts on HoTT, but see https://ncatlab.org/nlab/show/Kevin+Buzzard https://ncatlab.org/nlab/show/Kevin+Buzzard
juped 2y ago
Equality can be philosophically troubling, but as a practical matter, what you care about is the indiscernibility of identicals, and if every property you use follows from a universal property, then equal up to isomorphism is just equal. So every Rubik's cube is equal considered as a group of face rotations, and there's only one Rubik's cube, but if you care about chemical properties of sticker glue, they're no longer equal.
- deleted 2y ago
  [deleted]
- moomin 2y ago
  Something the author points out: sometimes theorems directly rely on specific constructions of mathematical objects, which are then used to establish things that do not mention the construction.
- passion__desire 2y ago
  The glue point reminds me of Benacerraf problem. https://en.m.wikipedia.org/wiki/Benacerraf%27s_identification_problem https://en.m.wikipedia.org/wiki/Benacerraf%27s_identificatio...
- Koshkin 2y ago
  > Equality can be philosophically troubling Which is probably why they are saying "equity" now
generationP 2y ago
This is probably better known here under the name of implicit type conversions. Strictly speaking, the rational number 1 is not the same as the integer 1; we just have a conversion map that preserves all the relevant properties. It's all fun and games until there are 1000 types and 10000 conversion maps involved and the relevant diagrams no longer commute (i.e., it depends what order you go).
- actionfromafar 2y ago
  I assume you mean any random enterprise codebase? Because that is any random enterprise codebase.
  - 082349872349872 2y ago
    In other areas, one might compare code jurisdictions, where presumably all the legislative clauses share a common vocabulary (and probably even conceptual framework), with common law jurisdictions, where all the legislative clauses occur in different centuries and thus one adds "picking a parallel transport" between the legal languages of the times (and jurisdictions) to the difficulties of adjudication.
  - om8 2y ago
    Not if you use a language that bans implicit type conversions (like go)
    - actionfromafar 2y ago
      I was thinking in much more abstract terms. You have information from a webflow, at some point converted to an XML message, converted to database entry, again to a JSON document, combined with an Azure workitem, then sent to Salesforce. At any one point the data can interact with other systems, travel through codebases each seeing the data through their types, legacy APIs, the same-(ish) new-(ish) RPC API and in each service the data is represented in its own internal quirky way. Sure, throw Go in that mix, hell at this point the more merrier! :)
- 2y ago
nyc111 2y ago
When this subject comes up I always think that the equality sign is loaded. It can mean, definition, equality, identity, and proportionality. How come this state of the equality sign is not mentioned in the paper?
- mikhailfranco 2y ago
  up to (non-)unique isomorphism
- mxmlnkn 2y ago
  As far as I remember, that's not a problem in math: := definition ≡ identity = equality ∝ proportionality
  - nyc111 2y ago
    But this is how it works: = definition = identity = equality = proportionality
    - Twisol 2y ago
      Big-O notation is a famous example where = is some flavor of (asymptotic) proportionality, and it catches a lot of people out when they first learn about it.
- yau8edq12i 2y ago
  As a mathematician, I have never, ever seen the equal sign used to denote proportionality. I cannot tell what you mean by "identity" that wouldn't be equality. And a definition in the sense you seem to mean is, indeed, also an equality. I guess this issue not mentioned in the paper because it doesn't exist.
  - ducttapecrown 2y ago
    [x:y] = [lx:ly] and I suppose the model of localization discussed in the article above counts as well.
lupire 2y ago
"When is one thing equal to some other thing?" Barry Mazur June 12, 2007 https://bpb-us-e1.wpmucdn.com/sites.harvard.edu/dist/a/189/files/2023/01/When-is-one-thing-equal-to-some-other-thing.pdf https://bpb-us-e1.wpmucdn.com/sites.harvard.edu/dist/a/189/f... https://people.math.osu.edu/cogdell.1/6112-Mazur-www.pdf https://people.math.osu.edu/cogdell.1/6112-Mazur-www.pdf
ajkjk 2y ago
I'm typing this after reading their section on page 6 about the "pentagon axiom". They write that RxR^2, R^2xR, and R^3 are isomorphic, but not literally equal under different constructions, because (a,(b,c)) is different from ((a,b), c), and that this is a problem. I feel like math kinda gets this wrong by treating sets as meaningful objects on their own. Physics gets it closer to correct because it tries to be "covariant", where the meaningful answers to questions have to either have units on them or be totally unitless e.g. irrespective of coordinate system. The two spaces Rx(RxR) and (RxR)xR have many isomorphisms between them (every possible coordinate change, for instance). But what matters, what makes them "canonically isomorphic", is not isomorphisms in how they are _constructed_ but in how they are _used_. When you write an element as (a,b,c), what you mean is that when you are asked for the values of three possible projections you will answer with the values a, b, and c. Regardless of how you define your product spaces, the product of (a), (b), and (c) are going to produce three projections that give the same answers when they are used (if not, you built them wrong). Hence they are indistinguishable, hence canonically isomorphic. This is exactly the way that physics always treats coordinates: sure, you can write down a function like V(x), but it's really a function from "points" in x to "points" in V, which happens to be temporarily written in terms of a coordinate system on x and a coordinate system on V. We just write it as V(x) because we're usually going to use it that way later. Any unitless predictions you get to any actual question are necessarily unchanged by those choices of coordinate systems (whereas if they have units then they are measured in one of the coordinate systems). So I would say that (a,(b,c)) and ((a,b), c) are just two different coordinate systems for R^3. But necessarily any math you do with R^3 can't depend on the choice of coordinates. There is probably a way to write that by putting something like "units" on every term and then expecting the results of any calculation to be unitless.
- generationP 2y ago
  This is exactly the "specification by universal property" that the author is talking about. In your case, it's saying "a 3-dimensional vector space is a vector space with three chosen vectors e, f, g and three linear maps x, y, z such that each vector v equals x(v) e + y(v) f + z(v) g". But as the author points out, not everything follows from universal properties, and when it does, there is often several universal properties defining the same object, and that sameness itself needs to be shown.
rhelz 2y ago
This is a very old consideration (cf https://www.jstor.org/stable/2183530 https://www.jstor.org/stable/2183530). If you want to frame a 'universal defining property', you have to frame it in some language. The definition, therefore, is inevitably idiosyncratic to that language, and, if you specify the same property using a different language, the definition is going to change. What's more, the two definitions can be incommensurable. And---all you have done is translate from the object language to the meet language--leaving the definitions of the terms of the meta language completely unexplicated. The solution to this is as old too---like "point", "line", etc, these terms can--and arguably should--remain completely un-defined.
- ysofunny 2y ago
  whence did you learn this idiom of "the meet language"??? i have working definitions of line, point, etc.. in terms of dimensions. but I have some issues with the precise definition of "dimension" due to having picked up the concept of "density". I cannot say what's the difference between density and dimension
  - rhelz 2y ago
    sigh I really hate autocorrect. It was supposed to be "meta", not "meet". It's bad enough that most of the content I read these days is being generated by LLMs. Slowly and inexorably, even the content I write is being written and overwritten by LLMs.
  - jhanschoo 2y ago
    Meet here is shorthand the comment author is using for: https://en.wikipedia.org/wiki/Join_and_meet https://en.wikipedia.org/wiki/Join_and_meet You should read it as: "the largest group of properties that both languages agree about said abstractly defined mathematical object."
    - rhelz 2y ago
      chuckle thanks for this heroic effort to charitably interpret me as actually being able to type in a coherent sentence :-) But, alas, I was just trying to type in "meta" and it was auto-completed to "meet". I really, really, hate autocomplete.
ysofunny 2y ago
reminicscent of Euler's use of Pi? I recall that Euler would write Pi but sometimes he meant 2*pi, or possibly pi/2 depending on context
- deleted 2y ago
  [deleted]
hackandthink 2y ago
This is an excellent text to understand mathematical structuralism. But it feels anticlimactic. At the beginning there are fundamental problems with mathematical equality. In the end, there is no great new idea but only the observation that in algebraic geometry some proofs have holes (two kinds), but they can be filled (quite) schematically.
- ducttapecrown 2y ago
  "Some proofs" are the proof used to verify that the definition of an affine scheme makes sense, and the author motions in the direction that every single proof in algebraic geometry uses identically wrong arguments when using the language of "canonical" maps. Thus the replication crisis of mathematics is revealed. In the words of John Conway: a map is canonical if you and your office neighbor write down the same map.
- Koshkin 2y ago
  At least it's a short piece, compared to A New Kind of Science.
abeppu 2y ago
I haven't actually dug up the source, so I'm not sure if the gaps here are related, but GC Rota apparently claimed that one reason the umbral calculus remained mysterious for as long as it did was about ambiguities with `=`. > Rota later stated that much confusion resulted from the failure to distinguish between three equivalence relations that occur frequently in this topic, all of which were denoted by "=". https://en.wikipedia.org/wiki/Umbral_calculus#The_modern_umbral_calculus https://en.wikipedia.org/wiki/Umbral_calculus#The_modern_umb...
- dan_mctree 2y ago
  There's so much ambiguous context that goes into your average '=', even when just talking about your standard functions on real numbers. You'll see it being used for anything from: - We've found these to be equal - We're hypothesizing this to be equal - These are approximately equal - These are defined to be equal - This is a way to calculate something else, whether it's equal is up to your philosophy (a^2+b^2=c^2) - I'm transforming my function into something else that looks different but is exactly the same - I'm transforming my function into something else that is the same for some of the stuff I care about (but for example does not work anymore for negative numbers, complex nrs, etc.) - I'm transforming my function into something else, but it's actually a trapdoor, and you can't convert it back. - This is kind of on average true within an extremely simplified context or we know it's not true at all, but we'll pretend for simplification (looking at you physics) - We are trying to check if these two are equal - This is equal, but only within a context where these variables follow some constraints mentioned somewhere else entirely - This is equal, but, we're not going to say whether you can or can't replace the variables with functions or whether it supports complex nrs, negative nrs, non-integers, etc. A lot of this is usually kind of clear from context, but some of these differences are a nightmare if you want to code it out
perihelions 2y ago
I was just thinking about something adjacent to this the other day. I had this half-baked idea that you could classify all the "types" built out of, say (R, ×, →) by algebraically replacing each copy of R with a finite set of cardinality a and then counting the cardinality of the entire type expression. So you'd formally associate, say, R^3 with the algebraic term a^3, and that holds regardless of how you rearrange R^3 = R^2 × R or R × R^2 or whatever. I liked the idea because it seemed (?) to derive non-obvious set theoretic equivalences, for free: such as R -> (R -> R) ~ (a^a)^a = a^(a^2) R^2 -> R ~ a^(a^2) (R -> R)^2 ~ (a^a)^2 = a^(2a) R -> R^2 ~ a^(2a) The first equivalence is between a "curried", partial-application, function form of a function of two arguments, and the "uncurried" form which takes a tuple argument. The second equivalence is between a pair of real functions and a path in the plane R^2—the two functions getting identified with the coordinate paths x(t) and y(t). (Remember the cardinality of distinct functions over finite sets S -> T is |T|^|S|). And I think you can take this further, I'm not sure how far, for example by associating different formal parameters a,b,c... for different abstract types S,T,U... Is this a trick that's already known, in type theory? (My motivation was to try to classify the "complexity", "size", of higher-ordered functions over the reals. The inspiration's that you're imagining a numerical approximation on a grid of size a for (a finite subinterval in) each copy of R: then that cardinality relates to the memory size of the numerical algorithm, working inside that space. And you could interpret the asymptotic growth of the formal function, as a complexity measure of the space. If you think of R^n -> R as a "larger" function space than R -> R^n, that observation maps to a^(a^n) being an asymptotically faster-growing function (of 'a') than (a^n)^a = a^(na). And similarly the functionals, (R -> R) -> R, and function operators (like differential operators) (R -> R) -> (R -> R), form a hierarchy of increasing "size").
- cvoss 2y ago
  The connection between type isomorphisms and algebraic equalities is known and explored in a variety of interesting ways. I don't know the precise history of the development of the notation and vocabulary, but there's a reason types like A+B are notated with a plus symbol and called "sums". Similarly for products. And it may surprise you (or not) to learn that people sometimes call A -> B an exponential type, and even notate it with superscript notation. One of my favorites is the result that the binary tree type is isomorphic to septuples of binary trees, which you can arrive at by using the definition of binary trees as the fixed point solution of T = 1 + T*T and deriving T = T^7 with some algebra. [0] [0] https://arxiv.org/abs/math/9405205 https://arxiv.org/abs/math/9405205
joewferrara 2y ago
kevin buzzard is a very good(usually math) expositor with a bent towards programming. love it
deleted 2y ago
[deleted]
_as_text 2y ago
I really like this. I remember my first serious math book, which was this old-school set theory and topology book, and being all excited about learning set theory up until I encountered iterated Cartesian product, and was forced to accept that ((x, y), z) and (x, (y, z)) are supposed to be indistinguishable to me. An answer on StackExchange said that "you will never, ever, ever need to worry about the details of set theory", but I still did.
giardini 2y ago
And I thought "Grothendieck" was a German social disease! I'm getting a real education here on HN!
- hanche 2y ago
  The story of Grothendieck is really fascinating. He was a superstar in algebraic geometry, only to suddenly reject the endeavor of mathematics and going off to grow vegetables in the Pyrenees. He also demanded that all notes from his lectures be destroyed. But those notes existed in so many hands, I don’t think many people (if any) complied.
_as_text 2y ago
I have now read the paper and it alone is enough to make me seriously consider devoting significant amount of my time to the author's project. Here's why: In my introductory statistics class, I learned that a independent and identically distributed sample is a sequence of random variables X[1], ..., X[n], all of the same signature Omega -> (usually) R. All of them are pairwise independent, and all of them have the same distribution, e.g. the same density function. Elsewhere in probability I have learned that two random variables that have the same density function are, for all intents and purposes, the same. For all, really? Let's take X[i] and X[j] from some i.i.d. random sample, i != j. They have the same density, which leads us to write X[i] = X[j]. They are also independent, hence P(X[i] in A, X[j] in A) = P(X[i] in A)*P(X[j] in A), but X[i] = X[j], so P(X[i] in A, X[j] in A) = P(X[i] in A, X[i] in A) = P(X[i] in A), so P(X[i] in A) in {0, 1}. This was a real problem for me, and I believe I had worse results in that statistics class than I would have if the concept was introduced properly. It took me a while to work out a solution for this. Of course, you can now see that the strict equality X[i] = X[j] is indefensible, in the sense that in general X[i](omega) != X[j](omega) for some atom omega. If you think about what needs to be true about Omega in order for it to have two different variables, X[i] and X[j]:Omega -> R, that are i.i.d, then it will turn out that you need Omega to be a categorical product of two probability spaces: Omega = Omega[i] x Omega[j] and X[i] (resp. X[j]) to be the same variable X composed with projection onto first (resp. second) factor. This definition of "sampling with replacement" is able to withstand all scrutiny. Of course, just like in Buzzard's example of ring localization, it was all caused by someone being careless about using equality.

178 points by golol 2y ago

fmap 2y ago

For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken... *) I'm going by second hand accounts here, please correct me if you think this statement is too strong.

bumbledraven 2y ago
For reference, the paper mentions the term "homotopy" exactly once, in this sentence: > The set-theoretic definition is too strong (Cauchy reals and Dedekind reals are certainly not equal as sets) and the homotopy type theoretic definition is too weak (things can be equal in more than one way, in contrast to Grothendieck’s usage of the term).
cwzwarich 2y ago
> For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. Arguably, Homotopy type theory still doesn't solve the problem, because while it strengthens the consequences of isomorphism it doesn't distinguish between "isomorphism" and "canonical isomorphism", whereas (some?) mathematicians informally seem to think that there's a meaningful difference. > The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken... In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory. It's far from established that this is possible at all with homotopy type theory, yet alone whether it would actually be easier or more economical to do so. And even if this state of affairs is permanent, homotopy type theory itself would still be an interesting topic of study like any other field of mathematics.
- lupire 2y ago
  "Canonical" refers largely to the names we give to things, so that we maximize the extent to which an isomorphism maps the object named A in X to the object named A in Y. And also to choosing an isomorphism that embeds in a different isomorphism (of superstructures) that isn't strictly the topic of the current question. I don't think anyone thinks canonical isomorphisms are mathematically controversial (except some people having fun with studying scenarios where more than one isomorphism is equally canonical, and other meta studies), they are a convenient communication shorthand for avoiding boring details. https://en.m.wikipedia.org/wiki/Isomorphism_theorems https://en.m.wikipedia.org/wiki/Isomorphism_theorems
  - moomin 2y ago
    I think the original author makes a good case that a) the shorthand approach isn’t going to fly as we formalise b) different mathematicians mean different things by canonical and these details matter when trying to combining results and that therefore 3) it would be better to provide a proper definition of what you’re talking about and give it an unambiguous name.
  - euiq 2y ago
    let me guess: you haven't read the article, have you?
    - xigoi 2y ago
      > Please don't comment on whether someone read an article. "Did you even read the article? It mentions that" can be shortened to "The article mentions that". https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- fmap 2y ago
  > it doesn't distinguish between "isomorphism" and "canonical isomorphism" You can distinguish these concepts in (higher )category theory, where isomorphisms are morphisms in groupoids and canonical isomorphisms are contractible spaces of morphisms. These sound like complicated concepts, but in HoTT you can discover the same phenomena as paths in types (i.e., equality) and a simple definition of contractibility which looks and works almost exactly like unique existence. > In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory. The authors of Lean are brilliant and I'm extremely happy that more mathematicians are looking into formalisations and recognizing the additional challenges that this brings. At the same time, it's a little bit depressing that we had finally gotten a good answer to many (not all!) of these additional challenges only to then retreat back to familiar ground. Anyway, there were several responses to my original comment and instead of answering each individually, I'm just going to point to the article itself. The big example from section 5 is that of localisations of R-algebras. Here is how this whole discussion changes in HoTT: 1) We have a path R[1/f][1/g] = R[1/fg], therefore the original theorem is applicable in the case that the paper mentions. 2) The statements in terms of "an arbitrary localisation" and "for all particular localisations" are equivalent. 3) ...and this is essentially because in HoTT there is a way to define the localisation of an R-algebra at a multiplicative subset. This is a higher-inductive type and the problematic aspects of the definition in classical mathematics stem from the fact that this is not (automatically) a Set. A higher-inductive definition is a definition by a universal property, yet you can work with this in the same way as you would with a concrete construction and the theorems that the article mentions are provable. --- There is much more that can be said here and it's not all positive. The only point I want to make is that everybody who ever formalised anything substantial is well aware of the problem the article talks about: you need to pick the correct definitions to formalise, you can't just translate a random math textbook and expect it to work. Usually, you need to pick the correct generalisation of a statement which actually applies in all the cases where you need to use it. Type theory is actually especially difficult here, because equality in type theory lacks many of the nice properties that you would expect it to have, on top of issues around isomorphisms and equality that are left vague in many textbooks/papers/etc. HoTT really does solve this issue. It presents a host of new questions and it's almost certain that we haven't found the best presentation of these ideas yet, but even the presentation we have solves the problems that the author talks about in this article.
voxl 2y ago
Classical versus non-classical has nothing to do with it. HoTT does not work to capture what a mathematician means by "unique isomorphism" because witnesses of equality in HoTT are very much not unique.
jhanschoo 2y ago
Can you elaborate more on how you think HoTT can solve the issue Buzzard mentions that when formalizing informal mathematics, the author frequently has a model (or, a particular construction) in mind and requires properties present in the model, and then claims that this is true for all "canonically equivalent" objects without actually spending time explicating the abstract nonsense required to properly specify the properties that canonically equivalent objects preserve, for their developement? (see: a product vs. the product) Edit: and furthermore, the situation where the obvious choice of universal property (read: level of isomorphism) was a poor one, in their attempt to formalize localizations.
YetAnotherNick 2y ago
I think 99.9% of the people talking about HoTT haven't used HoTT in practice. They just see isomorphism is equivalent to equivalence(or something similar), comes up with a mental model and think this is the main contribution of HoTT, whereas isomorphism is a well studied thing even before formal set theory was a thing. HoTT gets weird and anyone who has tried any tool to prove anything in HoTT knows this, and this is the reason why it didn't got adopted even though many leading tools like lean worked hard to implement it.
- deleted 2y ago
  [deleted]
- staunton 2y ago
  Have you used it? If yes, could you elaborate? Or if you haven't, can you point to any recent source on what it's like to be using HoTT in 2024?
  - YetAnotherNick 2y ago
    [1] is the only video which I would say I found any bit accessible. But to be honest even after spending days, I couldn't grok it. And in my observation, different implementations of HoTT are quite different from each other. [1]: https://www.youtube.com/watch?v=x4cz1OgpU3M https://www.youtube.com/watch?v=x4cz1OgpU3M
nicklecompte 2y ago
I think HOTT helps remove a lot of the footguns and computational hairiness around using type-theoretic mathematics. But the issues Buzzard is talking about are really more profound than that. This relates to a much deeper (but familiar and nontechnical) philosophical problem: you assign a symbol to a thing, and read two sentences that refer to the same symbol ("up to isomorphism"), but not necessarily the same thing. If the sentences contradict each other, is it because they disagree on the meaning of the symbol, or do they disagree on the essence of the thing? There is a strong argument that most debates about free will and consciousness are really about what poorly-understood thing(s) we are assigning to the symbol. Worse, this makes such debates ripe for bad faith, where flaws in an argument are defended by implicitly changing the meaning of the symbol. In the context of """simple""" mathematics, preverbal toddlers and chimpanzees clearly have an innate understanding of quantity and order. It's only after children fully develop this innate understanding that there's any point in teaching them "one," "two," "three," and thereby giving them the tools for handling larger numbers. I don't think it makes sense to say that toddlers understand the Peano axioms. Rather, Peano formulated the axioms based on his own (highly sophisticated) innate understanding of number. But given he spent decades of pondering the topic, it seems like Peano's abstract conception of "number" became different from (say) Kronecker's, or other constructivists/etc. Simply slapping the word "integer" on two different concepts and pointing out that they coincide for quantities we can comprehend doesn't actually do anything by itself to address the discrepancy in concept revealed by Peano allowing unbounded integers and Kronecker's skepticism. (The best argument against constructivism is essentially sociological and pragmatic, not "mathematically rational.") Zooming out a bit, I suspect we (scientifically-informed laypeople + many scientists) badly misunderstand the link between language and human cognition. It seems more likely to me that we have extremely advanced chimpanzee brains that make all sorts of sophisticated chimpanzee deductions, including the extremely difficult question of "what is a number?", but to be shared (and critically investigated) these deductions have to be squished into language, as a woefully insufficient compromise. And I think a lot of philosophical - and metamathematical - confusion can be understood as a discrepancy between our chimpanzee brains having a largely rigorous understanding of something, but running into limits with our Broca's and Wernicke's areas, limits which may or may not be fixed by "technological development" in human language. (Don't even get me started on GPT...)
Ericson2314 2y ago
The fact that Buzzard is writing this paper at all to me shows a much higher degree of respect than before --- see how humble the overview is. I think this is great progress!
zozbot234 2y ago
> It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place. It's not that simple, Buzzard actually seems to be quite familiar with HoTT. The HoTT schtick of defining equality between types as isomorphism does 'handle' these issues for you in the sense that they are treated rigorously, but there's no free lunch in that. You still need to do all the usual work establishing compatibility of values, functions etc. with the relevant isomorphisms, so other than the presentation being somewhat more straightforward there is not much of a gain in usability.
- zozbot234 2y ago
  Sorry about not providing a reference re: Kevin Buzzard's previously-stated thoughts on HoTT, but see https://ncatlab.org/nlab/show/Kevin+Buzzard https://ncatlab.org/nlab/show/Kevin+Buzzard

juped 2y ago

Equality can be philosophically troubling, but as a practical matter, what you care about is the indiscernibility of identicals, and if every property you use follows from a universal property, then equal up to isomorphism is just equal. So every Rubik's cube is equal considered as a group of face rotations, and there's only one Rubik's cube, but if you care about chemical properties of sticker glue, they're no longer equal.

deleted 2y ago
[deleted]
moomin 2y ago
Something the author points out: sometimes theorems directly rely on specific constructions of mathematical objects, which are then used to establish things that do not mention the construction.
passion__desire 2y ago
The glue point reminds me of Benacerraf problem. https://en.m.wikipedia.org/wiki/Benacerraf%27s_identification_problem https://en.m.wikipedia.org/wiki/Benacerraf%27s_identificatio...
Koshkin 2y ago
> Equality can be philosophically troubling Which is probably why they are saying "equity" now

generationP 2y ago

This is probably better known here under the name of implicit type conversions. Strictly speaking, the rational number 1 is not the same as the integer 1; we just have a conversion map that preserves all the relevant properties. It's all fun and games until there are 1000 types and 10000 conversion maps involved and the relevant diagrams no longer commute (i.e., it depends what order you go).

actionfromafar 2y ago
I assume you mean any random enterprise codebase? Because that is any random enterprise codebase.
- 082349872349872 2y ago
  In other areas, one might compare code jurisdictions, where presumably all the legislative clauses share a common vocabulary (and probably even conceptual framework), with common law jurisdictions, where all the legislative clauses occur in different centuries and thus one adds "picking a parallel transport" between the legal languages of the times (and jurisdictions) to the difficulties of adjudication.
- om8 2y ago
  Not if you use a language that bans implicit type conversions (like go)
  - actionfromafar 2y ago
    I was thinking in much more abstract terms. You have information from a webflow, at some point converted to an XML message, converted to database entry, again to a JSON document, combined with an Azure workitem, then sent to Salesforce. At any one point the data can interact with other systems, travel through codebases each seeing the data through their types, legacy APIs, the same-(ish) new-(ish) RPC API and in each service the data is represented in its own internal quirky way. Sure, throw Go in that mix, hell at this point the more merrier! :)
2y ago

nyc111 2y ago

When this subject comes up I always think that the equality sign is loaded. It can mean, definition, equality, identity, and proportionality. How come this state of the equality sign is not mentioned in the paper?

mikhailfranco 2y ago
up to (non-)unique isomorphism
mxmlnkn 2y ago
As far as I remember, that's not a problem in math: := definition ≡ identity = equality ∝ proportionality
- nyc111 2y ago
  But this is how it works: = definition = identity = equality = proportionality
  - Twisol 2y ago
    Big-O notation is a famous example where = is some flavor of (asymptotic) proportionality, and it catches a lot of people out when they first learn about it.
yau8edq12i 2y ago
As a mathematician, I have never, ever seen the equal sign used to denote proportionality. I cannot tell what you mean by "identity" that wouldn't be equality. And a definition in the sense you seem to mean is, indeed, also an equality. I guess this issue not mentioned in the paper because it doesn't exist.
- ducttapecrown 2y ago
  [x:y] = [lx:ly] and I suppose the model of localization discussed in the article above counts as well.

lupire 2y ago

"When is one thing equal to some other thing?" Barry Mazur June 12, 2007 https://bpb-us-e1.wpmucdn.com/sites.harvard.edu/dist/a/189/files/2023/01/When-is-one-thing-equal-to-some-other-thing.pdf https://bpb-us-e1.wpmucdn.com/sites.harvard.edu/dist/a/189/f... https://people.math.osu.edu/cogdell.1/6112-Mazur-www.pdf https://people.math.osu.edu/cogdell.1/6112-Mazur-www.pdf

ajkjk 2y ago

I'm typing this after reading their section on page 6 about the "pentagon axiom". They write that RxR^2, R^2xR, and R^3 are isomorphic, but not literally equal under different constructions, because (a,(b,c)) is different from ((a,b), c), and that this is a problem. I feel like math kinda gets this wrong by treating sets as meaningful objects on their own. Physics gets it closer to correct because it tries to be "covariant", where the meaningful answers to questions have to either have units on them or be totally unitless e.g. irrespective of coordinate system. The two spaces Rx(RxR) and (RxR)xR have many isomorphisms between them (every possible coordinate change, for instance). But what matters, what makes them "canonically isomorphic", is not isomorphisms in how they are _constructed_ but in how they are _used_. When you write an element as (a,b,c), what you mean is that when you are asked for the values of three possible projections you will answer with the values a, b, and c. Regardless of how you define your product spaces, the product of (a), (b), and (c) are going to produce three projections that give the same answers when they are used (if not, you built them wrong). Hence they are indistinguishable, hence canonically isomorphic. This is exactly the way that physics always treats coordinates: sure, you can write down a function like V(x), but it's really a function from "points" in x to "points" in V, which happens to be temporarily written in terms of a coordinate system on x and a coordinate system on V. We just write it as V(x) because we're usually going to use it that way later. Any unitless predictions you get to any actual question are necessarily unchanged by those choices of coordinate systems (whereas if they have units then they are measured in one of the coordinate systems). So I would say that (a,(b,c)) and ((a,b), c) are just two different coordinate systems for R^3. But necessarily any math you do with R^3 can't depend on the choice of coordinates. There is probably a way to write that by putting something like "units" on every term and then expecting the results of any calculation to be unitless.

generationP 2y ago
This is exactly the "specification by universal property" that the author is talking about. In your case, it's saying "a 3-dimensional vector space is a vector space with three chosen vectors e, f, g and three linear maps x, y, z such that each vector v equals x(v) e + y(v) f + z(v) g". But as the author points out, not everything follows from universal properties, and when it does, there is often several universal properties defining the same object, and that sameness itself needs to be shown.

rhelz 2y ago

This is a very old consideration (cf https://www.jstor.org/stable/2183530 https://www.jstor.org/stable/2183530). If you want to frame a 'universal defining property', you have to frame it in some language. The definition, therefore, is inevitably idiosyncratic to that language, and, if you specify the same property using a different language, the definition is going to change. What's more, the two definitions can be incommensurable. And---all you have done is translate from the object language to the meet language--leaving the definitions of the terms of the meta language completely unexplicated. The solution to this is as old too---like "point", "line", etc, these terms can--and arguably should--remain completely un-defined.

ysofunny 2y ago
whence did you learn this idiom of "the meet language"??? i have working definitions of line, point, etc.. in terms of dimensions. but I have some issues with the precise definition of "dimension" due to having picked up the concept of "density". I cannot say what's the difference between density and dimension
- rhelz 2y ago
  sigh I really hate autocorrect. It was supposed to be "meta", not "meet". It's bad enough that most of the content I read these days is being generated by LLMs. Slowly and inexorably, even the content I write is being written and overwritten by LLMs.
- jhanschoo 2y ago
  Meet here is shorthand the comment author is using for: https://en.wikipedia.org/wiki/Join_and_meet https://en.wikipedia.org/wiki/Join_and_meet You should read it as: "the largest group of properties that both languages agree about said abstractly defined mathematical object."
  - rhelz 2y ago
    chuckle thanks for this heroic effort to charitably interpret me as actually being able to type in a coherent sentence :-) But, alas, I was just trying to type in "meta" and it was auto-completed to "meet". I really, really, hate autocomplete.

ysofunny 2y ago

reminicscent of Euler's use of Pi? I recall that Euler would write Pi but sometimes he meant 2*pi, or possibly pi/2 depending on context

deleted 2y ago
[deleted]

hackandthink 2y ago

This is an excellent text to understand mathematical structuralism. But it feels anticlimactic. At the beginning there are fundamental problems with mathematical equality. In the end, there is no great new idea but only the observation that in algebraic geometry some proofs have holes (two kinds), but they can be filled (quite) schematically.

ducttapecrown 2y ago
"Some proofs" are the proof used to verify that the definition of an affine scheme makes sense, and the author motions in the direction that every single proof in algebraic geometry uses identically wrong arguments when using the language of "canonical" maps. Thus the replication crisis of mathematics is revealed. In the words of John Conway: a map is canonical if you and your office neighbor write down the same map.
Koshkin 2y ago
At least it's a short piece, compared to A New Kind of Science.

abeppu 2y ago

I haven't actually dug up the source, so I'm not sure if the gaps here are related, but GC Rota apparently claimed that one reason the umbral calculus remained mysterious for as long as it did was about ambiguities with `=`. > Rota later stated that much confusion resulted from the failure to distinguish between three equivalence relations that occur frequently in this topic, all of which were denoted by "=". https://en.wikipedia.org/wiki/Umbral_calculus#The_modern_umbral_calculus https://en.wikipedia.org/wiki/Umbral_calculus#The_modern_umb...

dan_mctree 2y ago
There's so much ambiguous context that goes into your average '=', even when just talking about your standard functions on real numbers. You'll see it being used for anything from: - We've found these to be equal - We're hypothesizing this to be equal - These are approximately equal - These are defined to be equal - This is a way to calculate something else, whether it's equal is up to your philosophy (a^2+b^2=c^2) - I'm transforming my function into something else that looks different but is exactly the same - I'm transforming my function into something else that is the same for some of the stuff I care about (but for example does not work anymore for negative numbers, complex nrs, etc.) - I'm transforming my function into something else, but it's actually a trapdoor, and you can't convert it back. - This is kind of on average true within an extremely simplified context or we know it's not true at all, but we'll pretend for simplification (looking at you physics) - We are trying to check if these two are equal - This is equal, but only within a context where these variables follow some constraints mentioned somewhere else entirely - This is equal, but, we're not going to say whether you can or can't replace the variables with functions or whether it supports complex nrs, negative nrs, non-integers, etc. A lot of this is usually kind of clear from context, but some of these differences are a nightmare if you want to code it out

perihelions 2y ago

I was just thinking about something adjacent to this the other day. I had this half-baked idea that you could classify all the "types" built out of, say (R, ×, →) by algebraically replacing each copy of R with a finite set of cardinality a and then counting the cardinality of the entire type expression. So you'd formally associate, say, R^3 with the algebraic term a^3, and that holds regardless of how you rearrange R^3 = R^2 × R or R × R^2 or whatever. I liked the idea because it seemed (?) to derive non-obvious set theoretic equivalences, for free: such as R -> (R -> R) ~ (a^a)^a = a^(a^2) R^2 -> R ~ a^(a^2) (R -> R)^2 ~ (a^a)^2 = a^(2a) R -> R^2 ~ a^(2a) The first equivalence is between a "curried", partial-application, function form of a function of two arguments, and the "uncurried" form which takes a tuple argument. The second equivalence is between a pair of real functions and a path in the plane R^2—the two functions getting identified with the coordinate paths x(t) and y(t). (Remember the cardinality of distinct functions over finite sets S -> T is |T|^|S|). And I think you can take this further, I'm not sure how far, for example by associating different formal parameters a,b,c... for different abstract types S,T,U... Is this a trick that's already known, in type theory? (My motivation was to try to classify the "complexity", "size", of higher-ordered functions over the reals. The inspiration's that you're imagining a numerical approximation on a grid of size a for (a finite subinterval in) each copy of R: then that cardinality relates to the memory size of the numerical algorithm, working inside that space. And you could interpret the asymptotic growth of the formal function, as a complexity measure of the space. If you think of R^n -> R as a "larger" function space than R -> R^n, that observation maps to a^(a^n) being an asymptotically faster-growing function (of 'a') than (a^n)^a = a^(na). And similarly the functionals, (R -> R) -> R, and function operators (like differential operators) (R -> R) -> (R -> R), form a hierarchy of increasing "size").

cvoss 2y ago
The connection between type isomorphisms and algebraic equalities is known and explored in a variety of interesting ways. I don't know the precise history of the development of the notation and vocabulary, but there's a reason types like A+B are notated with a plus symbol and called "sums". Similarly for products. And it may surprise you (or not) to learn that people sometimes call A -> B an exponential type, and even notate it with superscript notation. One of my favorites is the result that the binary tree type is isomorphic to septuples of binary trees, which you can arrive at by using the definition of binary trees as the fixed point solution of T = 1 + T*T and deriving T = T^7 with some algebra. [0] [0] https://arxiv.org/abs/math/9405205 https://arxiv.org/abs/math/9405205

joewferrara 2y ago

kevin buzzard is a very good(usually math) expositor with a bent towards programming. love it

deleted 2y ago

[deleted]

_as_text 2y ago

I really like this. I remember my first serious math book, which was this old-school set theory and topology book, and being all excited about learning set theory up until I encountered iterated Cartesian product, and was forced to accept that ((x, y), z) and (x, (y, z)) are supposed to be indistinguishable to me. An answer on StackExchange said that "you will never, ever, ever need to worry about the details of set theory", but I still did.

giardini 2y ago

And I thought "Grothendieck" was a German social disease! I'm getting a real education here on HN!

hanche 2y ago
The story of Grothendieck is really fascinating. He was a superstar in algebraic geometry, only to suddenly reject the endeavor of mathematics and going off to grow vegetables in the Pyrenees. He also demanded that all notes from his lectures be destroyed. But those notes existed in so many hands, I don’t think many people (if any) complied.

_as_text 2y ago

I have now read the paper and it alone is enough to make me seriously consider devoting significant amount of my time to the author's project. Here's why: In my introductory statistics class, I learned that a independent and identically distributed sample is a sequence of random variables X[1], ..., X[n], all of the same signature Omega -> (usually) R. All of them are pairwise independent, and all of them have the same distribution, e.g. the same density function. Elsewhere in probability I have learned that two random variables that have the same density function are, for all intents and purposes, the same. For all, really? Let's take X[i] and X[j] from some i.i.d. random sample, i != j. They have the same density, which leads us to write X[i] = X[j]. They are also independent, hence P(X[i] in A, X[j] in A) = P(X[i] in A)*P(X[j] in A), but X[i] = X[j], so P(X[i] in A, X[j] in A) = P(X[i] in A, X[i] in A) = P(X[i] in A), so P(X[i] in A) in {0, 1}. This was a real problem for me, and I believe I had worse results in that statistics class than I would have if the concept was introduced properly. It took me a while to work out a solution for this. Of course, you can now see that the strict equality X[i] = X[j] is indefensible, in the sense that in general X[i](omega) != X[j](omega) for some atom omega. If you think about what needs to be true about Omega in order for it to have two different variables, X[i] and X[j]:Omega -> R, that are i.i.d, then it will turn out that you need Omega to be a categorical product of two probability spaces: Omega = Omega[i] x Omega[j] and X[i] (resp. X[j]) to be the same variable X composed with projection onto first (resp. second) factor. This definition of "sampling with replacement" is able to withstand all scrutiny. Of course, just like in Buzzard's example of ring localization, it was all caused by someone being careless about using equality.