definition of `is_nilpotent`

Stream: maths

[Kevin Buzzard]

I knocked off a basic theory of nilpotent groups yesterday because I was talking about possible projects with an undergraduate and this was one (I thought I'd start them off). But the linter informs me that my predicate is_nilpotent on groups in the root namespace clashes with the predicate is_nilpotent on elements of rings (or more generally monoids with zero) also in the root namespace. Such is life -- but what do I do? Define group.is_nilpotent? The word nilpotent certainly means several (related, but not equal) things in mathematics.

[Oliver Nash]

Sorry, I put is_nilpotent into the global namespace! For what it's worth, I face the Lie algebra variant of your group problem and I just rely on namespacing lie_algebra.is_nilpotent.

[Kevin Buzzard]

OK I'll put this stuff in the group namespace. Thanks!

[Damiano Testa]

I am not sure if this is a good idea, but could is_nilpotent be the to_additive version of is_unipotent? In my mental picture, this captures most of the meaning of "unipotent/nilpotent", at least when applied to individual elements.

This would also go well with a unipotent/nilpotent matrices.

[Kevin Buzzard]

I think you're talking about nilpotent elements not nilpotent groups, and I think what you're suggesting will run into the issue that r^n=1 will be translated by to_additive as n \bub r = 0 rather than r^n=0 :-)

[Damiano Testa]

Yes, I was indeed thinking about individual elements. Also, you are right about the pow/smul issue. I know that Floris has been updating to_additive, but I do not know if he tried to make this work as well...

[Kevin Buzzard]

I believe that he got it working fine!

I guess I mis-spoke -- I don't think r^n=1 is relevant here. What does unipotent mean to you? Do you just mean (r-1)^n=0? I am not sure that to_additive should be translating between nilpotent and unipotent elements, I think the relationship is more subtle. to_additive is performing the blanket isomorphism between group theory set up $\times$ and group theory set up with $+$. The relationship between unipotent and nilpotent seems to me to be something to do with the much more subtle relationship between them, namely via exp and log, where these things are often not isomorphisms, but rather local isomorphisms where the interest is in higher-order effects (e.g. the Lie bracket comes from failure of commutativity of multiplication, pushed into an additive world via exp rather than by to_additive, and my feeling about the relationship between unipotent and nilpotent elements is that it's of a similar flavour.)

[Damiano Testa]

I think that you are right, Kevin: in my mind, I was thinking of to_additive as a magic wand that would convert anything multiplicative to anything additive, e.g. using exp/log when needed.

My wishful thinking came about precisely because you mentioned nilpotency in the context of groups and right after, it was pointed out that there is nilpotency for Lie algebras. Thus, I got to thinking: could the conversion between Lie groups and Lie algebras be automated (at least somewhat)? And my mind very happily said "there already is to_additive"!

I guess that there is the need for a to_lie_algebra tactic...