PR !4#9111: feat(LinearAlgebra/CliffordAlgebra): port Spi...

Stream: triage

[Random Issue Bot]

Today I chose PR 9111 for discussion!

feat(LinearAlgebra/CliffordAlgebra): port SpinGroup
Created by @Utensil (@utensil) on 2023-12-16
Labels: awaiting-review

Is this PR still relevant? Any recent updates? Anyone making progress?

[Utensil Song]

The PR review was previously discussed in a thread named "#16040 Spin Group" borrowing the old thread from the mathlib3 PR, and its review and progress paused quite a while since the new year, and it's back alive thanks to @Eric Wieser 's review comments and some commits, and now I'm back at it too.

I wonder the difference between triage and PR reviews, should the long discussion go back to the old thread and this is literally just triage?

[Johan Commelin]

Yes, that's right

[Johan Commelin]

This stream is just so that a bot reminds us that we shouldn't forget a certain pr

[Eric Wieser]

Scott Carnahan said:

It's been more than a month since the last bot post. Who should we call?

I think this is probably between you and me; I think this is probably almost ready to go, but:

• I wanted to leave some notes about using subgroups vs sub monoids (initially I proposed changing this but I think it's not so clear a win as I'd hoped, and want to write down why)
• I think we should make sure to capture some of the confusion that you outlined in your answer to my mathoverflow question a year or so ago; even if we just refer to it and explain which choice we picked.

[Eric Wieser]

Oh, you mean since any bot post in this stream

[Utensil Song]

Sorry that I missed this message. I DMed you about my thoughts on subgroups vs sub monoids, now I'm looking forward to your notes about why.

My takeaway on https://mathoverflow.net/a/457323/489031 is that sources mentioned other than the Wikipedia definition are assuming more than explicitly spelled out, thus invalid.

[Scott Carnahan]

The section about spin and pin groups in the Wikipedia article on Clifford algebras was primarily written by Richard Borcherds, who seems to have spent a lot of time trying to get spinors to work right.

[Random Issue Bot]

Today I chose PR 9111 for discussion!

feat(LinearAlgebra/CliffordAlgebra): port SpinGroup
Created by @Utensil (@utensil) on 2023-12-16
Labels: awaiting-author, new-contributor

Is this PR still relevant? Any recent updates? Anyone making progress?

[Utensil Song]

I think the PR is ready to merge if the submonoid approach is acceptable.

I was thinking about working out the subgroup approach in Lean for comparison, but yet to find time to do that.

In the meanwhile, I have some note drafts about the definitions of Spin groups ( Web , PDF ).