search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

Geometric Algebra #5059

Open jfcg opened 3 years ago

jfcg commented 3 years ago

According to Prof. Alan Macdonald's page GA:

... and its extension to geometric calculus unify, simplify, and generalize vast areas of mathematics that involve geometric ideas, including linear algebra, multivariable calculus, real analysis, complex analysis, and euclidean, noneuclidean, and projective geometry. They provide a unified mathematical language for physics (classical and quantum mechanics, electrodynamics, relativity), the geometrical aspects of computer science (e.g., graphics, robotics, computer vision), and engineering.

According to the Macdonald's page and wikipedia's article, GA provides natural representations to geometric objects and operations on those objects. For example it naturally accomodates complex and quaternion number systems.

I know mathlib is at a preliminary stage and I'm no expert but using it from initial stages of mathlib development could bring quite a lot simplifications and new horizons, including a good base for physical mathematics (quite in the future possibly).

Is there any plan to use/introduce GA in mathlib? Thanks..

jcommelin commented 3 years ago

@eric-wieser has been working on this.

eric-wieser commented 3 years ago

I gave an introductory presentation on lean and it's application to GA at ICCA 2020, recorded here: https://m.youtube.com/watch?v=DX2n_-MD-A4

Since that conference, @utensil and I now have clifford_algebra Q in Mathlib, but not much else. I've built some stuff on top of that at https://github.com/pygae/lean-ga/pull/13, but it's currently short the wedge and contraction products, without which it's obviously of limited use to GA.

eric-wieser commented 3 years ago

For example it naturally accomodates complex and quaternion number systems.

As of very recently, these two facts are now in mathlib!

eric-wieser commented 2 years ago

While its content is somewhat outdated, the paper corresponding to the ICCA talk is now published at https://link.springer.com/article/10.1007/s00006-021-01164-1. I strongly recommend not reading in-browser, springer have truly butchered the typesetting. The PDF is fine.