Derivations on Lie algebras

Stream: mathlib4

[Frédéric Marbach]

Hi, I am new to formalization and Lean, and my long term goal is to formalize some of my current research results on control theory. With this goal in mind, I plan to start by contributing to mathlib4 by formalizing some of the prerequisites that I need.

In particular, I intended to start by proving that Hall sets (of the free magma over a set X) yield bases of the free Lie algebra over X (see e.g. Free Lie Algebras by Bill Casselman). From the mathematical point of view, this is standard stable material dating from the 1970s and the proofs are rather straightforward. The proofs that I know of require manipulating derivations on Lie algebras (e.g. a linear map from a Lie algebra L to itself, satisfying Leibniz's law).

As discussed in this thread, the current definition of derivations in mathlib4 only works for commutative algebras, so doesn't apply to Lie algebras.

• On the one hand, I understand from the given thread that the proper refactoring with a generalization covering all possible settings for derivations might be complicated (and out of reach for me).
• On the other hand, the definition in the case of Lie algebras is probably simpler and I only need rather basic stuff about these derivations (say for example that the set of derivations of a Lie algebra is itself a Lie algebra).

How does the mathlib4 community approach such cases: do I need to wait for the long-term proper refactoring of derivations to include the non-commutative non-associative case? or could I follow the following plan:

1. State in mathlib4 a definition specific to Lie algebras, for example along the lines (please do correct me)

structure LieDerivation (R : Type*) (L : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
  extends L →ₗ[R] L where
  leibniz (a b : L) : toLinearMap ⁅ a, b ⁆ = ⁅ toLinearMap a, b ⁆ + ⁅ a, toLinearMap b ⁆

2. Prove in mathlib4 the basic facts that I need for such derivations of a Lie algebra to itself (e.g. they are themselves a Lie algebra).
3. Use these facts to prove in mathlib4 Viennot's theorem that Hall sets yield bases of the free Lie algebra.
4. One day, when the generalized definition becomes available, LieDerivation just becomes a kind of alias for the particular case of a derivation from a Lie algebra to itself, and we throw away the proofs of Step 2, since they now directly follow from the general case (and/or we also throw away the definition from Step 1, relying directly on the generalized notion).

Thanks for you thoughts

[Yaël Dillies]

cc @Oliver Nash

[Oliver Nash]

I am travelling so I will not be able to answer this properly till Monday. For now I’ll just say that I think your plan is probably the right way forward.

[Oliver Nash]

I have the following remarks to make about derivations on Lie algebras:

1. In addition to the issue that docs#Derivation requires commutativity (pending a refactor, possibly using right actions) it also requires associativity! So this is another obstacle to unifying docs#Derivation with a new LieDerivation definition.
2. Because all the Lie theory is developed using docs#Bracket for the product rather than docs#Mul, even if we refactored docs#Derivation so that it was able to permit non-commutative, non-associative products, we would still have work to do because we do not have a to_bracket attribute analogous to to_additive for this job (and I don't think we should create one).
3. With the above in mind we should just define LieDerivation essentially as you suggest. If / when we have a sufficiently general docs#Derivation we can have lemmas to connect the two notions, rather than bending over backwards to have a single definition.
4. I think we should generalise LieDerivation slightly to allow for a general representation M of a Lie algebra L (suggestion below).
5. Note that in some sense, the suggestion below commits the same sin as docs#Derivation since its leibniz axiom reverses a and b. It also does this for the same reason: we don't have right actions of Lie algebras. However because every Lie algebra satisfies docs#lie_skew, all is well (see apply_lie_eq_add in the suggestion below). The only way this sin would ever be an issue is if someone wants to develop the theory of derivations of representations of Leibniz algebras which I think is sufficiently exotic that we should ignore it.

import Mathlib.Algebra.Lie.Basic
import Mathlib.Algebra.Lie.Killing

variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
  [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]

structure LieDerivation extends L →ₗ[R] M where
  leibniz (a b : L) : toLinearMap ⁅a, b⁆ = ⁅a, toLinearMap b⁆ - ⁅b, toLinearMap a⁆

namespace LieDerivation

instance instCoeLinearMap : Coe (LieDerivation R L M) (L →ₗ[R] M) := ⟨toLinearMap⟩

instance instFunLike : FunLike (LieDerivation R L M) L M where
  coe D := D.toLinearMap
  coe_injective' D₁ D₂ h := by cases D₁; cases D₂; simpa using h

protected lemma apply_lie_eq_sub (D : LieDerivation R L M) (a b : L) :
    D ⁅a, b⁆ = ⁅a, D b⁆ - ⁅b, D a⁆ :=
  D.leibniz a b

protected lemma apply_lie_eq_add (D : LieDerivation R L L) (a b : L) :
    D ⁅a, b⁆ = ⁅a, D b⁆ + ⁅D a, b⁆ := by
  rw [D.apply_lie_eq_sub, sub_eq_add_neg, lie_skew]

end LieDerivation

def lieDerivationOf (m : M) : LieDerivation R L M where
  __ := (LieModule.toEndomorphism R L M : L →ₗ[R] Module.End R M).flip m
  leibniz := by simp

/-- Every derivation of a finite-dimensional semisimple Lie algebra is inner. -/
lemma LieAlgebra.exists_eq_derivationOf
    (K : Type*) [Field K] [LieAlgebra K L] [FiniteDimensional K L]
    [IsKilling K L] -- Or maybe we really need `[CharZero K] [IsSemisimple K L]`
    (D : LieDerivation K L L) :
    ∃ x, D = lieDerivationOf K L L x := by
  sorry

[Oliver Nash]

My final remark would be that I'm really excited to hear that someone will add LieDerivation to the library: it's a notable gap in our Lie algebra theory. A very useful result which I'd love to see someone add is that every derivation of a finite-dimensional semisimple Lie algebra in characteristic zero is inner (I've added this sorry to the example above).

[Johan Commelin]

Should lieDerivationOf be called innerDerivation or something like that?

[Frédéric Marbach]

Thank you for your detailed answer! As discussed in Marseille, I have started working on this (and the semi-simple related result, for which I am almost done). As a first step, I just pushed PR#11790 which concerns only the definition of Lie derivations, elementary properties (as for the other derivations), and the fact that they form a Lie algebra themselves.

Since I am new to Lean, and I copy-pasted the (non-Lie) Derivation file, my code is guaranteed to contain all the imperfections of the initial file + all new new ones I might have added. So I am looking forward to your feedback.

[Frédéric Marbach]

Thanks @Oliver Nash for reviewing and merging https://github.com/leanprover-community/mathlib4/pull/11790 containing the definition of LieDerivation. I still have a bunch of content on my computer which I am trying to cut in appropriate chunks.

My next step was pushing:
1) the definition of the adjoint action of a Lie algebra L,
2) the fact that it is a Lie algebra morphism from L to the Lie derivations over L,
3) that it's image is an ideal of the set of derivations.

