feat: if a Lie algebra has non-degenerate Killing form then its Cartan subalgebras are Abelian (#8430)

Note: the proof (due to Zassenhaus) makes no assumption about the characteristic of the coefficients.

Author: ocfnash

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -47,4 +47,12 @@ lemma trace_eq_sum_trace_restrict [Fintype ι]
     toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf, Matrix.trace_blockDiagonal',
     ← trace_eq_matrix_trace]
 
+lemma trace_eq_sum_trace_restrict' (hN : {i | N i ≠ ⊥}.Finite)
+    {f : M →ₗ[R] M} (hf : ∀ i, MapsTo f (N i) (N i)) :
+    trace R M f = ∑ i in hN.toFinset, trace R (N i) (f.restrict (hf i)) := by
+  let _ : Fintype {i // N i ≠ ⊥} := hN.fintype
+  let _ : Fintype {i | N i ≠ ⊥} := hN.fintype
+  rw [← Finset.sum_coe_sort, trace_eq_sum_trace_restrict (isInternal_ne_bot_iff.mpr h) _]
+  exact Fintype.sum_equiv hN.subtypeEquivToFinset _ _ (fun i ↦ rfl)
+
 end LinearMap

Mathlib/Algebra/DirectSum/Module.lean

@@ -453,6 +453,12 @@ theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} (
   exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩
 #align direct_sum.is_internal_submodule_iff_is_compl DirectSum.isInternal_submodule_iff_isCompl
 
+@[simp]
+theorem isInternal_ne_bot_iff {A : ι → Submodule R M} :
+    IsInternal (fun i : {i // A i ≠ ⊥} ↦ A i) ↔ IsInternal A := by
+  simp only [isInternal_submodule_iff_independent_and_iSup_eq_top]
+  exact Iff.and CompleteLattice.independent_ne_bot_iff_independent <| by simp
+
 /-! Now copy the lemmas for subgroup and submonoids. -/
 
 

Mathlib/Algebra/Lie/Abelian.lean

@@ -45,6 +45,14 @@ theorem trivial_lie_zero (L : Type v) (M : Type w) [Bracket L M] [Zero M] [LieMo
   LieModule.IsTrivial.trivial x m
 #align trivial_lie_zero trivial_lie_zero
 
+instance LieModule.instIsTrivialOfSubsingleton {L M : Type*}
+    [LieRing L] [AddCommGroup M] [LieRingModule L M] [Subsingleton L] : LieModule.IsTrivial L M :=
+  ⟨fun x m ↦ by rw [Subsingleton.eq_zero x, zero_lie]⟩
+
+instance LieModule.instIsTrivialOfSubsingleton' {L M : Type*}
+    [LieRing L] [AddCommGroup M] [LieRingModule L M] [Subsingleton M] : LieModule.IsTrivial L M :=
+  ⟨fun x m ↦ by simp_rw [Subsingleton.eq_zero m, lie_zero]⟩
+
 /-- A Lie algebra is Abelian iff it is trivial as a Lie module over itself. -/
 abbrev IsLieAbelian (L : Type v) [Bracket L L] [Zero L] : Prop :=
   LieModule.IsTrivial L L
@@ -87,11 +95,6 @@ theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :
   simp only [h₁, h₂, LieRing.of_associative_ring_bracket, sub_eq_zero]
 #align commutative_ring_iff_abelian_lie_ring commutative_ring_iff_abelian_lie_ring
 
-theorem LieAlgebra.isLieAbelian_bot (R : Type u) (L : Type v) [CommRing R] [LieRing L]
-    [LieAlgebra R L] : IsLieAbelian (⊥ : LieIdeal R L) :=
-  ⟨fun ⟨x, hx⟩ _ => by simp [eq_iff_true_of_subsingleton]⟩
-#align lie_algebra.is_lie_abelian_bot LieAlgebra.isLieAbelian_bot
-
 section Center
 
 variable (R : Type u) (L : Type v) (M : Type w) (N : Type w₁)
@@ -281,6 +284,12 @@ theorem isLieAbelian_iff_center_eq_top : IsLieAbelian L ↔ center R L = ⊤ :=
 
 end LieAlgebra
 
+variable {R L} in
+lemma LieModule.commute_toEndomorphism_of_mem_center_left
+    {x : L} (hx : x ∈ LieAlgebra.center R L) (y : L) :
+    Commute (toEndomorphism R L M x) (toEndomorphism R L M y) := by
+  rw [Commute.symm_iff, commute_iff_lie_eq, ← LieHom.map_lie, hx y, LieHom.map_zero]
+
 end Center
 
 section IdealOperations

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.DirectSum.LinearMap
 import Mathlib.Algebra.Lie.Nilpotent
 import Mathlib.Algebra.Lie.Semisimple
 import Mathlib.Algebra.Lie.Weights.Cartan
@@ -35,6 +36,8 @@ We define the trace / Killing form in this file and prove some basic properties.
    a Lie algebra is non-singular, it remains non-singular when restricted to a Cartan subalgebra.
  * `LieAlgebra.IsKilling.isSemisimple`: if a Lie algebra has non-singular Killing form then it is
    semisimple.
+ * `LieAlgebra.IsKilling.isLieAbelian_of_isCartanSubalgebra`: if the Killing form of a Lie algebra
+   is non-singular, then its Cartan subalgebras are Abelian.
 
 ## TODO
 
@@ -45,9 +48,13 @@ variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
   [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
   [Module.Free R M] [Module.Finite R M]
 
+attribute [local instance] isNoetherian_of_isNoetherianRing_of_finite
+attribute [local instance] Module.free_of_finite_type_torsion_free'
+
 local notation "φ" => LieModule.toEndomorphism R L M
 
 open LinearMap (trace)
+open Set BigOperators
 
 namespace LieModule
 
@@ -162,6 +169,67 @@ lemma eq_zero_of_mem_weightSpace_mem_posFitting [LieAlgebra.IsNilpotent R L]
   obtain ⟨m, rfl⟩ := (mem_posFittingCompOf R x m₁).mp hm₁ k
   simp [hB, hk]
 
+lemma trace_toEndomorphism_eq_zero_of_mem_lcs
+    {k : ℕ} {x : L} (hk : 1 ≤ k) (hx : x ∈ lowerCentralSeries R L L k) :
+    trace R _ (toEndomorphism R L M x) = 0 := by
+  replace hx : x ∈ lowerCentralSeries R L L 1 := antitone_lowerCentralSeries _ _ _ hk hx
+  replace hx : x ∈ Submodule.span R {m | ∃ u v : L, ⁅u, v⁆ = m} := by
+    rw [lowerCentralSeries_succ, ← LieSubmodule.mem_coeSubmodule,
+      LieSubmodule.lieIdeal_oper_eq_linear_span'] at hx
+    simpa using hx
+  refine Submodule.span_induction (p := fun x ↦ trace R _ (toEndomorphism R L M x) = 0) hx
+    (fun y ⟨u, v, huv⟩ ↦ ?_) ?_ (fun u v hu hv ↦ ?_) (fun t u hu ↦ ?_)
+  · simp_rw [← huv, LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
+  · simp
+  · simp [hu, hv]
+  · simp [hu]
+
+variable [LieAlgebra.IsNilpotent R L] [IsTriangularizable R L M]
+  [IsDomain R] [IsPrincipalIdealRing R]
+
+lemma traceForm_eq_sum_weightSpaceOf (z : L) :
+    traceForm R L M =
+    ∑ χ in (finite_weightSpaceOf_ne_bot R L M z).toFinset, traceForm R L (weightSpaceOf M χ z) := by
+  ext x y
+  have hxy : ∀ χ : R, MapsTo ((toEndomorphism R L M x).comp (toEndomorphism R L M y))
+      (weightSpaceOf M χ z) (weightSpaceOf M χ z) :=
+    fun χ m hm ↦ LieSubmodule.lie_mem _ <| LieSubmodule.lie_mem _ hm
+  have hfin : {χ : R | (weightSpaceOf M χ z : Submodule R M) ≠ ⊥}.Finite := by
+    convert finite_weightSpaceOf_ne_bot R L M z
+    exact LieSubmodule.coeSubmodule_eq_bot_iff (weightSpaceOf M _ _)
+  classical
+  have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
+    (LieSubmodule.independent_iff_coe_toSubmodule.mp <| independent_weightSpaceOf R L M z)
+    (IsTriangularizable.iSup_eq_top z)
+  simp only [LinearMap.coeFn_sum, Finset.sum_apply, traceForm_apply_apply,
+    LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
+  exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)
+
+-- In characteristic zero a stronger result holds (no `⊓ LieAlgebra.center K L`) TODO prove this!
+lemma lowerCentralSeries_one_inf_center_le_ker_traceForm :
+    lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L ≤ LinearMap.ker (traceForm R L M) := by
+  rintro z ⟨hz : z ∈ lowerCentralSeries R L L 1, hzc : z ∈ LieAlgebra.center R L⟩
+  ext x
+  suffices ∀ χ : R, traceForm R L (weightSpaceOf M χ x) z x = 0 by
+    simp [traceForm_eq_sum_weightSpaceOf R L M x, this]
+  intro χ
+  replace hz : LinearMap.trace R _ (toEndomorphism R L (weightSpaceOf M χ x) z) = 0 :=
+    trace_toEndomorphism_eq_zero_of_mem_lcs R L _ (le_refl _) hz
+  let f := toEndomorphism R L (weightSpaceOf M χ x) z
+  let g := toEndomorphism R L (weightSpaceOf M χ x) x
+  have h_comm : Commute f g := commute_toEndomorphism_of_mem_center_left _ hzc x
+  have hg : _root_.IsNilpotent (g - algebraMap R _ χ) :=
+    (toEndomorphism R L M x).isNilpotent_restrict_iSup_sub_algebraMap χ
+  rw [traceForm_apply_apply, LinearMap.trace_comp_eq_mul_of_commute_of_isNilpotent χ h_comm hg, hz,
+    mul_zero]
+
+/-- A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian. -/
+lemma isLieAbelian_of_ker_traceForm_eq_bot (h : LinearMap.ker (traceForm R L M) = ⊥) :
+    IsLieAbelian L := by
+  simpa only [← disjoint_lowerCentralSeries_maxTrivSubmodule_iff R L L, disjoint_iff_inf_le,
+    LieIdeal.coe_to_lieSubalgebra_to_submodule, LieSubmodule.coeSubmodule_eq_bot_iff, h]
+    using lowerCentralSeries_one_inf_center_le_ker_traceForm R L M
+
 end LieModule
 
 namespace LieSubmodule
@@ -316,6 +384,13 @@ instance isSemisimple [IsDomain R] [IsPrincipalIdealRing R] : IsSemisimple R L :
 
 -- TODO: formalize a positive-characteristic counterexample to the above instance
 
+instance instIsLieAbelian_of_isCartanSubalgebra
+    [IsDomain R] [IsPrincipalIdealRing R] [IsArtinian R L]
+    (H : LieSubalgebra R L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable R H L] :
+    IsLieAbelian H :=
+  LieModule.isLieAbelian_of_ker_traceForm_eq_bot R H L <|
+    ker_restrictBilinear_of_isCartanSubalgebra_eq_bot R L H
+
 end IsKilling
 
 end LieAlgebra

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -325,6 +325,7 @@ noncomputable def nilpotencyLength : ℕ :=
   sInf {k | lowerCentralSeries R L M k = ⊥}
 #align lie_module.nilpotency_length LieModule.nilpotencyLength
 
+@[simp]
 theorem nilpotencyLength_eq_zero_iff [IsNilpotent R L M] :
     nilpotencyLength R L M = 0 ↔ Subsingleton M := by
   let s := {k | lowerCentralSeries R L M k = ⊥}
@@ -350,6 +351,19 @@ theorem nilpotencyLength_eq_succ_iff (k : ℕ) :
   exact Nat.sInf_upward_closed_eq_succ_iff hs k
 #align lie_module.nilpotency_length_eq_succ_iff LieModule.nilpotencyLength_eq_succ_iff
 
+@[simp]
+theorem nilpotencyLength_eq_one_iff [Nontrivial M] :
+    nilpotencyLength R L M = 1 ↔ IsTrivial L M := by
+  rw [nilpotencyLength_eq_succ_iff, ← trivial_iff_lower_central_eq_bot]
+  simp
+
+theorem isTrivial_of_nilpotencyLength_le_one [IsNilpotent R L M] (h : nilpotencyLength R L M ≤ 1) :
+    IsTrivial L M := by
+  nontriviality M
+  cases' Nat.le_one_iff_eq_zero_or_eq_one.mp h with h h
+  · rw [nilpotencyLength_eq_zero_iff] at h; infer_instance
+  · rwa [nilpotencyLength_eq_one_iff] at h
+
 /-- Given a non-trivial nilpotent Lie module `M` with lower central series
 `M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is the `k-1`th term in the lower central series (the last
 non-trivial term).
@@ -381,6 +395,35 @@ theorem nontrivial_lowerCentralSeriesLast [Nontrivial M] [IsNilpotent R L M] :
     exact h.2
 #align lie_module.nontrivial_lower_central_series_last LieModule.nontrivial_lowerCentralSeriesLast
 
+theorem lowerCentralSeriesLast_le_of_not_isTrivial [IsNilpotent R L M] (h : ¬ IsTrivial L M) :
+    lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 := by
+  rw [lowerCentralSeriesLast]
+  replace h : 1 < nilpotencyLength R L M := by
+    by_contra contra
+    have := isTrivial_of_nilpotencyLength_le_one R L M (not_lt.mp contra)
+    contradiction
+  cases' hk : nilpotencyLength R L M with k <;> rw [hk] at h
+  · contradiction
+  · exact antitone_lowerCentralSeries _ _ _ (Nat.lt_succ.mp h)
+
+/-- For a nilpotent Lie module `M` of a Lie algebra `L`, the first term in the lower central series
+of `M` contains a non-zero element on which `L` acts trivially unless the entire action is trivial.
+
+Taking `M = L`, this provides a useful characterisation of Abelian-ness for nilpotent Lie
+algebras. -/
+lemma disjoint_lowerCentralSeries_maxTrivSubmodule_iff [IsNilpotent R L M] :
+    Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M) ↔ IsTrivial L M := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by simp⟩
+  nontriviality M
+  by_contra contra
+  have : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M :=
+    le_inf_iff.mpr ⟨lowerCentralSeriesLast_le_of_not_isTrivial R L M contra,
+      lowerCentralSeriesLast_le_max_triv R L M⟩
+  suffices ¬ Nontrivial (lowerCentralSeriesLast R L M) by
+    exact this (nontrivial_lowerCentralSeriesLast R L M)
+  rw [h.eq_bot, le_bot_iff] at this
+  exact this ▸ not_nontrivial _
+
 theorem nontrivial_max_triv_of_isNilpotent [Nontrivial M] [IsNilpotent R L M] :
     Nontrivial (maxTrivSubmodule R L M) :=
   Set.nontrivial_mono (lowerCentralSeriesLast_le_max_triv R L M)

Mathlib/Algebra/Lie/Semisimple.lean

@@ -98,7 +98,7 @@ theorem subsingleton_of_semisimple_lie_abelian [IsSemisimple R L] [h : IsLieAbel
 #align lie_algebra.subsingleton_of_semisimple_lie_abelian LieAlgebra.subsingleton_of_semisimple_lie_abelian
 
 theorem abelian_radical_of_semisimple [IsSemisimple R L] : IsLieAbelian (radical R L) := by
-  rw [IsSemisimple.semisimple]; exact isLieAbelian_bot R L
+  rw [IsSemisimple.semisimple]; infer_instance
 #align lie_algebra.abelian_radical_of_semisimple LieAlgebra.abelian_radical_of_semisimple
 
 /-- The two properties shown to be equivalent here are possible definitions for a Lie algebra

Mathlib/Algebra/Lie/Solvable.lean

@@ -351,7 +351,7 @@ theorem abelian_derivedAbelianOfIdeal (I : LieIdeal R L) :
     IsLieAbelian (derivedAbelianOfIdeal I) := by
   dsimp only [derivedAbelianOfIdeal]
   cases' h : derivedLengthOfIdeal R L I with k
-  · exact isLieAbelian_bot R L
+  · infer_instance
   · rw [derivedSeries_of_derivedLength_succ] at h; exact h.1
 #align lie_algebra.abelian_derived_abelian_of_ideal LieAlgebra.abelian_derivedAbelianOfIdeal
 

Mathlib/Algebra/Lie/Submodule.lean

@@ -546,6 +546,14 @@ theorem codisjoint_iff_coe_toSubmodule :
   rw [codisjoint_iff, codisjoint_iff, ← coe_toSubmodule_eq_iff, sup_coe_toSubmodule,
     top_coeSubmodule, ← codisjoint_iff]
 
+theorem independent_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L M} :
+    CompleteLattice.Independent N ↔ CompleteLattice.Independent fun i ↦ (N i : Submodule R M) := by
+  simp [CompleteLattice.independent_def, disjoint_iff_coe_toSubmodule]
+
+theorem iSup_eq_top_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L M} :
+    ⨆ i, N i = ⊤ ↔ ⨆ i, (N i : Submodule R M) = ⊤ := by
+  rw [← iSup_coe_toSubmodule, ← top_coeSubmodule (L := L), coe_toSubmodule_eq_iff]
+
 instance : AddCommMonoid (LieSubmodule R L M) where
   add := (· ⊔ ·)
   add_assoc _ _ _ := sup_assoc

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -574,6 +574,21 @@ lemma independent_weightSpace [NoZeroSMulDivisors R M] :
     rintro - ⟨u, hu, rfl⟩
     exact LieSubmodule.mapsTo_pow_toEndomorphism_sub_algebraMap _ hu
 
+lemma independent_weightSpaceOf [NoZeroSMulDivisors R M] (x : L) :
+    CompleteLattice.Independent fun (χ : R) ↦ weightSpaceOf M χ x := by
+  rw [LieSubmodule.independent_iff_coe_toSubmodule]
+  exact (toEndomorphism R L M x).independent_generalizedEigenspace
+
+lemma finite_weightSpaceOf_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) :
+    {χ : R | weightSpaceOf M χ x ≠ ⊥}.Finite :=
+  CompleteLattice.WellFounded.finite_ne_bot_of_independent
+    (LieSubmodule.wellFounded_of_noetherian R L M) (independent_weightSpaceOf R L M x)
+
+lemma finite_weightSpace_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] :
+    {χ : L → R | weightSpace M χ ≠ ⊥}.Finite :=
+  CompleteLattice.WellFounded.finite_ne_bot_of_independent
+    (LieSubmodule.wellFounded_of_noetherian R L M) (independent_weightSpace R L M)
+
 /-- A Lie module `M` of a Lie algebra `L` is triangularizable if the endomorhpism of `M` defined by
 any `x : L` is triangularizable. -/
 class IsTriangularizable : Prop :=

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -295,6 +295,28 @@ lemma mapsTo_iSup_generalizedEigenspace_of_comm {f g : End R M} (h : Commute f g
   rintro x ⟨k, hk⟩
   exact ⟨k, f.mapsTo_generalizedEigenspace_of_comm h μ k hk⟩
 
+/-- The restriction of `f - μ • 1` to the `k`-fold generalized `μ`-eigenspace is nilpotent. -/
+lemma isNilpotent_restrict_sub_algebraMap (f : End R M) (μ : R) (k : ℕ)
+    (h : MapsTo (f - algebraMap R (End R M) μ)
+      (f.generalizedEigenspace μ k) (f.generalizedEigenspace μ k) :=
+      mapsTo_generalizedEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ k) :
+    IsNilpotent ((f - algebraMap R (End R M) μ).restrict h) := by
+  use k
+  ext
+  simp [LinearMap.restrict_apply, LinearMap.pow_restrict _]
+
+/-- The restriction of `f - μ • 1` to the generalized `μ`-eigenspace is nilpotent. -/
+lemma isNilpotent_restrict_iSup_sub_algebraMap [IsNoetherian R M] (f : End R M) (μ : R)
+    (h : MapsTo (f - algebraMap R (End R M) μ)
+      ↑(⨆ k, f.generalizedEigenspace μ k) ↑(⨆ k, f.generalizedEigenspace μ k) :=
+      mapsTo_iSup_generalizedEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ) :
+    IsNilpotent ((f - algebraMap R (End R M) μ).restrict h) := by
+  obtain ⟨l, hl⟩ : ∃ l, ⨆ k, f.generalizedEigenspace μ k = f.generalizedEigenspace μ l :=
+    ⟨_, maximalGeneralizedEigenspace_eq f μ⟩
+  use l
+  ext ⟨x, hx⟩
+  simpa [hl, LinearMap.restrict_apply, LinearMap.pow_restrict _] using hx
+
 lemma disjoint_generalizedEigenspace [NoZeroSMulDivisors R M]
     (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) (k l : ℕ) :
     Disjoint (f.generalizedEigenspace μ₁ k) (f.generalizedEigenspace μ₂ l) := by