Derivations

Stream: maths

[Oliver Nash]

I'm interested in defining derivations (or in having someone else define them!) and I'm wondering how hard we should try to be general.

Thanks to @Nicolò Cavalleri I have seen this thread:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/derivation
where @Kenny Lau sketched out some superb stuff but seems to have shelved it a year ago.

[Oliver Nash]

Consider the following (informal) theorems / definitions:

1. The exceptional Lie algebra g₂ is equivalent to the derivations of the octonions
2. Every derivation of a semisimple Lie algebra is inner
3. For commutative algebras there exists a universal derivation through which all others factor

For now I'm only interested in 1 above but I would like if the same definition of derivation worked for each.

[Oliver Nash]

Mathematically, given a possibly-non-associative algebra $A$, a derivation is an additive group $M$ that is simultaneously a left- and right- $A$-module (not necessarily a bimodule since I want to cater for the non-associative cases 1 and 2 with the algebras as left-right modules over themselves via multiplication) together with a linear map: $d : A \to M$
satisfying: $d(ab) = (da) • b + a • db$

[Oliver Nash]

Unfortunately, I immediately encounter a few issues if I think about formalising this in Mathlib.
Specifically:
A. We do not have a definition of not-necessarily-associative algebras
B. We only have left modules
C. The product on Lie algebras comes from an instance of has_bracket rather than has_mul

To me (A) is fine; indeed building up the theory of non-necessarily-associative algebras, say as far as basic facts about composition algebras, would probably be very rewarding. Everyone knows the octonions are loads of fun!

For (B) maybe there's no issue here provided I'm willing to talk about opposite rings.

So it's (C) that really concerns me. Even with (A) and (B) out of the way, we're be faced with the problem that Lie algebras would not definitionally be non-associative algebras and so we'd be forced to have a separate lie_derivation definition and annoying logic to transport language back and forth.

[Oliver Nash]

I realise this is all rather waffly but I'd be very grateful for any comments, especially with respect to (C). I do hope the above makes sense, I have had some wine.

[Kevin Buzzard]

Your point is that the operation on the octonians is usually written * but the operation on a Lie algebra is usually written [a,b] and you want these both to be instances of a non-associative algebra class. Yeah, this is an issue, I agree. You can either bundle the operation into the definition of the class, or you can write to_bracketive :-/

[Oliver Nash]

Oh, I realise I have a thinko above wrt (B) I should be talking about modules of a possibly-non-associative _algebra_ and I'd need some convincing there's a sensible representation theory of these

[Oliver Nash]

@Kevin Buzzard Yes that's exactly my point.

[Oliver Nash]

I think I'll need to sleep on this, the more I think about this, the slightly less trivial it seems to be to make the general definition I'd like.

[Kevin Buzzard]

@Yury G. Kudryashov let's say Oliver wanted to make a variant has_foo of has_add, and we wanted too_fooitive to work in some part of mathematics, e.g. the theory of Lie algebras, translating between theorems with a typeclass has_foo and theorems with a typeclass has_mul (which also happened to be Lie algebras). At the very least you'd need some kind of dictionary from the mul, one, inv words to the corresponding abbreviations in your language. If we can't do this, then how do we put the R-algebra structure on 2x2 real matrices coming from the Lie bracket? Those matrices already have an R-algebra structure, coming from matrix multiplication.

[Yury G. Kudryashov]

I see two possible approaches to has_mul vs has_bracket: (1) type tag like multiplicative/additive; (2) to_additive-style attribute.

[Oliver Nash]

OK thank you both. I hope to have time to return to this in a week or so. For now I'm mentally summarising this as "while awkward, solutions exist".

[Yury G. Kudryashov]

Feel free to ask questions about pros and cons of each approach. I don't read all the messages every day, so the best way to get a faster reply from me is to @ tag me.

[Kevin Buzzard]

I see. So lie_algebra.to_nonassociative_algebra sends L to the defeq to_multiplicative L and then you just pray that Lean guesses the right multiplication

[Yury G. Kudryashov]

Yes, you define instance to_nonassoc_algebra_has_mul [has_bracket L] : has_mul (to_nonassoc_algebra L) := ⟨λ x y, (bracket x y : L)⟩, then restate all theorems you need about has_mul version in terms of has_bracket with proofs := @mul_thm (to_nonassoc_algebra L) ... (see algebra/group_power for example).

[Oliver Nash]

Thanks @Yury G. Kudryashov I look forward to trying to use this in the near future. I appreciate the guidance!