My initial plan was to create a Algebra.Lie.Derivation.AdjointAction file.

Just before pushing, I realized, that the adjoint action is already defined in the Algebra.Lie.OfAssociative file, specifically here LieAlgebra.ad as a Lie algebra morphism from L to the linear endomorphisms of L.

I initially thought that I should extract the section AdjointAction part of Algebra.Lie.OfAssociative and move it to a Algebra.Lie.Derivation.AdjointAction file. But then I realized that this section also contained stuff about LieModule.toEndomorphism which does not seem to be a Lie derivation (since M has no Lie structure). So I thought about extracting only the LieAlgebra.ad part and leave the LieModule.toEndormorphism where it is. But there is some intertwining between the APIs of both.

Where should I put 2) and 3)?

[Johan Commelin]

@Frédéric Marbach How much lines of code is this? If it isn't too much, you could include it in the file on Lie derivations.

[Johan Commelin]

Otherwise, go ahead and start the AdjointAction file.

[Frédéric Marbach]

Not much, around 50 lines. My problem was more that there is already a definition of LieAlgebra.ad in the OfAssociative file. So I need to enhance this definition (to make it clear that the values of ad are Lie derivations, not just endomorphisms). But extracting ad from there seemed tough because it has intertwinned lemmas with the LieModule.toEndomorphism stuff.

