feat(Algebra/Lie): prove derivations are inner in finite-dimensional Killing Lie algebra (#12250)

This finishes the proof that all derivations in a finite-dimensional Lie algebra with non-degenerate Killing form are inner derivations, a project discussed in [this thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras) with @ocfnash.



Co-authored-by: Oliver Nash <github@olivernash.org>

Author: 2 people

Mathlib.lean

@@ -328,6 +328,7 @@ 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.Derivation.Killing
 import Mathlib.Algebra.Lie.DirectSum
 import Mathlib.Algebra.Lie.Engel
 import Mathlib.Algebra.Lie.EngelSubalgebra

Mathlib/Algebra/Lie/Derivation/AdjointAction.lean

@@ -60,6 +60,11 @@ lemma ad_ker_eq_center : (ad R L).ker = LieAlgebra.center R L := by
   rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]
   simp [DFunLike.ext_iff]
 
+/-- If the center of a Lie algebra is trivial, then the adjoint action is injective. -/
+lemma injective_ad_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
+    Function.Injective (ad R L) := by
+  rw [← LieHom.ker_eq_bot, ad_ker_eq_center, h]
+
 /-- 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

Mathlib/Algebra/Lie/Derivation/Killing.lean

@@ -0,0 +1,96 @@
+/-
+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.Derivation.AdjointAction
+import Mathlib.Algebra.Lie.Killing
+import Mathlib.LinearAlgebra.BilinearForm.Orthogonal
+
+/-!
+# Derivations of finite dimensional Killing Lie algebras
+
+This file establishes that all derivations of finite-dimensional Killing Lie algebras are inner.
+
+## Main statements
+
+- `LieDerivation.ad_mem_orthogonal_of_mem_orthogonal`: if a derivation `D` is in the Killing
+orthogonal of the range of the adjoint action, then, for any `x : L`, `ad (D x)` is also in this
+orthogonal.
+- `LieDerivation.Killing.range_ad_eq_top`: in a finite-dimensional Lie algebra with non-degenerate
+Killing form, the range of the adjoint action is full,
+- `LieDerivation.Killing.exists_eq_ad`: in a finite-dimensional Lie algebra with non-degenerate
+Killing form, any derivation is an inner derivation.
+-/
+
+namespace LieDerivation.Killing
+
+section
+
+variable (R L : Type*) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L]
+
+/-- A local notation for the set of (Lie) derivations on `L`. -/
+local notation "𝔻" => (LieDerivation R L L)
+
+/-- A local notation for the range of `ad`. -/
+local notation "𝕀" => (LieHom.range (ad R L))
+
+/-- A local notation for the Killing complement of the ideal range of `ad`. -/
+local notation "𝕀ᗮ" => LinearMap.BilinForm.orthogonal (killingForm R 𝔻) 𝕀
+
+lemma killingForm_restrict_range_ad : (killingForm R 𝔻).restrict 𝕀 = killingForm R 𝕀 := by
+  rw [← (ad_isIdealMorphism R L).eq, ← LieIdeal.killingForm_eq]
+  rfl
+
+variable {R L}
+
+/-- If a derivation `D` is in the Killing orthogonal of the range of the adjoint action, then, for
+any `x : L`, `ad (D x)` is also in this orthogonal. -/
+lemma ad_mem_orthogonal_of_mem_orthogonal {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
+    ad R L (D x) ∈ 𝕀ᗮ := by
+  have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by
+    simp [← (ad_isIdealMorphism R L).eq]
+  rw [this] at hD ⊢
+  rw [← lie_der_ad_eq_ad_der]
+  exact lie_mem_left _ _ (ad R L).idealRange.killingCompl _ _ hD
+
+lemma ad_mem_ker_killingForm_ad_range_of_mem_orthogonal
+    {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
+    ad R L (D x) ∈ (LinearMap.ker (killingForm R 𝕀)).map (LieHom.range (ad R L)).subtype := by
+  rw [← killingForm_restrict_range_ad]
+  exact LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict
+    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl ⟨by simp, ad_mem_orthogonal_of_mem_orthogonal hD x⟩
+
+variable (R L)
+variable [LieAlgebra.IsKilling R L]
+
+@[simp] lemma ad_apply_eq_zero_iff (x : L) : ad R L x = 0 ↔ x = 0 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+  rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot_of_semisimple,
+    LieSubmodule.mem_bot] at h
+
+instance instIsKilling_range_ad : LieAlgebra.IsKilling R 𝕀 :=
+  (LieEquiv.ofInjective (ad R L) (injective_ad_of_center_eq_bot <| by simp)).isKilling
+
+/-- The restriction of the Killing form of a finite-dimensional Killing Lie algebra to the range of
+the adjoint action is nondegenerate. -/
+lemma killingForm_restrict_range_ad_nondegenerate : ((killingForm R 𝔻).restrict 𝕀).Nondegenerate :=
+  killingForm_restrict_range_ad R L ▸ LieAlgebra.IsKilling.killingForm_nondegenerate R _
+
+/-- The range of the adjoint action on a finite-dimensional Killing Lie algebra is full. -/
+@[simp]
+lemma range_ad_eq_top : 𝕀 = ⊤ := by
+  rw [← LieSubalgebra.coe_to_submodule_eq_iff]
+  apply LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
+    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl (killingForm_restrict_range_ad_nondegenerate R L)
+  refine (Submodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
+  simpa using ad_mem_ker_killingForm_ad_range_of_mem_orthogonal hD x
+
+variable {R L} in
+/-- Every derivation of a finite-dimensional Killing Lie algebra is an inner derivation. -/
+lemma exists_eq_ad (D : 𝔻) : ∃ x, ad R L x = D := by
+  change D ∈ 𝕀
+  rw [range_ad_eq_top R L]
+  exact Submodule.mem_top
+
+end

Mathlib/Algebra/Lie/Killing.lean

@@ -80,6 +80,8 @@ lemma traceForm_apply_apply (x y : L) :
 lemma traceForm_comm (x y : L) : traceForm R L M x y = traceForm R L M y x :=
   LinearMap.trace_mul_comm R (φ x) (φ y)
 
+lemma traceForm_isSymm : LinearMap.IsSymm (traceForm R L M) := LieModule.traceForm_comm R L M
+
 @[simp] lemma traceForm_flip : LinearMap.flip (traceForm R L M) = traceForm R L M :=
   Eq.symm <| LinearMap.ext₂ <| traceForm_comm R L M
 
@@ -367,29 +369,28 @@ variable (I : LieIdeal R L)
 
 /-- The orthogonal complement of an ideal with respect to the killing form is an ideal. -/
 noncomputable def killingCompl : LieIdeal R L :=
-  { LinearMap.ker ((killingForm R L).compl₁₂ LinearMap.id I.subtype) with
+  { __ := (killingForm R L).orthogonal I.toSubmodule
     lie_mem := by
       intro x y hy
-      ext ⟨z, hz⟩
-      suffices killingForm R L ⁅x, y⁆ z = 0 by simpa
-      rw [LieModule.traceForm_comm, ← LieModule.traceForm_apply_lie_apply, LieModule.traceForm_comm]
       simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
-        Submodule.mem_toAddSubmonoid, LinearMap.mem_ker] at hy
-      replace hy := LinearMap.congr_fun hy ⟨⁅z, x⁆, lie_mem_left R L I z x hz⟩
-      simpa using hy }
+        Submodule.mem_toAddSubmonoid, LinearMap.BilinForm.mem_orthogonal_iff,
+        LieSubmodule.mem_coeSubmodule, LinearMap.BilinForm.IsOrtho]
+      intro z hz
+      rw [← LieModule.traceForm_apply_lie_apply]
+      exact hy _ <| lie_mem_left _ _ _ _ _ hz }
+
+@[simp] lemma toSubmodule_killingCompl :
+    LieSubmodule.toSubmodule I.killingCompl = (killingForm R L).orthogonal I.toSubmodule :=
+  rfl
 
 @[simp] lemma mem_killingCompl {x : L} :
