Timeline for Constructive theory of Lie algebras
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 7, 2023 at 8:20 | comment | added | ಠ_ಠ | @Gro-Tsen To be honest, I'm happy with whatever I can get. There just isn't much that I could find out there. Ideally, the development would be done with commutative rings if possible, and specializing to fields of the appropriate sort if necessary. This is just for my personal interest---I'm not working on a paper on this topic. | |
| Jun 7, 2023 at 7:50 | comment | added | Gro-Tsen | (contd.) But in any case, my comment was not to answer your question, it was to ask you to clarify what the base ring or field would be, which is at least as important as the ambient logic. If you want something over an arbitrary commutative ring, you should at least first inquire as to what is known classically over an arbitrary commutative ring. If you want something over a field, you should clarify which constructive flavor of “field” you mean (any Heyting field? a discrete field? or a specific one like the reals or a finite field?). | |
| Jun 7, 2023 at 7:46 | comment | added | Gro-Tsen | @ಠ_ಠ In one direction, because the constructive results would apply to the structural sheaf in the Zariski or étale (say) topos over a scheme. In the other direction, there is no automatic reason, but algebraic-geometric results and constructions which apply to such a topos tend to be valid in any ringed topos. See, e.g., Ingo Blechschmidt's thesis for a start if you're not aware of this. (contd.) | |
| Jun 6, 2023 at 23:00 | comment | added | ಠ_ಠ | @Gro-Tsen I'm not sure I follow: how can working constructively produce the same results as working with LEM and AC for Lie algebras over a commutative ring? | |
| Jun 6, 2023 at 11:17 | comment | added | Gro-Tsen | Over what base field/ring? I suspect that if you want something over an arbitrary commutative ring, the constructive setup doesn't change anything because algebra working classically over a commutative ring (or scheme) is essentially done in the topos of sheaves over it. (So maybe this question is a place to start.) And at the other extreme, for finite fields, the theory is purely combinatorial anyway. | |
| Jun 6, 2023 at 2:53 | history | edited | ಠ_ಠ | CC BY-SA 4.0 |
added 26 characters in body
|
| Jun 6, 2023 at 2:52 | comment | added | ಠ_ಠ | @darijgrinberg I'm looking for anything that's out there, really. For example, a constructive proof of Ado's theorem would be nice. | |
| Jun 5, 2023 at 23:25 | comment | added | darij grinberg | (If I'm not mistaken, Nathan Jacobson's papers from the 1940s/50s actually develop representation theory over an arbitrary char-$0$ field without eigenvalues.) | |
| Jun 5, 2023 at 23:24 | comment | added | darij grinberg | What parts are you looking at specifically? The formal theory and the theory of free Lie algebras are mostly constructive already (well, you probably need a total ordering on the basis for Lyndon words, and likely much more for Nielsen-Schreier). Coxeter-type Lie algebras are also pretty constructive (you need some cyclotomic extensions of $\mathbb Q$ to build their geometric representation, but that's easy to construct). Finite-dimensional representation theory is often done using eigenvalues over $\mathbb C$, but you can likely reduce it to finite extensions of $\mathbb Q$ as well. | |
| Jun 5, 2023 at 23:03 | history | asked | ಠ_ಠ | CC BY-SA 4.0 |