feat(Algebra/Lie): Killing Lie algebras are semisimple (#13265)

Author: jcommelin

Mathlib/Algebra/Lie/Killing.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import Mathlib.Algebra.Lie.InvariantForm
 import Mathlib.Algebra.Lie.Semisimple.Basic
 import Mathlib.Algebra.Lie.TraceForm
 
@@ -22,19 +23,22 @@ non-degenerate Killing form.
 
 This file contains basic definitions and results for such Lie algebras.
 
-## Main definitions
+## Main declarations
+
  * `LieAlgebra.IsKilling`: a typeclass encoding the fact that a Lie algebra has a non-singular
    Killing form.
- * `LieAlgebra.IsKilling.instHasTrivialRadical`: if a Lie algebra has non-singular Killing form
-   then it has trivial radical.
+ * `LieAlgebra.IsKilling.instSemisimple`: if a finite-dimensional Lie algebra over a field
+   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.
 
 ## TODO
 
  * Prove that in characteristic zero, a semisimple Lie algebra has non-singular Killing form.
 
 -/
 
-variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
+variable (R K L M : Type*) [CommRing R] [Field K] [LieRing L] [LieAlgebra R L] [LieAlgebra K L]
 
 namespace LieAlgebra
 
@@ -60,13 +64,28 @@ lemma killingForm_nondegenerate :
     (killingForm R L).Nondegenerate := by
   simp [LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot]
 
-/-- The converse of this is true over a field of characteristic zero. There are counterexamples
-over fields with positive characteristic. -/
-instance instHasTrivialRadical [IsDomain R] [IsPrincipalIdealRing R] : HasTrivialRadical R L := by
-  refine (hasTrivialRadical_iff_no_abelian_ideals R L).mpr fun I hI ↦ ?_
+variable {R L} in
+lemma ideal_eq_bot_of_isLieAbelian [IsDomain R] [IsPrincipalIdealRing R]
+    (I : LieIdeal R L) [IsLieAbelian I] : I = ⊥ := by
   rw [eq_bot_iff, ← killingCompl_top_eq_bot]
   exact I.le_killingCompl_top_of_isLieAbelian
 
+instance instSemisimple [IsKilling K L] [Module.Finite K L] : IsSemisimple K L := by
+  apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)
+  · exact IsKilling.killingForm_nondegenerate _ _
+  · exact LieModule.traceForm_lieInvariant _ _ _
+  · exact (LieModule.traceForm_isSymm K L L).isRefl
+  · intro I h₁ h₂
+    exact h₁.1 <| IsKilling.ideal_eq_bot_of_isLieAbelian I
+
+/-- The converse of this is true over a field of characteristic zero. There are counterexamples
+over fields with positive characteristic.
+
+Note that when the coefficients are a field this instance is redundant since we have
+`LieAlgebra.IsKilling.instSemisimple` and `LieAlgebra.IsSemisimple.instHasTrivialRadical`. -/
+instance instHasTrivialRadical [IsDomain R] [IsPrincipalIdealRing R] : HasTrivialRadical R L :=
+  (hasTrivialRadical_iff_no_abelian_ideals R L).mpr IsKilling.ideal_eq_bot_of_isLieAbelian
+
 end IsKilling
 
 section LieEquiv

Mathlib/Algebra/Lie/TraceForm.lean

@@ -3,12 +3,12 @@ Copyright (c) 2023 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.LinearAlgebra.PID
 import Mathlib.Algebra.DirectSum.LinearMap
-import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
-import Mathlib.LinearAlgebra.BilinearForm.Orthogonal
+import Mathlib.Algebra.Lie.InvariantForm
 import Mathlib.Algebra.Lie.Weights.Cartan
 import Mathlib.Algebra.Lie.Weights.Linear
+import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
+import Mathlib.LinearAlgebra.PID
 
 /-!
 # The trace and Killing forms of a Lie algebra.
@@ -85,6 +85,10 @@ lemma traceForm_apply_lie_apply' (x y z : L) :
       = - traceForm R L M ⁅y, x⁆ z := by rw [← lie_skew x y, map_neg, LinearMap.neg_apply]
     _ = - traceForm R L M y ⁅x, z⁆ := by rw [traceForm_apply_lie_apply]
 
+lemma traceForm_lieInvariant : (traceForm R L M).lieInvariant L := by
+  intro x y z
+  rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]
+
 /-- This lemma justifies the terminology "invariant" for trace forms. -/
 @[simp] lemma lie_traceForm_eq_zero (x : L) : ⁅x, traceForm R L M⁆ = 0 := by
   ext y z
@@ -344,15 +348,7 @@ 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 :=
-  { __ := (killingForm R L).orthogonal I.toSubmodule
-    lie_mem := by
-      intro x y hy
-      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
-        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 }
+  LieAlgebra.InvariantForm.orthogonal (killingForm R L) (LieModule.traceForm_lieInvariant R L L) I
 
 @[simp] lemma toSubmodule_killingCompl :
     LieSubmodule.toSubmodule I.killingCompl = (killingForm R L).orthogonal I.toSubmodule :=