4 ms·

How is constructive mathematics closer to Lie groups than regular mathematics? From what I read in that presentation, a bunch of basic assumptions in calculus (

by joppy 8y ago

How is constructive mathematics closer to Lie groups than regular mathematics? From what I read in that presentation, a bunch of basic assumptions in calculus (such as the intermediate value theorem) no longer hold, and the theory of Lie groups is built on manifolds/calculus/real analysis etc.

adamnemecek 8y ago
Good question. I don’t have a direct answer answer but fundamentally the connection has something to do with adjoints. Google for adjoints and constructive mathematics and Lie groups and adjoints. This particular pair I understand only indirectly, I somewhat understand the relationship between linear logic and Lie groups and constructive mathematics and linear logic and this is a transitive relationship. Edit: in the presentation they mention “In constructive mathematics, there can also be numbers† d such that d^2 = 0 but not necessarily d = 0.”. They are talking about alternarivity, one of the three requirements for a Lie algebra https://en.m.wikipedia.org/wiki/Lie_algebra https://en.m.wikipedia.org/wiki/Lie_algebra
- joppy 8y ago
  “Something to do with adjoints” is hopelessly vague, and what do you mean by transitive? In regular mathematics there can be nonzero numbers whose square is zero (for example, the “dual numbers”). But I don’t see how this has anything to do with constructive vs nonconstructive mathematics.
  - adamnemecek 8y ago
    > hopelessly vague, You didn’t do the reading so hold your horses with hopelessly. From the slides “In constructive mathematics, every function is continuous”. (From the presentation) Sounds like Lie groups to me. I’m aware of dual numbers funny that you bring them up as they correspond to Lie groups. I have been talking about dual quaternions nonstop on hn.
    - mikorym 8y ago
      I'm sorry, but he is right. Adjoints are everywhere [1]. Referencing adjoints is indeed pretty vague. You can't make a case for why things are interesting by quoting a bunch of resources of other people making cases why things are interesting. (I guess you can, but then, why make the argument at all if it is not yours?) You don't even need funny names to get x^2=0. This is true for any of the two elements of the group of order 2. Linear logic is indeed having a mini revival, but so is general category theory. I don't see the particular advantage for people to evangelise certain parts of mathematics, especially if the case being made is not clear. [1] Not attributed to me.
      - adamnemecek 8y ago
        > I'm sorry, but he is right. That’s like your opinion, man. You conveniently ignored the continousness of both constructive mathematics and Lie groups. Did you read the paper on chu spaces and constructive mathematics? What did it say about adjoints?
- eastWestMath 8y ago
  There’s a reason why intuitionistic logic comes into studying Lie Groupoids, but I’m not quite sure you understand why. It’s great to see some enthusiasm, but I’d recommend spending a few months working through Barr and Wells before you start publicly advocating like this.
fmap 8y ago
Lie groups come up very naturally in synthetic differential geometry (SDG) (http://www.fuw.edu.pl/~kostecki/sdg.pdf http://www.fuw.edu.pl/~kostecki/sdg.pdf). In fact, the main advantage of SDG over the classical formulation of differential geometry is that it can be developed in a largely coordinate free fashion and that you can talk natively about differential forms. That said, there is a design space here and while SDG is close enough to ordinary mathematics that you can explain it to high-school students, it might not be the best fit for developing modern physics. There are several different approaches (e.g., working in the internal language of a "synthetic differential infinity-topos") which seem promising. It's an area of active research and one that is still extraordinarily difficult to get into.
- joppy 8y ago
  Does this have anything to do with constructive mathematics though? I still don’t see the connection.
  - fmap 8y ago
    These are all models of a constructive type theory/intuitionistic logic. The axiom of excluded middle fails in SDG and in any infinity-topos.
thrwyioio 8y ago
Is there a constructive version of Gleason and Montgomery-Zippin solution of the Hilbert 5th problem? Reference pls if any.

by joppy 8y ago

adamnemecek 8y ago

Good question. I don’t have a direct answer answer but fundamentally the connection has something to do with adjoints. Google for adjoints and constructive mathematics and Lie groups and adjoints. This particular pair I understand only indirectly, I somewhat understand the relationship between linear logic and Lie groups and constructive mathematics and linear logic and this is a transitive relationship. Edit: in the presentation they mention “In constructive mathematics, there can also be numbers† d such that d^2 = 0 but not necessarily d = 0.”. They are talking about alternarivity, one of the three requirements for a Lie algebra https://en.m.wikipedia.org/wiki/Lie_algebra https://en.m.wikipedia.org/wiki/Lie_algebra

joppy 8y ago
“Something to do with adjoints” is hopelessly vague, and what do you mean by transitive? In regular mathematics there can be nonzero numbers whose square is zero (for example, the “dual numbers”). But I don’t see how this has anything to do with constructive vs nonconstructive mathematics.
- adamnemecek 8y ago
  > hopelessly vague, You didn’t do the reading so hold your horses with hopelessly. From the slides “In constructive mathematics, every function is continuous”. (From the presentation) Sounds like Lie groups to me. I’m aware of dual numbers funny that you bring them up as they correspond to Lie groups. I have been talking about dual quaternions nonstop on hn.
  - mikorym 8y ago
    I'm sorry, but he is right. Adjoints are everywhere [1]. Referencing adjoints is indeed pretty vague. You can't make a case for why things are interesting by quoting a bunch of resources of other people making cases why things are interesting. (I guess you can, but then, why make the argument at all if it is not yours?) You don't even need funny names to get x^2=0. This is true for any of the two elements of the group of order 2. Linear logic is indeed having a mini revival, but so is general category theory. I don't see the particular advantage for people to evangelise certain parts of mathematics, especially if the case being made is not clear. [1] Not attributed to me.
    - adamnemecek 8y ago
      > I'm sorry, but he is right. That’s like your opinion, man. You conveniently ignored the continousness of both constructive mathematics and Lie groups. Did you read the paper on chu spaces and constructive mathematics? What did it say about adjoints?
eastWestMath 8y ago
There’s a reason why intuitionistic logic comes into studying Lie Groupoids, but I’m not quite sure you understand why. It’s great to see some enthusiasm, but I’d recommend spending a few months working through Barr and Wells before you start publicly advocating like this.

fmap 8y ago

Lie groups come up very naturally in synthetic differential geometry (SDG) (http://www.fuw.edu.pl/~kostecki/sdg.pdf http://www.fuw.edu.pl/~kostecki/sdg.pdf). In fact, the main advantage of SDG over the classical formulation of differential geometry is that it can be developed in a largely coordinate free fashion and that you can talk natively about differential forms. That said, there is a design space here and while SDG is close enough to ordinary mathematics that you can explain it to high-school students, it might not be the best fit for developing modern physics. There are several different approaches (e.g., working in the internal language of a "synthetic differential infinity-topos") which seem promising. It's an area of active research and one that is still extraordinarily difficult to get into.

joppy 8y ago
Does this have anything to do with constructive mathematics though? I still don’t see the connection.
- fmap 8y ago
  These are all models of a constructive type theory/intuitionistic logic. The axiom of excluded middle fails in SDG and in any infinity-topos.

thrwyioio 8y ago

Is there a constructive version of Gleason and Montgomery-Zippin solution of the Hilbert 5th problem? Reference pls if any.