feat(Algebra/Lie): define adjoint action and its ideal image (#12106)

This defines the *adjoint action* of a Lie algebra `L` on itself, when seen as an homomorphism of Lie algebras from `L` to the Lie algebra of its derivations. 

The adjoint action was also defined in the `Mathlib.Algebra.Lie.OfAssociative.lean` file, under the name `LieAlgebra.ad`, as the homomorphism with values in the endormophisms of `L`. We make the link between both. This design choice was discussed in [this thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras).

We also establish elementary properties, such as the fact that the image of the adjoint action is an ideal of the derivations.

This is the penultimate step towards proving that all derivations of a finite-dimensional semisimple Lie algebra are inner, a goal described in [this thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras).

Mathlib.lean

@@ -314,6 +314,7 @@ import Mathlib.Algebra.Lie.CartanMatrix
 import Mathlib.Algebra.Lie.CartanSubalgebra
 import Mathlib.Algebra.Lie.Character
 import Mathlib.Algebra.Lie.Classical
+import Mathlib.Algebra.Lie.Derivation.AdjointAction
 import Mathlib.Algebra.Lie.Derivation.Basic
 import Mathlib.Algebra.Lie.DirectSum
 import Mathlib.Algebra.Lie.Engel

Mathlib/Algebra/Lie/Derivation/AdjointAction.lean

@@ -0,0 +1,84 @@
+/-
+Copyright © 2024 Frédéric Marbach. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Frédéric Marbach
+-/
+import Mathlib.Algebra.Lie.Abelian
+import Mathlib.Algebra.Lie.Derivation.Basic
+import Mathlib.Algebra.Lie.OfAssociative
+
+/-!
+# Adjoint action of a Lie algebra on itself
+
+This file defines the *adjoint action* of a Lie algebra on itself, and establishes basic properties.
+
+## Main definitions
+
+- `LieDerivation.ad`: The adjoint action of a Lie algebra `L` on itself, seen as a morphism of Lie
+algebras from `L` to the Lie algebra of its derivations. The adjoint action is also defined in the
+`Mathlib.Algebra.Lie.OfAssociative.lean` file, under the name `LieAlgebra.ad`, as the morphism with
+values in the endormophisms of `L`.
+
+## Main statements
+
+- `LieDerivation.coe_ad_apply_eq_ad_apply`: when seen as endomorphisms, both definitions coincide,
+- `LieDerivation.ad_ker_eq_center`: the kernel of the adjoint action is the center of `L`,
+- `LieDerivation.lie_der_ad_eq_ad_der`: the commutator of a derivation `D` and `ad x` is `ad (D x)`,
+- `LieDerivation.ad_isIdealMorphism`: the range of the adjoint action is an ideal of the
+derivations.
+-/
+
+namespace LieDerivation
+
+section AdjointAction
+
+variable (R L : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
+
+/-- The adjoint action of a Lie algebra `L` on itself, seen as a morphism of Lie algebras from
+`L` to its derivations.
+Note the minus sign: this is chosen to so that `ad ⁅x, y⁆ = ⁅ad x, ad y⁆`. -/
+@[simps!]
+def ad : L →ₗ⁅R⁆ LieDerivation R L L :=
+  { __ := - inner R L L
+    map_lie' := by
+      intro x y
+      ext z
+      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.neg_apply, coe_neg,
+        Pi.neg_apply, inner_apply_apply, commutator_apply]
+      rw [leibniz_lie, neg_lie, neg_lie, ← lie_skew x]
+      abel }
+
+variable {R L}
+
+/-- The definitions `LieDerivation.ad` and `LieAlgebra.ad` agree. -/
+@[simp] lemma coe_ad_apply_eq_ad_apply (x : L) : ad R L x = LieAlgebra.ad R L x := by ext; simp
+
+variable (R L) in
+/-- The kernel of the adjoint action on a Lie algebra is equal to its center. -/
+lemma ad_ker_eq_center : (ad R L).ker = LieAlgebra.center R L := by
+  ext x
+  rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]
+  simp [DFunLike.ext_iff]
+
+/-- The commutator of a derivation `D` and a derivation of the form `ad x` is `ad (D x)`. -/
+lemma lie_der_ad_eq_ad_der (D : LieDerivation R L L) (x : L) : ⁅D, ad R L x⁆ = ad R L (D x) := by
+  ext a
+  rw [commutator_apply, ad_apply_apply, ad_apply_apply, ad_apply_apply, apply_lie_eq_add,
+    add_sub_cancel_left]
+
+variable (R L) in
+/-- The range of the adjoint action homomorphism from a Lie algebra `L` to the Lie algebra of its
+derivations is an ideal of the latter. -/
+lemma ad_isIdealMorphism : (ad R L).IsIdealMorphism := by
+  simp_rw [LieHom.isIdealMorphism_iff, lie_der_ad_eq_ad_der]
+  tauto
+
+/-- A derivation `D` belongs to the ideal range of the adjoint action iff it is of the form `ad x`
+for some `x` in the Lie algebra `L`. -/
+lemma mem_ad_idealRange_iff {D : LieDerivation R L L} :
+    D ∈ (ad R L).idealRange ↔ ∃ x : L, ad R L x = D :=
+  (ad R L).mem_idealRange_iff (ad_isIdealMorphism R L)
+
+end AdjointAction
+
+end LieDerivation

