Geometric Algebra

[jfcg]

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]

@eric-wieser has been working on this.

[eric-wieser]

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 pygae/lean-ga#13, but it's currently short the wedge and contraction products, without which it's obviously of limited use to GA.

[eric-wieser]

For example it naturally accomodates complex and quaternion number systems.

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

[eric-wieser]

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.