[HN Gopher] Grothendieck's use of equality
___________________________________________________________________
Grothendieck's use of equality
Author : golol
Score : 132 points
Date : 2024-05-20 11:41 UTC (11 hours ago)
(HTM) web link (arxiv.org)
(TXT) w3m dump (arxiv.org)
| fmap wrote:
| 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 wrote:
| 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 wrote:
| > 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 wrote:
| "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
| moomin wrote:
| 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 wrote:
| let me guess: you haven't read the article, have you?
| fmap wrote:
| > 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 wrote:
| 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 wrote:
| 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 wrote:
| 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.
| staunton wrote:
| 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 wrote:
| [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
| nicklecompte wrote:
| 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 wrote:
| 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 wrote:
| > 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.
| juped wrote:
| 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.
| moomin wrote:
| 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 wrote:
| The glue point reminds me of Benacerraf problem.
|
| https://en.m.wikipedia.org/wiki/Benacerraf%27s_identificatio...
| generationP wrote:
| 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 wrote:
| I assume you mean any random enterprise codebase? Because that
| is any random enterprise codebase.
| 082349872349872 wrote:
| 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 wrote:
| Not if you use a language that bans implicit type conversions
| (like go)
| actionfromafar wrote:
| 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! :)
| nico wrote:
| Or when your formulas on Google sheets start failing because
| you do 1-1 and the result is not 0, and then you spend 30
| minutes creating new sheets, searching the web and double
| checking everything, until you realize that the value on the
| cell wasn't 1, but 1.
|
| This happened to me yesterday
| boppo1 wrote:
| Can you elaborate?
| gatane wrote:
| 1 vs 1.0 ???
| nico wrote:
| Now I noticed that the period at the end of the paragraph
| is a bit unfortunate
|
| The value was 1. which I guess is shorthand for 1.0 and
| it's technically not the same value as 1
|
| On top of that, sometimes values like 0.961727 will be
| shown as 1, so sometimes you think that the value in the
| cell you are referring to is a 1 but instead it's something
| close to it
|
| In particular I was making a list of array positions from 1
| to 32 and calculating x,y coordinates from the position
| using the formulas (x = (i-1) % width, y = (i-1)/width)
|
| Some of the coordinates were wrong, and it was because the
| i values were not integers, which I couldn't tell just by
| looking at the sheet, and only realized it when double
| clicked on the cells
| jkaptur wrote:
| It's frustrating that there isn't an easy way to see the
| "canonical" value and format of a cell (in Sheets or
| Excel).
|
| Just looking at a cell, it's not trivial to see if it's
| the number 1 or the string 1 (you can enter text by using
| a leading apostrophe, but that's not the _only_ way to
| get text in a cell!). Numbers and strings have different
| alignments by default, but that can be overridden. The
| numeric value of the string 1 is 0 if you 're using the
| SUM formula, but it's 1 if you use +. In other words,
| =A1+A2 does not necessarily equal =SUM(A1:A2)
|
| Then you can format numbers however you like. For
| example, dates are stored in spreadsheets as days since
| an epoch (not the Unix epoch). So you can have the number
| 2 in a spreadsheet cell, then format it as a date, but
| just the day of the month, and it can appear as 1.
|
| There's rounding, which bit you. 0.95 can appear as 1 if
| you display fewer decimal places.
|
| Finally, there's the fact that the calculation is done
| like IEEE 754. Programmers are used to floating point
| numbers and the fact that properties like associativity
| don't apply, but that's not obvious to everyone.
| boppo1 wrote:
| Thank you!
| paulddraper wrote:
| 1 is an integer, a rational number, a positive integer, an odd
| integer, a power of 2, etc.
| sharkbot wrote:
| It's also a complex number, a Unicode character, an ASCII
| character, an Extended ASCII character, a glyph, the
| multiplicative identity element, a raster image, ...
|
| The GP point is correct; we implicitly convert between all
| these representations naturally and quickly, but there are
| interesting branches of mathematics that consider those
| conversions explicitly and find nuances (eg, category
| theory).
| kbolino wrote:
| But the integers are a subset of the rationals, which are a
| subset of the reals, which are a subset of the complex
| numbers. Looking only at the objects _and not their
| operations_ 1 (integer) = 1 (rational) = 1 (real) = 1
| (complex). Moreover, when we do account for the operations,
| we also see that 1 + 1 = 2 and 1 * 1 = 1 in every one of
| those systems. This isn 't just a coincidence, of course;
| it's by design.
|
| However, the way you arrive at 1 + 1 = 2 is _not_ the same
| (though I suppose you could short-circuit the algorithm).
| Rational addition requires finding a common denominator,
| while integer addition doesn 't. They achieve the same
| result when the inputs are integers, and again this is by
| design, but the process isn't the same. Ditto real addition
| vs. rational and complex addition vs. real.
|
| In higher-level mathematics, the operations on the objects
| become definitional. We don't look at just a set of things,
| we look at a set of things and the set of operations upon
| those things. Thus "1 with integer addition and integer
| multiplication" becomes the object under consideration
| (even if it's just contextually understood) instead of
| simply 1. This is why they don't satisfy higher-level
| notions of equivalence, even if they intentionally do
| satisfy simple equality as taught in grade school.
|
| Of course, the entire point of the submitted paper is to
| examine this in detail.
| JadeNB wrote:
| > But the integers are a subset of the rationals, which
| are a subset of the reals, which are a subset of the
| complex numbers.
|
| It depends on definitions, and, in some sense, the point
| of the common approach to mathematics is not just that
| one does not, but that one cannot, ask such questions.
| One approach is to look at natural numbers set
| theoretically, starting with 0 = [?]; to define integers
| as equivalence classes of pairs of natural numbers; to
| define rational numbers as equivalence classes of certain
| pairs of integers; and to define real numbers as
| equivalence classes of Cauchy sequences of rational
| numbers. In each of these cases there is an obvious
| injection which we are used to regarding as inclusion,
| but most of mathematics is set up to make it meaningless
| even to _ask_ whether the natural number 1 is the same as
| the integer 1 is the same as ....
|
| That is to say, if you're working on an application where
| encoding details are important, then you can and will ask
| such questions; but if I am writing a paper about natural
| numbers, I do not have to worry about the fact that, for
| some choice of encoding, the number 2 = {[?], {[?]}} is
| the same as the ordered pair (0, 0) = {0, {0, 0}} = {[?],
| {[?]}}, and in fact it is meaningless to test whether 2
| "equals" (0, 0). The philosophy of studiously avoiding
| such meaningless questions leads some to avoid even
| testing for equality, as opposed to isomorphism; failing
| to do so used to be referred to in category-theoretic
| circles as "evil", although, as the nLab points out if
| you try to go to https://ncatlab.org/nlab/show/evil , it
| seems common nowadays to avoid such language.
| generationP wrote:
| This is not the point of the article. Even at the level
| of the objects themselves, 1 : integer is not 1 :
| rational. The latter is an ordered pair (1, 1) of two
| coprime positive integers, or an equivalence class of
| ordered pairs up to cancelling. Some ugly hackery is
| required to really make the integers _equal_ to their
| respective rationals, and its consequences aren 't great
| either (just imagine that _some_ rationals are pairs
| while others are not -- that 's what you get if you
| forcibly replace the rational k/1 by the integer k), and
| no one wants to do that.
| passion__desire wrote:
| All the examples of shadows mentioned by Douglas in the
| video [0]:
|
| Traditional Shadow from Sunlight: A tree casting a shadow
| in bright sunlight during the summer, characterized by the
| typical darkening on the ground.
|
| Snow Shadow: Occurs in winter when a tree intercepts
| snowflakes, resulting in an absence of snow under the tree
| despite being surrounded by snow. This is likened to a
| shadow because it mimics the visual absence typical of
| shadows, even though caused by a different kind of
| blockage.
|
| Rain Shadow: Explained with the example of the Cascade
| Mountains, where the mountains block rain clouds leading to
| dry conditions on the leeward side, effectively creating a
| "shadow" where rain is absent due to the geographical
| barrier.
|
| Car Shadow by a Truck: Described during highway driving,
| where a large truck casts a "shadow" by preventing cars
| behind it from passing. This "shadow" is the area in front
| of the truck where cars tend to stay clear due to the
| difficulty in passing the truck.
|
| Shadow Cast by England Due to the Gulf Stream: This is a
| metaphorical shadow, where England blocks the warm Gulf
| Stream from reaching certain areas, resulting in colder
| temperatures on one side, while allowing it to pass above
| to northern Norway, warming it. This is referred to as the
| "shadow of England" on the coast of Norway, influenced by
| the flow of water rather than light.
|
| These examples use the concept of "shadow" in various
| physical and metaphorical contexts, showing disruptions in
| different types of flows (light, snow, rain, traffic, and
| ocean currents) caused by obstructions.
|
| [0] : https://youtu.be/LnTVzB5S8m4?t=973
| LudwigNagasena wrote:
| Saying 1 is both an integer and a rational number is wildly
| different from saying it is both an integer and an ASCII
| character. Z is a subset of Q. ASCII characters don't
| overlap with either.
|
| When you construct numbers using sets under ZFC axioms or
| inside lambda calculus what you get is representation. But
| 1 is just 1.
| pitched wrote:
| Your keyboard has a button with '1' printed on it. When
| you push that, you don't always get an integer or a
| rational number. You can convert what you get to either.
| So there must be overlap with ASCII somehow?
| LudwigNagasena wrote:
| There is some overlap in some sense somehow, but not in
| any literal sense unlike in the sense in which all
| elements of Z are elements of Q.
| gerdesj wrote:
| There are multiple things that we denote using a particular
| symbol: 1. 1 in and of itself is not a single concept. You
| could replace the symbol 1 with any other, even the sound of
| a fart and the concepts still remain the same. Given that we
| somehow agree that a fart sound shall be the way that we
| refer to a concept/object/thing.
|
| It's a largely useful conceit to use 1 for all of those
| objects and more besides. It makes talking about them easier
| but we do have to be careful to use the correct rule-set for
| their manipulation.
|
| I would personally prefer to see 1.0 for "rational 1" or
| perhaps 1. but that would require a convoluted sentence to
| avoid 1. being at the end of the sentence, unless we allow
| for: 1.! Well, that would work but what about 1.? Oh for ffs,
| I mean: 1..
|
| One notes that one's own ones may not be the same as one's
| other ones.
|
| If only I could spin "won", "own" and perhaps "wan" into that
| last sentence! ... Right, I've wedged in own. Needs some work
| 8)
| reaperman wrote:
| > (i.e., it depends what order you go)
|
| At the risk of utterly derailing this with irrelevant
| discussion: path-dependent systems are particularly tricky for
| some people IMHO. I think in a more state-based way, and my
| first rigorous dive into path-dependent calculation was during
| my chemical engineering degree -- I learned to be extremely
| vigilant about memorizing what was path-dependent and triple-
| checking if that affected the situation I was calculating.
|
| I do wish there was more rigorous exposure to them at lower
| levels of education and younger age. Because while I'm
| perfectly capable of handling path-dependent systems with
| proper focus and effort, my brain doesn't feel "native" when
| deriving solutions around those spaces - it feels similar to
| being "fluent enough" in another language. I feel this way
| about a lot of things -- I really feel I'd have been happier
| and more fulfilled if I'd been immersed in super rigorous
| first-principles education beginning around age 8-9. I didn't
| do well with things like "memorize this procedure for doing
| long division" and did much better with conceptual derivations
| of physics/math/science/historical arcs, etc.
| generationP wrote:
| The problem is that no one thinks of type conversions as
| taking any explicit paths! It's one thing to view the actual
| process of long division as path-dependent (something
| everyone who learns about Grobner bases is familiar with, as
| at the right level of generality even the result is path-
| dependent); it's another thing to apply the same intuition to
| the way the inputs are parsed. (You said divide 3 by 2 with
| remainder? Sure, the quotient is 3/2 and the remainder is 0.
| Problem?)
| reaperman wrote:
| > _The problem is that no one thinks of type conversions as
| taking any explicit paths!_
|
| Indeed. This is super surprising to me and I'm adding the
| topic to my "study" list. I had no idea until today - I
| easily could imagine it's possible if some of the type
| conversions are "lossy" (e.g. maps to lists), but I have a
| strong feeling that simpified lossy conversions are not
| what is being referenced.
| zmgsabst wrote:
| Isn't that the intuition behind homotopy type theory --
| that equivalence is a path between types?
|
| (And related, eg, cubical type theory.)
| belter wrote:
| > Strictly speaking, the rational number 1 is not the same as
| the integer 1
|
| So does that mean you can have different 0 zero's ?
| lupire wrote:
| Yes
| zarzavat wrote:
| This doesn't sound right to me. The rational numbers are a
| superset of the integers. We know that there's only one 1 in
| the rational numbers, then it must be the same 1 object as the
| 1 in the integers.
|
| The statement "3/3 is in Z" is true. There's no conversion
| happening: 3/3 is a notation for 1, just like 0.999... is a
| notation for 1. Many notations, but only one 1 object.
|
| The case of R x R^2 = R^3 is different because the Cartesian
| product is _defined_ to produce a set of ordered pairs. So it
| cannot give rise to a set of triples any more than a dog can
| give birth to a cat. So either x is not a Cartesian product or
| = is isomorphism not equality.
| perforator wrote:
| Your statements such as
|
| > We know that there's only one 1 in the rational numbers,
| then it must be the same 1 object as the 1 in the integers. >
| The statement "3/3 is in Z" is true.
|
| make it sound very trivial while in reality it is not. I do
| not quite understand your example with R^3 but the _defined_
| applies equally to your statements. There are many ways to
| define and think about the objects you mentioned -- there is
| not one single truth. Unless you are a devoted platonist, in
| which case, it 's still like your opinion, man.
| AlecBG wrote:
| I'm not sure I agree. That sort of type conversion involves
| inclusions, while the examples Buzzard talked about involved
| isomorphisms
| types_vs_sets wrote:
| Inclusions are a form of isomorphism. In the more common
| developments of elementary arithmetic, Q is _constructed_
| from Z, and in particular the subset of integral rational
| numbers are technically a different ring from Z. The
| conversion Z \to Q in particular is an isomorphism from Z to
| that subset.
|
| Type conversions in every day programming languages though
| sometimes not only fail to be surjective, they can also fail
| to be injective, for example int32 -> float32.
|
| type-conversions and "implicit isomorphisms" differ because
| the former does not need to be invertible, but they agree in
| that they are implicit maps, that are often performed without
| thought by the user. So I think that the type-conversions
| analogy is pretty good in that it captures the idea that
| implicit conversions, when composed in different ways from A
| to B, can arrive at various values, even if each stage along
| the way the choices seemed natural.
| nyc111 wrote:
| 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 wrote:
| _up to (non-)unique isomorphism_
| mxmlnkn wrote:
| As far as I remember, that's not a problem in math:
|
| := definition [?] identity = equality [?] proportionality
| nyc111 wrote:
| But this is how it works:
|
| = definition = identity = equality = proportionality
| Twisol wrote:
| 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 wrote:
| 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 wrote:
| [x:y] = [lx:ly]
|
| and I suppose the model of localization discussed in the
| article above counts as well.
| yau8edq12i wrote:
| ... What? That's just symbol soup. What are you trying to
| write? Do it in latex if it helps.
| lupire wrote:
| "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/f...
|
| https://people.math.osu.edu/cogdell.1/6112-Mazur-www.pdf
| ajkjk wrote:
| 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 wrote:
| 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.
| ajkjk wrote:
| Yes, I know it's the meaning of it, but I'm saying that the
| presence of "units" allows you to sort of... operationalize
| it? In a way that removes the ambiguity about what's going
| on. Or like, in theory. I dunno it's a comment on the
| internet lol.
| yau8edq12i wrote:
| I think it's the first time that I witness this comic
| https://xkcd.com/793/ happening but with math as a target.
| mathgradthrow wrote:
| You use R^3 in your example of why coordinates don't matter.
| R^3 can be covered by _one_ chart. Maybe your argument would be
| more convincing if you pick a different manifold. I have no
| idea what your complaint is otherwise.
| ajkjk wrote:
| I'm not talking about charts of R^3; I'm talking about the
| different isomorphic constructions of products like ((a, b),
| c) and (a, (b, c)) as being a sort of 'choice of coordinate
| system' on the isomorphic class of objects.
| mathgradthrow wrote:
| yes, and these choices dont matter individually, but how
| these choices glue together does, in fact, depend on all of
| them collectively.
| rhelz wrote:
| This is a very old consideration (cf
| 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 wrote:
| 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
| yau8edq12i wrote:
| How can you frame a paper from 1965 as "very old" when the
| linked article is about Grothendieck, who started his math PhD
| in 1950 (and presumably studied math before that)?
| ysofunny wrote:
| 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
| hackandthink wrote:
| 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 wrote:
| "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.
| abeppu wrote:
| 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_umb...
| perihelions wrote:
| 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, x, -) 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 x R or R x
| 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 wrote:
| 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
___________________________________________________________________
(page generated 2024-05-20 23:00 UTC)