-    x ∈ I.killingCompl ↔ ∀ y ∈ I, killingForm R L x y = 0 := by
-  change x ∈ LinearMap.ker ((killingForm R L).compl₁₂ LinearMap.id I.subtype) ↔ _
-  simp only [LinearMap.mem_ker, LieModule.traceForm_apply_apply, LinearMap.ext_iff,
-    LinearMap.compl₁₂_apply, LinearMap.id_coe, id_eq, Submodule.coeSubtype,
-    LieModule.traceForm_apply_apply, LinearMap.zero_apply, Subtype.forall]
+    x ∈ I.killingCompl ↔ ∀ y ∈ I, killingForm R L y x = 0 := by
   rfl
 
 lemma coe_killingCompl_top :
     killingCompl R L ⊤ = LinearMap.ker (killingForm R L) := by
-  ext
-  simp [LinearMap.ext_iff]
+  ext x
+  simp [LinearMap.ext_iff, LinearMap.BilinForm.IsOrtho, LieModule.traceForm_comm R L L x]
 
 variable [IsDomain R] [IsPrincipalIdealRing R]
 
@@ -406,7 +407,7 @@ lemma restrict_killingForm :
   intro x (hx : x ∈ I)
   simp only [mem_killingCompl, LieSubmodule.mem_top, forall_true_left]
   intro y