Mathlib/Algebra/Lie/Derivation/Basic.lean

@@ -14,8 +14,9 @@ This file defines *Lie derivations* and establishes some basic properties.
 
 ## Main definitions
 
-- `LieDerivation` : A Lie derivation `D` from the Lie `R`-algebra `L` to the `L`-module `M` is an
+- `LieDerivation`: A Lie derivation `D` from the Lie `R`-algebra `L` to the `L`-module `M` is an
 `R`-linear map that satisfies the Leibniz rule `D [a, b] = [a, D b] - [b, D a]`.
+- `LieDerivation.inner`: The natural map from a Lie module to the derivations taking values in it.
 
 ## Main statements
 
@@ -224,6 +225,8 @@ theorem coe_smul_linearMap (r : S) (D : LieDerivation R L M) : ↑(r • D) = r
 theorem smul_apply (r : S) (D : LieDerivation R L M) : (r • D) a = r • D a :=
   rfl
 
+instance instSMulBase : SMulBracketCommClass R L M := ⟨fun s l a ↦ (lie_smul s l a).symm⟩
+
 instance instSMulNat : SMulBracketCommClass ℕ L M := ⟨fun s l a => (lie_nsmul l a s).symm⟩
 
 instance instSMulInt : SMulBracketCommClass ℤ L M := ⟨fun s l a => (lie_zsmul l a s).symm⟩
@@ -284,8 +287,6 @@ instance : LieRing (LieDerivation R L L) where
   leibniz_lie d e f := by
     ext a; simp only [commutator_apply, add_apply, sub_apply, map_sub]; abel
 
-instance : SMulBracketCommClass R L L := ⟨fun s x y => (lie_smul s x y).symm⟩
-
 /-- The set of Lie derivations from a Lie algebra `L` to itself is a Lie algebra. -/
 instance instLieAlgebra : LieAlgebra R (LieDerivation R L L) where
   lie_smul := fun r d e => by ext a; simp only [commutator_apply, map_smul, smul_sub, smul_apply]
@@ -313,4 +314,20 @@ instance instNoetherian [IsNoetherian R L] : IsNoetherian R (LieDerivation R L L
 
 end
 
+section Inner
+
+variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
+    [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
+
+/-- The natural map from a Lie module to the derivations taking values in it. -/
+@[simps!]
+def inner : M →ₗ[R] LieDerivation R L M where
+  toFun m :=
+    { __ := (LieModule.toEndomorphism R L M : L →ₗ[R] Module.End R M).flip m
+      leibniz' := by simp }
+  map_add' m n := by ext; simp
+  map_smul' t m := by ext; simp
+
+end Inner
+
 end LieDerivation

Mathlib/Algebra/Lie/IdealOperations.lean

@@ -310,9 +310,9 @@ theorem comap_bracket_eq {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
     simp only [hz₁, hz₂, Submodule.coe_mk, LieHom.map_lie]
   · rintro ⟨x, ⟨⟨z₁, hz₁⟩, ⟨z₂, hz₂⟩, hx⟩, hy⟩; rw [← hy, ← hx]
     have hz₁' : f z₁ ∈ f.idealRange ⊓ J₁ := by
-      rw [LieSubmodule.mem_inf]; exact ⟨f.mem_idealRange, hz₁⟩
+      rw [LieSubmodule.mem_inf]; exact ⟨f.mem_idealRange z₁, hz₁⟩
     have hz₂' : f z₂ ∈ f.idealRange ⊓ J₂ := by
-      rw [LieSubmodule.mem_inf]; exact ⟨f.mem_idealRange, hz₂⟩
+      rw [LieSubmodule.mem_inf]; exact ⟨f.mem_idealRange z₂, hz₂⟩
     use ⟨f z₁, hz₁'⟩, ⟨f z₂, hz₂'⟩; simp only [Submodule.coe_mk, LieHom.map_lie]
 #align lie_ideal.comap_bracket_eq LieIdeal.comap_bracket_eq
 

Mathlib/Algebra/Lie/Submodule.lean

@@ -1104,7 +1104,7 @@ theorem idealRange_eq_map : f.idealRange = LieIdeal.map f ⊤ := by
   rfl
 #align lie_hom.ideal_range_eq_map LieHom.idealRange_eq_map
 
-/-- The condition that the image of a morphism of Lie algebras is an ideal. -/
+/-- The condition that the range of a morphism of Lie algebras is an ideal. -/
 def IsIdealMorphism : Prop :=
   (f.idealRange : LieSubalgebra R L') = f.range
 #align lie_hom.is_ideal_morphism LieHom.IsIdealMorphism
@@ -1149,7 +1149,7 @@ theorem mem_ker {x : L} : x ∈ ker f ↔ f x = 0 :=
     simp only [ker_coeSubmodule, LinearMap.mem_ker, coe_toLinearMap]
 #align lie_hom.mem_ker LieHom.mem_ker
 
-theorem mem_idealRange {x : L} : f x ∈ idealRange f := by
+theorem mem_idealRange (x : L) : f x ∈ idealRange f := by
   rw [idealRange_eq_map]
   exact LieIdeal.mem_map (LieSubmodule.mem_top x)
 #align lie_hom.mem_ideal_range LieHom.mem_idealRange