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
withnamespace LieDerivation
- Remove
open Algebra
- Replace
Algebra A
withLieAlgebra L
everywhere - Replace
Derivation R A M
withLieDerivation 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 forleibniz'
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
andleibniz_invOf
(no inverse in a Lie algebra)map_algebraMap
(no scalars in the Lie algebra)
- Derivation has an
mk'
constructor to bypass themap_one_eq_zero'
field in anAddCancelCommMonoid M
. Since we don't require this property for Lie derivations, we delete everything related:mk'
,coe_mk'
,coe_mk'_linearMap
(the wholesection 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 aseqOn_lieSpan
. Since the proof of this result relied on an induction principleRingTheory.Adjoin.Basic.adjoin_induction
, we needed a similar principle for Lie spans. We added it as theAlgebra.Lie.Submodule.lieSpan_induction
theorem in theAlgebra.Lie.Submodule
file. - Add a
SMulBracketCommClass
class to encode commutativity of scalar multiplication and left Lie action (as a substitute forSMulCommClass S L M
), seesection Scalar
. Introduce instances forS = Nat
andS = 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.