Formalisation of Lie algebras in other languages

Stream: general

[Oliver Nash]

I'm considering writing something about Mathlib's formalisation of Lie algebras and so I'd like to learn more about the prior art.

I'm really looking for other instances of (computer) formalisation of Lie algebras. So far I have not found any.

The closest matches I have found are distant, for example:

• a Coq program that carries out case analysis on data related to Lie algebra representations
• some fascinating slides by Bill Casselman that are vaguely related
• a Coq library for robotics

Of course I have looked in places such as:

• https://www.isa-afp.org/search.html
• https://github.com/math-comp/math-comp/
• https://github.com/UniMath/UniMath/
• https://github.com/metamath/set.mm

More generally, I'd be grateful for guidance on how to search the literature. I feel a bit lost not being able to rely on MathSciNet (Math Reviews). Are there particular conferences / journals I should check or people I should ask?

[Yakov Pechersky]

The links are broken, unfortunately. I think you've swapped the link text and URL.

[Oliver Nash]

Just testing of anyone was watching ;-)

[Oliver Nash]

I wonder if @Cyril Cohen might know?

[Johan Commelin]

Ooh, that first one is really interesting! But it's completely axiomatic, afaik.

[Johan Commelin]

The second one isn't about formalisation, right?

[Oliver Nash]

No, it's not really. But I liked it too much not to mention it.

[Oliver Nash]

The first one is this paper, and is indeed very interesting: https://arxiv.org/abs/1806.00347

[Johan Commelin]

The third one has a definition, as opposed to the axiomatic approach of the first. But I think it quickly specialises to an example, and does not develop Lie theory further. Cyril, please correct me if I'm wrong.

[Oliver Nash]

That's exactly what I see too.

[Cyril Cohen]

@Oliver Nash you found every piece of development I know is related to Lie algebras in Coq...

[Cyril Cohen]

Unfortunately...

[Oliver Nash]

Thanks for such a swift reply Cyril!

[Jason Rute]

I assume you only mean formal theorem proving, but another interpretation is any computer implementation of Lie algebras. It agents to have been implemented in GAP and Magma. (This is just from Googling. I don’t even know the definition of a Lie algebra, so my answer isn’t too informed.)

[Scott Morrison]

I wrote an ancient Mathematica package for dealing with quantum groups (quantised enveloping algebras, and explicit models for the intertwiners between finite dimensional reps, and braid representations). I think it was only ever used by other people inside the KnotTheory package written by Dror (and in part me) available from http://katlas.org/.

However there's essentially no documentation, and nothing to cite. :-)

There are a few other packages for doing calculations inside Lie algebras and/or quantum groups (or their reps) as add-ons for various computer algebra systems.

[Oliver Nash]

Thanks Scott, Katlas itself (new to me) is awesome.

[Oliver Nash]

Jason Rute said:

I assume you only mean formal theorem proving, but another interpretation is any computer implementation of Lie algebras. It appears to have been implemented in GAP and Magma.

Thanks Jason, I had seen mention of these and though they are different to what I've been doing, I'm still interested.

[Oliver Nash]

I now have a draft article waffling on about my work on Lie algebras and I'd be grateful for feedback / corrections etc. Any remarks most welcome.

[Oliver Nash]

report.pdf

[Yakov Pechersky]

This is awesome! First nit: I'd use unfreezingI { obtain ... } instead of tactic.unfreezing_local...

[Eric Wieser]

The acknowledgements section has a typo in the word acknowledge :). The section on the choice of axioms is nice; although it makes me wonder whether it makes sense to have right- or bi- lie modules.

[Oliver Nash]

LOL, of all the places to have a spelling mistake!

[Oliver Nash]

The point about left- / right- / bi- modules occurred to me too but I left it out to avoid confusion.

[Oliver Nash]

(well not exactly confusion but there's enough going on)

[Eric Wieser]

I agree that you don't need to open that can of worms to make that paper interesting, there's enough there already

[Eric Wieser]

Footnote 5 seems to refer to a PR link that didn't make it to the PDF. Perhaps a hyperref misconfiguration?

[Oliver Nash]

Yakov Pechersky said:

This is awesome! First nit: I'd use unfreezingI { obtain ... } instead of tactic.unfreezing_local...

Thanks for this, I agree. On the other hand tactic.unfreezing_local... is currently how this looks in master.

[Eric Wieser]

Well if you end up publishing master will look entirely different by the time you're done anyway, most likely.

[Yakov Pechersky]

You might not even need unfreezing if you say "obtain ... := id h"

[Oliver Nash]

I guess I could PR this change. On this point, I don't actually understand this beyond the syntactical difference. Do unfreezingI and tactic.unfreezing_local behave differently in any way, e.g., maybe the former purges less cache?

[Yakov Pechersky]

Unfreezing is needed because you're destroying something that was in the typeclass instance cache. But if you "clone" the hyp via "id", you might not need to. Untested, just guessing

[Yakov Pechersky]

No, they're precisely the same.

[Oliver Nash]

Yakov Pechersky said:

Unfreezing is needed because you're destroying something that was in the typeclass instance cache. But if you "clone" the hyp via "id", you might not need to. Untested, just guessing

Interesting, I'll try this out!

[Yakov Pechersky]

For the end user. UnfreezingI does return to the the original cache state after the end of the block

[Oliver Nash]

Oh wow, what a neat trick. You're right; this works:

  obtain ⟨k, hk⟩ := id hI,
  obtain ⟨l, hl⟩ := id hJ,
  exact ⟨⟨k+l, lie_ideal.derived_series_add_eq_bot hk hl⟩⟩,

[Oliver Nash]

Is that acceptable style?

[Oliver Nash]

Maybe obtain could be taught to do this?

[Eric Wieser]

This isn't always the right behavior for obtain though; sometimes you want to substitute hI in the goal and other hypotheses too, which is what happens without id.

[Yaël Dillies]

I personally use obtain ... := id ... to destruct hypotheses without clearing them. Useful trick in general.

[Eric Wieser]

Another option is just to use let in term mode instead of obtain. For the proof in question (src#lie_algebra.is_solvable_add) that golfs away the entire tactic component!

[Eric Rodriguez]

That was a nice read :)

[Eric Rodriguez]

If you're trying to make it beginner friendly, I personally found 4 the most challenging section to read, but otherwise very understandable

[Eric Wieser]

Looking at the lemmas about is_solvable R J... I almost wonder if the proofs would be easier as has_solution R J k or solution R J : Type, and then you don't have to pull apart exists every time (see: docs#invertible vs docs#is_unit vs docs#units, respectively, or docs#has_sum vs docs#summable vs docs#tsum). Perhaps it's never useful to know the value of k though.

[Eric Wieser]

Which isn't to say anything needs changing, but just that this is yet another opportunity to describe a design decision if you wanted too!

[Oliver Nash]

Thanks @Eric Rodriguez , @Eric Wieser, @Yakov Pechersky , and @Yaël Dillies All of this feedback is very useful and much appreciated.