# Commit 2024-04-01 21:53 d8d7e696

View on Github →feat(Algebra/Lie): define derivations on Lie algebras (#11790)
This defines derivations on Lie algebras. The current definition of Derivation is restricted to commutative associative algebras, and thus cannot be used to manipulate derivations on Lie algebras. As discussed in this Zulip thread, we thus give a parallel definition of a `LieDerivation`

structure, which is specific to derivations on Lie algebras.
This PR is focused on the definition of this structure and the first associated properties. It adds a new file `Algebra.Lie.Derivation.Basic`

which was mostly obtained by a large copy-paste of file `RingTheory.Derivation.Basic`

. I report below the changes I made with respect to this other version.

- Remove all
`#align`

directives - Adapt import statements
- Add new definition of
`LieDerivation`

- Replace
`namespace Derivation`

with`namespace LieDerivation`

- Remove
`open Algebra`

- Replace
`Algebra A`

with`LieAlgebra L`

everywhere - Replace
`Derivation R A M`

with`LieDerivation R L M`

everywhere - Delete field
`map_one_eq_zero'`

in instances, since we don't require it in the definition of Lie derivation - Adjust
`simp only`

tactics for`leibniz'`

field in instances - Add lemma
`apply_lie_eq_add`

to restore usual Leibniz rule in Lie algebras (since our definition relies on left actions, so has a minus sign). - There is no unit 1 in a Lie algebra. We delete all related theorems
`map_one_eq_zero`

(there is no 1 in a Lie algebra)`map_coe_nat`

(there is no "n : Nat" in a Lie algebra)`map_coe_int`

(there is no "n : Int" in a Lie algebra)`leibniz_pow`

(there is "power" in a Lie algebra)`leibniz_of_mul_eq_one`

(there is no [a,b]= 1 in a Lie algebra)`leibniz_inv`

and`leibniz_invOf`

(no inverse in a Lie algebra)`map_algebraMap`

(no scalars in the Lie algebra)

- Derivation has an
`mk'`

constructor to bypass the`map_one_eq_zero'`

field in an`AddCancelCommMonoid M`

. Since we don't require this property for Lie derivations, we delete everything related:`mk'`

,`coe_mk'`

,`coe_mk'_linearMap`

(the whole`section Cancel`

) - Derivations have a theorem
`eqOn_adjoin`

to prove that if two derivations are equal on a set, they are equal on the subalgebra spanned by this set. We write it as`eqOn_lieSpan`

. Since the proof of this result relied on an induction principle`RingTheory.Adjoin.Basic.adjoin_induction`

, we needed a similar principle for Lie spans. We added it as the`Algebra.Lie.Submodule.lieSpan_induction`

theorem in the`Algebra.Lie.Submodule`

file. - Add a
`SMulBracketCommClass`

class to encode commutativity of scalar multiplication and left Lie action (as a substitute for`SMulCommClass S L M`

), see`section Scalar`

. Introduce instances for`S = Nat`

and`S = Int`

. - Unwrap useless section, useless variables
- Delete
`compAlgebraMap`

theorem, related with a tower of algebras, since a Lie algebra cannot serve as a scalar field for another one. - Delete
`section Pushforward`

(and everything inside), as it was related to composing an A-linear map with a derivation. While this works when A is an associative algebra, one cannot use a Lie algebra in this role since it is not associative. - Could not figure out what the equivalent instance of
`IsCentralScalar S (Derivation R A M)`

for a Lie derivation should be, so I skipped this instance.