Commit 2024-04-01 21:53 d8d7e696

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.