Einstein notation

Stream: general

[Joseph Tooby-Smith]

High energy physicists (and others) have a tendency to use Einstein notation.

An important part of Einstein notation is the ability to have subscript and superscript greek indices. I.e. for a matrix $\eta$, then $\eta_{\mu\nu}$ corresponds to the $(\mu, \nu)$-element of the matrix $\eta$. Furthermore, $\eta^{\mu\nu}$ corresponds to the $(\mu, \nu)$-element of the matrix $\eta^{-1}$.

There is more to Einstein notation. But I was wondering if anyone had an idea of how to implement these basic parts into Lean?

[Henrik Böving]

In general getting arbitrary super and subscript symbols is non trivial. UTF-8 does not even specify all numerals to have super and subscript versions, let alone greek things. So whatever you are goin to do to get there will either be a horrible hack, or will have to make compromises on the recognizability of the notation from paper.

[Joseph Tooby-Smith]

Ok, thanks. In that case, the latter route seems like the only feasible one.

[Joseph Tooby-Smith]

This is the best I could come up with:

notation "η⁽" mu "⁾⁽" nu "⁾"   => η mu nu

notation "η₍" mu "₎₍" nu "₎"   => η⁻¹ mu nu

[Eric Wieser]

Note that the horrible hack exists in mathlib already, as

macro "η⁽" mu:superscript(term) "⁾⁽" nu:superscript(term) "⁾"  : term  => η mu nu

[Utensil Song]

Related discussion here.

[Joseph Tooby-Smith]

Thanks for sharing this. Though, I don't think this lets me do exactly what I want, since e.g. $\mu$ and $\nu$ (as greek letters) don't appear in Mapping.superscript. I think it will let me do e.g. $\eta^{01}$ etc. for specific values of the indices.

[Kevin Buzzard]

Mathematicians have been spoilt by LaTeX. Unicode, whilst better than all the ascii <= stuff we see in earlier proof assistants, is still at the end of the day a very poor substitute. I would love to see some kind of magic button we can press which makes some part of the infoview or something look like LaTeX. Is this something which could one day be viable @Patrick Massot ?

[Patrick Massot]

Yes this is doable but requires engineering work.

[Eric Wieser]

https://github.com/kmill/LeanTeX is part of the story, I imagine

[Utensil Song]

At the core of the solution is a mechanism to declare how a notation or a plain definition is shown, parallel to delab. A little like Typst's show.

[Mr Proof]

A few points:
(1) Mostly you can get away with just using covariant form of tensors. e.g. Riemann tensor with all indices lowered. You could assume that the contracting of two covariant tensors involves contraction with the metric. That's one way to avoid mixed indices
(2) Some systems use notation such as A[3][4][-2][-4] with negative signs to indicate raised tensors. (Not that this is very nice)
(3) In my spare time I am working on a nice latex like interface for Lean which would display nice equations but run Lean underneath. If you have a wishlist of requests of what features you would like let me know.

[Utensil Song]

Joseph Tooby-Smith said:

This is the best I could come up with:

notation "η⁽" mu "⁾⁽" nu "⁾"   => η mu nu

notation "η₍" mu "₎₍" nu "₎"   => η⁻¹ mu nu

In retrospect, this is actually a better direction if with a slight modification to use these parentheses to indicate sup/sub, so one can write η⁽a b⁾₍c₎⁽d⁾ to mean $\eta^{ab}_{\phantom{oo}c}{}^{d}$ where a b c d could be symbols or specific values. But the layout is just poor.

One will need to write a small DSL syntax to cover this, or better, η^{a b}_{c}^{d} which mimics LaTeX but I'm tempted to use brackets i.e. η^[a b]_[c]^[d].

[Joseph Tooby-Smith]

I agree, I think the notation: η^[a b]_[c]^[d] is the best here.

[Joseph Tooby-Smith]

As a follow on to this discussion: I now have the basics of a general theory of index notation in HepLean here.

The underlying theory, which is based on modular operads, is (I believe) be general enough to cover ordinary Einstein notation, index notation for Lorentz tensors, and Van der Waerden notation, etc... In the case of index notation for Lorentz tensors, it is possible to write e.g. T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃" for the tensors and the contraction their indices (where e.g. T|"ᵤ₁ᵤ₂" is a tensor and ⊗ᵀ is notation for the tensor product).

I plan to write something more detailed up on this, when I have made explicit examples of its use.

[Igor Khavkine]

Just thought that it was worth mentioning it explicitly, though Mr Proof alluded to this convention earlier. There is the quite well established Mathematica package xAct for tensor computations (especially designed for manipulating abstract indices). Its preferred notation is T[a,b,-c,d], where a - indicates a covariant (down) index and no sign indicates a contravariant (up) index.