[Johan Commelin]

Aah, so just define adLieHom or something like that.

[Johan Commelin]

For example, we also have cast from Nat to any semiring as a function, as add_monoid hom, and as ring hom.

[Johan Commelin]

So we can have multiple versions of the same map.

[Oliver Nash]

I presume you're defining something like:

variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
  [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]

def LieDerivation.inner (m : M) : LieDerivation R L M where
  __ := (LieModule.toEndomorphism R L M : L →ₗ[R] Module.End R M).flip m
  leibniz := by simp

and possibly and abbrev for the case M = L?

In any case, I agree with Johan, make a second definition taking values in LieDerivation R L L together with a simp lemma saying that if it is regarded as a map to Module.End R L then it is equal to docs#LieAlgebra.ad

[Oliver Nash]

Somewhat independently, you should feel free to propose a reorganisation of the file / import structure of the Lie theory files, especially the older files (usually higher up in the hierarchy). Some of the files are also too big and deserve splitting. We have learned a lot since some of the original decisions were taken.

[Frédéric Marbach]

Thanks for your answers. I am working on it.

Parallely, since the proof about inner derivations involves the Killing form, I will need to know that the set of Lie derivations is a finite free module. I created a PR for this basic fact: https://github.com/leanprover-community/mathlib4/pull/11927. I tried to sharpen the hypotheses or shorten the proofs but after many failures I settled for this version which is sufficient for the goal about inner derivations on semisimple Lie algebras.

[Oliver Nash]

Thanks for all your work here. I left some review on #11927 and I look forward to the follow up :)

[Frédéric Marbach]

Thanks! I knew [Field R] was not the correct assumption and that it had something to do with the Noetherian stuff but I had not managed to find your neat solution! I pushed a commit with your changes.

[Frédéric Marbach]

The proof about inner derivations is finished (on my laptop). As a prerequisite, I pushed #12008, which states that if a Lie algebra is isomorphic to a Killing Lie algebra, then it is Killing too.

[Frédéric Marbach]

Another prerequisite is to have lemmas about orthogonal complements for the new bilinear form (not the old one). I pushed #12015 for this purpose.

[Oliver Nash]

Congratulations! This is a really useful result and is basically the dream outcome of my attempt to drag you into the Lie theory effort. I'll take a look at these PRs this evening!

[Oliver Nash]

Here's a mathematical to which I do not know the answer: is it necessary to assume characteristic zero or is non-degenerate Killing form sufficient?

[Frédéric Marbach]

Thank you for suggesting this result! It turned out to be a both a fun landmark and a useful benchmark for my definitions. Lean seems to think that it holds as follows (well, more might be true of course):

variable {R L : Type*} [Field R] [LieRing L]
  [LieAlgebra R L] [Module.Finite R L] [LieAlgebra.IsKilling R L]

theorem exists_eq_ad (D : LieDerivation R L L) : ∃ x, D = ad R L x := by sorry

I might step out of semisimple Lie algebras after this is done since they are far outside my confort zone. I will try to go back to free Lie algebras and prove what I need there.

[Kevin Buzzard]

If you like universal enveloping algebras then I'd love to see them acting on C^infty functions on a Lie group!

[Frédéric Marbach]

Thanks, I see that you guys are experts at suggesting further projects!

For my applications to control theory, I had in mind to "start" by

• the fact that Hall sets yield bases of the free Lie algebra,
• the Poincaré-Birkhoff-Witt theorem,
• the Guillemin-Sternberg realization theorem for transitive Lie algebras.

[Kevin Buzzard]

PBW would I'm sure be a very welcome addition, and it has the advantage that it's what you are interested in :-) FLT can wait :-)

[Johan Commelin]

Huge upvote for PBW from me (-;