Should (some of) Lie theory import algebraic geometry?

Stream: mathlib4

[Calle Sönne]

I want to try to formalize the fact that all cartan subalgebras in a lie algebra (over a char 0 alg cl. field) are conjugate (see also project).

One very clean approach, lecture_9 uses input from algebraic geometry (which is proven directly in that file). The proof is very direct, and apart from making this AG input work, I expect it to be very short. For the AG input, one could even prove it by invoking more high-powered AG theorems about smoothness (jacobian criterion and the rank theorem). We do not currently have these in mathlib, but since people are working on smoothness these are hopefully not too far away, and I'm guessing it will take me some time to formalize the glue for treating vector spaces as schemes anyways. This approach would be the most satisfying to me "math-wise". However, maybe there is an issue with importing a possibly large amount of AG (smoothness + dependencies) into lie theory.

There is also a proof (in Humphreys) which doesn't use any AG. However, that proof is considerably more convoluted, and will be significantly longer (but probably shorter in total if one counts all the needed AG imports of the other proof).

So I have 3 options for formalizing this statement about Lie algebras:

1. Go with the very long and convoluted Humphreys proof (which is a purely Lie theoretic proof)
2. Go with the AG approach, but try to minimize AG imports by proving the AG statement myself as in the file (although in the end it might be quite painful to develop the theory in this special case, so maybe this option is also not the best).
3. Go with the AG approach + use high-powered theorems. This will make the proof itself the shortest, but it will have the most imports. It will also make the proof the most readable.

What do people think about this? Is there a big drawback with having some of Lie theory depend on AG, and are there good reasons to go through the pain of avoiding this? Or can I just go with the most high-powered and import-heavy proof?

(cc @Oliver Nash @Johan Commelin )

[Kevin Buzzard]

My instinct is that if alg geom can be used to do something useful here then go for it and import as much as you need! I'm a bit unclear about the motivations of the minimise-imports crowd though.

[Oliver Nash]

I only have a moment for a quick remark as I'm working today but I would mostly ignore any "heavy import" considerations.

For me the main thing is always to have the most general (or at least generalisable) statement / proof. For example, it would certainly be a huge step forward for Mathlib's Lie theory if we got this result only for algebraically-closed fields but one day we might want results for the non-algebraically-closed case so one might prefer a proof for which algebraic closure factors in later. (I have to admit that I'm not really clear on the statement here and for all I know the real case is best dealt with by complexifying anyway.)

Once you're in a situation where you're proving the result at the "right" level of generality I think the next most important thing is to do it in the conceptually nicest way. I think most of the time I'd rather an import-heavy proof that uses the right techniques.

But really it's up to you: I'd be delighted to see any proof of this result land in Mathlib!

[Matthew Ballard]

I worry that Lie theory will grind to a halt on your machine with this because AG imports almost everything and Lie theory is already quite slow.

[Ruben Van de Velde]

As long as you put it in a new file, import whatever makes sense. (But maybe add a note that a less high-powered proof is available, in case it would become a problem in the future.)

[Matthew Ballard]

Yes, I would say: definitely do it, but quarantine it as Ruben suggested. I am curious as to the effects.

[Damiano Testa]

Also, if the jacobian criterion can only be used within algebraic geometry, I think that there are other issues that need to be addressed...

[Calle Sönne]

Okay thanks everyone! I will start working on the AG-heavy approach then.

[Calle Sönne]

Damiano Testa said:

Also, if the jacobian criterion can only be used within algebraic geometry, I think that there are other issues that need to be addressed...

Yes and not being able to import Lie theory and AG simultaneously would also be a general issue for e.g. the theory of algebraic groups

[Antoine Chambert-Loir]

Matthew Ballard said:

I worry that Lie theory will grind to a halt on your machine with this because AG imports almost everything and Lie theory is already quite slow.

Of course, such an issue does not need to be resolved within a week, but I worry how a proof of Fermat's Last Theory will be at all possible in lean if Algebraic Geometry, Lie Theory, Number Theory, Differential Geometry and Spectral Theory can't be imported simultaneously.

[Kim Morrison]

Neither Lie theory nor algebraic geometry are involved in Mathlib's current longest pole, so I don't think there's anything to worry about for now.

[Kim Morrison]

Follow the maths!

[Oliver Nash]

Matthew Ballard said:

Lie theory is already quite slow.

Is there a way for me to see this in Speedcenter or somewhere? (I never really notice slowness but then I have a fast laptop.)

[Matthew Ballard]

Not easily. You can glean facts like: Lie theory accounts for 2-3% of the 200 largest by instruction files while being .8% of the overall library. I think that would be even worse if you weight number of lines in the file.

[Oliver Nash]

OK well I'd be happy to help with speed issues in this part of the library if they ever become problematic.