-  rw [LieModule.traceForm_comm, LieModule.traceForm_apply_apply]
+  rw [LieModule.traceForm_apply_apply]
   exact LieSubmodule.traceForm_eq_zero_of_isTrivial I I (by simp) _ hx
 
 end LieIdeal
@@ -746,7 +747,7 @@ respective Killing forms of `L` and `L'` satisfy `κ'(e x, e y) = κ(x, y)`. -/
 lemma isKilling_of_equiv [IsKilling R L] (e : L ≃ₗ⁅R⁆ L') : IsKilling R L' := by
   constructor
   ext x'
-  rw [LieIdeal.mem_killingCompl]
+  simp_rw [LieIdeal.mem_killingCompl, LieModule.traceForm_comm]
   refine ⟨fun hx' ↦ ?_, fun hx y _ ↦ hx ▸ LinearMap.map_zero₂ (killingForm R L') y⟩
   suffices e.symm x' ∈ LinearMap.ker (killingForm R L) by
     rw [IsKilling.ker_killingForm_eq_bot] at this

Mathlib/Algebra/Lie/Submodule.lean

@@ -1114,6 +1114,9 @@ theorem isIdealMorphism_def : f.IsIdealMorphism ↔ (f.idealRange : LieSubalgebr
   Iff.rfl
 #align lie_hom.is_ideal_morphism_def LieHom.isIdealMorphism_def
 
+variable {f} in
+theorem IsIdealMorphism.eq (hf : f.IsIdealMorphism) : f.idealRange = f.range := hf
+
 theorem isIdealMorphism_iff : f.IsIdealMorphism ↔ ∀ (x : L') (y : L), ∃ z : L, ⁅x, f y⁆ = f z := by
   simp only [isIdealMorphism_def, idealRange_eq_lieSpan_range, ←
     LieSubalgebra.coe_to_submodule_eq_iff, ← f.range.coe_to_submodule,

Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

@@ -161,6 +161,8 @@ theorem mem_orthogonal_iff {N : Submodule R M} {m : M} :
   Iff.rfl
 #align bilin_form.mem_orthogonal_iff LinearMap.BilinForm.mem_orthogonal_iff
 
+@[simp] lemma orthogonal_bot : B.orthogonal ⊥ = ⊤ := by ext; simp [IsOrtho]
+
 theorem orthogonal_le (h : N ≤ L) : B.orthogonal L ≤ B.orthogonal N := fun _ hn l hl => hn l (h hl)
 #align bilin_form.orthogonal_le LinearMap.BilinForm.orthogonal_le
 
@@ -318,7 +320,9 @@ variable [FiniteDimensional K V]
 
 open FiniteDimensional Submodule
 
-theorem finrank_add_finrank_orthogonal {B : BilinForm K V} {W : Subspace K V} (b₁ : B.IsRefl) :
+variable {B : BilinForm K V} {W : Subspace K V}
+
+theorem finrank_add_finrank_orthogonal (b₁ : B.IsRefl) :
     finrank K W + finrank K (B.orthogonal W) =
       finrank K V + finrank K (W ⊓ B.orthogonal ⊤ : Subspace K V) := by
   rw [← toLin_restrict_ker_eq_inf_orthogonal _ _ b₁, ←
@@ -332,7 +336,7 @@ theorem finrank_add_finrank_orthogonal {B : BilinForm K V} {W : Subspace K V} (b
 
 /-- A subspace is complement to its orthogonal complement with respect to some
 reflexive bilinear form if that bilinear form restricted on to the subspace is nondegenerate. -/
-theorem restrict_nondegenerate_of_isCompl_orthogonal {B : BilinForm K V} {W : Subspace K V}
+theorem restrict_nondegenerate_of_isCompl_orthogonal
     (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) : IsCompl W (B.orthogonal W) := by
   have : W ⊓ B.orthogonal W = ⊥ := by
     rw [eq_bot_iff]
@@ -351,12 +355,40 @@ theorem restrict_nondegenerate_of_isCompl_orthogonal {B : BilinForm K V} {W : Su
 
 /-- A subspace is complement to its orthogonal complement with respect to some reflexive bilinear
 form if and only if that bilinear form restricted on to the subspace is nondegenerate. -/
-theorem restrict_nondegenerate_iff_isCompl_orthogonal {B : BilinForm K V} {W : Subspace K V}
+theorem restrict_nondegenerate_iff_isCompl_orthogonal
     (b₁ : B.IsRefl) : (B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W) :=
   ⟨fun b₂ => restrict_nondegenerate_of_isCompl_orthogonal b₁ b₂, fun h =>
     B.nondegenerateRestrictOfDisjointOrthogonal b₁ h.1⟩
 #align bilin_form.restrict_nondegenerate_iff_is_compl_orthogonal LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal
 
+lemma orthogonal_eq_top_iff (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) :
+    B.orthogonal W = ⊤ ↔ W = ⊥ := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
+  have := (B.restrict_nondegenerate_of_isCompl_orthogonal b₁ b₂).inf_eq_bot
+  rwa [h, inf_top_eq] at this
+
+lemma eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
+    (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.orthogonal W = ⊥) :
+    W = ⊤ := by
+  have := (B.restrict_nondegenerate_of_isCompl_orthogonal b₁ b₂).sup_eq_top
+  rwa [b₃, sup_bot_eq] at this
+
+lemma orthogonal_eq_bot_iff
+    (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) (b₃ : B.Nondegenerate) :
+    B.orthogonal W = ⊥ ↔ W = ⊤ := by
+  refine ⟨eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot b₁ b₂, fun h ↦ ?_⟩
+  rw [h, eq_bot_iff]
+  exact fun x hx ↦ b₃ x fun y ↦ b₁ y x <| by simpa using hx y
+
+lemma inf_orthogonal_self_le_ker_restrict (b₁ : B.IsRefl) :
+    W ⊓ B.orthogonal W ≤ (LinearMap.ker <| B.restrict W).map W.subtype := by
+  rintro v ⟨hv : v ∈ W, hv' : v ∈ B.orthogonal W⟩
+  simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coeSubtype, Subtype.exists,
+    exists_and_left, exists_prop, exists_eq_right_right]
+  refine ⟨?_, hv⟩
+  ext ⟨w, hw⟩
+  exact b₁ w v <| hv' w hw
+
 end
 
 /-! We note that we cannot use `BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal` for the