7
$\begingroup$

I'm looking for references on constructive Lie algebra theory, e.g. the sort of theory you could develop in Martin-Löf type theory or internal to some topos with a NNO. Obviously excluded middle is not allowed in this setting, but I'm willing to accept countable choice (though no stronger choice axioms).

So far, I've found a PhD thesis on this topic from 1990:

Merrin, S. D. (1990). Some constructive results in the theory of Lie algebras (Order No. 9029729). Available from ProQuest Dissertations & Theses Global. (303904437).

I'd also be happy to get some references on Lie algebras from a more computational perspective (even if the author doesn't explicitly use constructive foundations).

Improve this question
$\endgroup$
8
  • 3
    $\begingroup$ 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. $\endgroup$
    – darij grinberg
    Commented Jun 5, 2023 at 23:24
  • 1
    $\begingroup$ (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.) $\endgroup$
    – darij grinberg
    Commented Jun 5, 2023 at 23:25
  • 1
    $\begingroup$ @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? $\endgroup$
    – ಠ_ಠ
    Commented Jun 6, 2023 at 23:00
  • 1
    $\begingroup$ @ಠ_ಠ 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.) $\endgroup$
    – Gro-Tsen
    Commented Jun 7, 2023 at 7:46
  • 1
    $\begingroup$ (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?). $\endgroup$
    – Gro-Tsen
    Commented Jun 7, 2023 at 7:50

0

Reset to default

You must log in to answer this question.