feat: Killing orthogonal complement is complement (leanprover-community#34856)

Killing orthogonal complement is complement

Co-authored-by: Janos Wolosz <janos.wolosz@gmail.com>

Author: jano-wol

Mathlib/Algebra/Lie/Killing.lean

@@ -33,6 +33,8 @@ This file contains basic definitions and results for such Lie algebras.
   has non-singular Killing form then it is semisimple.
 * `LieAlgebra.IsKilling.instHasTrivialRadical`: if a Lie algebra over a PID
   has non-singular Killing form then it has trivial radical.
+* `LieIdeal.isCompl_killingCompl`: if a Lie algebra has non-singular Killing form then for all
+  ideals, an ideal and its Killing orthogonal complement are complements.
 
 ## TODO
 
@@ -127,3 +129,23 @@ alias _root_.LieEquiv.isKilling := LieAlgebra.isKilling_of_equiv
 end LieEquiv
 
 end LieAlgebra
+
+open LieAlgebra in
+variable {K L} in
+lemma LieIdeal.isCompl_killingCompl [IsKilling K L] [Module.Finite K L] (I : LieIdeal K L) :
+    IsCompl I I.killingCompl := by
+  suffices Disjoint I I.killingCompl by
+    rwa [← LieSubmodule.isCompl_toSubmodule, I.toSubmodule_killingCompl,
+      LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint (LieModule.traceForm_isSymm K L L).isRefl,
+      ← I.toSubmodule_killingCompl, LieSubmodule.disjoint_toSubmodule]
+  suffices IsLieAbelian (I ⊓ I.killingCompl : LieIdeal K L) by
+    rw [disjoint_iff]
+    exact IsKilling.ideal_eq_bot_of_isLieAbelian _
+  suffices ∀ (x y z : L) (hx : x ∈ killingCompl K L I) (hy : y ∈ I),
+      LieModule.traceForm K L L ⁅x, y⁆ z = 0 by
+    rw [LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieSubmodule.lie_eq_bot_iff]
+    rintro x ⟨-, hx⟩ y ⟨hy, -⟩
+    exact (IsKilling.killingForm_nondegenerate K L).1 _ fun z ↦ this x y z hx hy
+  intro x y z hx hy
+  rw [LieModule.traceForm_apply_lie_apply K L L x y z, LieModule.traceForm_comm K L L]
+  exact I.mem_killingCompl.mp hx _ <| lie_mem_left K L I y z hy