feat: the Geck Construction yields trace-free matrices (#27831)

This will be used with `LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful` (and a proof of irreducibility) to prove semisimplicity.

Author: ocfnash

Mathlib/Algebra/Lie/Semisimple/Lemmas.lean

@@ -19,20 +19,16 @@ This file is a home for lemmas about semisimple and reductive Lie algebras.
 
 ## TODO
 
-* It appears that the lemmas in this file may hold for any principal ideal domain (of
-  characteristic zero) instead of a field. The plan would be to define the nilradical of a Lie
-  algebra (currently missing) and use it with
-  `LieModule.exists_nontrivial_weightSpace_of_isNilpotent` instead of using the solvable radical
-  with `LieModule.exists_nontrivial_weightSpace_of_isSolvable`, as below. The conclusion of
-  `LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful` would then make a statement
-  that the nilradical vanishes and one would prove elsewhere that vanishing nilradical is
-  equivalent to `HasCentralRadical`.
+* Introduce a `Prop`-valued typeclass `LieModule.IsTracefree` stating
+  `(toEnd R L M).range ≤ LieAlgebra.derivedSeries R (Module.End R M) 1`, prove
+  `f ∈ LieAlgebra.derivedSeries k (Module.End k V) 1 ↔ LinearMap.trace k _ f = 0`, and restate
+  `LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful` using `LieModule.IsTracefree`.
 
 -/
 
 namespace LieAlgebra
 
-open LieModule LieSubmodule Module
+open LieModule LieSubmodule Module Set
 
 variable (k L M : Type*) [Field k] [CharZero k]
   [LieRing L] [LieAlgebra k L] [Module.Finite k L]
@@ -76,4 +72,18 @@ theorem hasTrivialRadical_of_isIrreducible_of_isFaithful
   suffices t = 0 by simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), ← ht, this]
   simpa [this, ← ht] using h
 
+variable {k L M}
+variable {R : Type*} [CommRing R] [IsReduced R] [LieAlgebra R L] [Module R M] [LieModule R L M]
+
+open LinearMap in
+lemma trace_toEnd_eq_zero {s : Set L} (hs : ∀ x ∈ s, _root_.IsNilpotent (toEnd R _ M x))
+    {x : L} (hx : x ∈ LieSubalgebra.lieSpan R L s) :
+    trace R _ (toEnd R _ M x) = 0 := by
+  induction hx using LieSubalgebra.lieSpan_induction with
+  | mem u hu => simpa using isNilpotent_trace_of_isNilpotent (hs u hu)
+  | zero => simp
+  | add u v _ _ hu hv => simp [hu, hv]
+  | smul t u _ hu => simp [hu]
+  | lie u v _ _ _ _ => simp
+
 end LieAlgebra

Mathlib/Data/Matrix/Mul.lean

@@ -934,6 +934,20 @@ lemma vecMul_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R}
   intro x y hxy
   simpa [hBl] using congrArg B.vecMul hxy
 
+lemma pow_row_eq_zero_of_le [Fintype n] [DecidableEq n] {M : Matrix n n R} {k l : ℕ} {i : n}
+    (h : (M ^ k).row i = 0) (h' : k ≤ l) :
+    (M ^ l).row i = 0 := by
+  replace h' : l = k + (l - k) := by omega
+  rw [← single_one_vecMul] at h ⊢
+  rw [h', pow_add, ← vecMul_vecMul, h, zero_vecMul]
+
+lemma pow_col_eq_zero_of_le [Fintype n] [DecidableEq n] {M : Matrix n n R} {k l : ℕ} {i : n}
+    (h : (M ^ k).col i = 0) (h' : k ≤ l) :
+    (M ^ l).col i = 0 := by
+  replace h' : l = (l - k) + k := by omega
+  rw [← mulVec_single_one] at h ⊢
+  rw [h', pow_add, ← mulVec_mulVec, h, mulVec_zero]
+
 end Semiring
 
 section CommSemiring

Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

@@ -3,10 +3,13 @@ Copyright (c) 2025 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import Mathlib.Algebra.Lie.Matrix
 import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Algebra.Lie.Semisimple.Lemmas
 import Mathlib.Algebra.Lie.Sl2
 import Mathlib.LinearAlgebra.RootSystem.CartanMatrix
 import Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
+import Mathlib.RingTheory.Finiteness.Nilpotent
 
 /-!
 # Geck's construction of a Lie algebra associated to a root system
@@ -64,7 +67,7 @@ namespace RootPairing.GeckConstruction
 
 variable {ι R M N : Type*} [Finite ι] [CommRing R] [IsDomain R] [CharZero R]
   [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
-  {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base}
+  {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base}
 
 /-- Part of an `sl₂` triple used in Geck's construction of a Lie algebra from a root system. -/
 def e (i : b.support) :
@@ -117,7 +120,7 @@ variable {b}
 attribute [local simp] Ring.lie_def Matrix.mul_apply Matrix.one_apply Matrix.diagonal_apply
 
 omit [Finite ι] [IsDomain R] [CharZero R] [P.IsCrystallographic] in
-lemma ω_mul_ω [DecidableEq ι] [Fintype ι] :
+@[simp] lemma ω_mul_ω [DecidableEq ι] [Fintype ι] :
     ω b * ω b = 1 := by
   ext (k | k) (l | l) <;>
   simp [ω, -indexNeg_neg]
@@ -478,4 +481,115 @@ lemma lie_e_f_ne [P.IsNotG2] :
 
 end lie_e_f_ne
 
+variable [DecidableEq ι]
+
+/-- An auxiliary lemma en route to `RootPairing.GeckConstruction.isNilpotent_e`. -/
+private lemma isNilpotent_e_aux {j : ι} (n : ℕ) (h : letI _i := P.indexNeg; j ≠ -i) :
+    (e i ^ n).col (.inr j) = 0 ∨
+      ∃ (k : ι) (x : ℕ), P.root k = P.root j + n • P.root i ∧
+        (e i ^ n).col (.inr j) = x • Pi.single (.inr k) 1 := by
+  have _i : NoZeroSMulDivisors ℤ M := by have := P.reflexive_left; exact .int_of_charZero R M
+  letI _i := P.indexNeg
+  have aux (n : ℕ) : (e i ^ (n + 1)).col (.inr j) = (e i).mulVec ((e i ^ n).col (.inr j)) := by
+    rw [pow_succ', ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]; simp
+  induction n with
+  | zero => exact Or.inr ⟨j, 1, by simp, by ext; simp [Pi.single_apply]⟩
+  | succ n ih =>
+    rcases ih with hn | ⟨k, x, hk₁, hk₂⟩
+    · left; simp [aux, hn]
+    rw [aux, hk₂, Matrix.mulVec_smul]
+    have hki : k ≠ -i := by
+      rintro rfl
+      replace hk₁ : P.root (-j) = (n + 1) • P.root i := by
+        simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self, neg_eq_iff_add_eq_zero,
+          add_smul, one_smul] at hk₁ ⊢
+        rw [← hk₁]
+        module
+      rcases n.eq_zero_or_pos with rfl | hn
+      · apply h
+        rw [zero_add, one_smul, EmbeddingLike.apply_eq_iff_eq] at hk₁
+        simp [← hk₁, -indexNeg_neg]
+      · have _i : (n + 1).AtLeastTwo := ⟨by omega⟩
+        exact P.nsmul_notMem_range_root (n := n + 1) (i := i) ⟨-j, hk₁⟩
+    by_cases hij : P.root j + (n + 1) • P.root i ∈ range P.root
+    · obtain ⟨l, hl⟩ := hij
+      right
+      refine ⟨l, x * (P.chainBotCoeff i k + 1), hl, ?_⟩
+      ext (m | m)
+      · simp [e, -indexNeg_neg, hki]
+      · rcases eq_or_ne m l with rfl | hml
+        · replace hl : P.root m = P.root i + P.root k := by rw [hl, hk₁]; module
+          simp [e, -indexNeg_neg, hl, mul_add]
+        · replace hl : P.root m ≠ P.root i + P.root k :=
+            fun contra ↦ hml (P.root.injective <| by rw [hl, contra, hk₁]; module)
+          simp [e, -indexNeg_neg, hml, hl]
+    · left
+      ext (l | l)
+      · simp [e, -indexNeg_neg, hki]
+      · replace hij : P.root l ≠ P.root i + P.root k :=
+          fun contra ↦ hij ⟨l, by rw [contra, hk₁]; module⟩
+        simp [e, -indexNeg_neg, hij]
+
+lemma isNilpotent_e :
+    IsNilpotent (e i) := by
+  classical
+  have _i : NoZeroSMulDivisors ℤ M := by have := P.reflexive_left; exact .int_of_charZero R M
+  letI _i := P.indexNeg
+  rw [Matrix.isNilpotent_iff_forall_col]
+  have case_inl (j : b.support) : (e i ^ 2).col (Sum.inl j) = 0 := by
+    ext (k | k)
+    · simp [e, sq, ne_neg P i, -indexNeg_neg]
+    · have aux : ∀ x : ι, x ∈ Finset.univ → ¬ (x = i ∧ P.root k = P.root i + P.root x) := by
+        suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul]
+        exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩
+      simp [e, sq, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux]
+  rintro (j | j)
+  · exact ⟨2, case_inl j⟩
+  · by_cases hij : j = -i
+    · use 2 + 1
+      replace hij : (e i).col (Sum.inr j) = Pi.single (Sum.inl i) 1 := by
+        ext (k | k)
+        · simp [e, -indexNeg_neg, Pi.single_apply, hij]
+        · have hk : P.root k ≠ P.root i + P.root j := by simp [hij, P.ne_zero k]
+          simp [e, -indexNeg_neg, hk]
+      rw [pow_succ, ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]
+      simp [hij, case_inl i]
+    use P.chainTopCoeff i j + 1
+    rcases isNilpotent_e_aux i (P.chainTopCoeff i j + 1) hij with this | ⟨k, x, hk₁, -⟩
+    · assumption
+    exfalso
+    replace hk₁ : P.root j + (P.chainTopCoeff i j + 1) • P.root i ∈ range P.root := ⟨k, hk₁⟩
+    have hij' : LinearIndependent R ![P.root i, P.root j] := by
+      apply IsReduced.linearIndependent P ?_ ?_
+      · rintro rfl
+        apply P.nsmul_notMem_range_root (n := P.chainTopCoeff i i + 2) (i := i)
+        convert hk₁ using 1
+        module
+      · contrapose! hij
+        rw [root_eq_neg_iff] at hij
+        rw [hij, ← indexNeg_neg, neg_neg]
+    rw [root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'] at hk₁
+    omega
+
+lemma isNilpotent_f :
+    IsNilpotent (f i) := by
+  obtain ⟨n, hn⟩ := isNilpotent_e i
+  suffices (ω b) * (f i ^ n) = 0 from ⟨n, by simpa [← mul_assoc] using congr_arg (ω b * ·) this⟩
+  suffices (ω b) * (f i ^ n) = (e i ^ n) * (ω b) by simp [this, hn]
+  clear hn
+  induction n with
+  | zero => simp
+  | succ n ih => rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
+
+open LinearMap LieModule in
+/-- This is the main result of lemma 4.1 from [Geck](Geck2017). -/
+lemma trace_toEnd_eq_zero (x : lieAlgebra b) :
+    trace R _ (toEnd R _ (b.support ⊕ ι → R) x) = 0 := by
+  obtain ⟨x, hx⟩ := x
+  suffices trace R _ x.toLin' = 0 by simpa
+  refine LieAlgebra.trace_toEnd_eq_zero ?_ hx
+  rintro - (⟨i, rfl⟩ | ⟨i, rfl⟩)
+  · simpa using isNilpotent_e i
+  · simpa using isNilpotent_f i
+
 end RootPairing.GeckConstruction

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

@@ -175,6 +175,22 @@ end ListMultiset
 
 end ConditionallyCompleteLinearOrder
 
+namespace Finite
+
+variable [Finite ι] [ConditionallyCompleteLattice α] (f : ι → α)
+
+lemma le_ciSup (i : ι) : f i ≤ ⨆ j, f j := by
+  suffices BddAbove (range f) from _root_.le_ciSup this i
+  let : Fintype ι := Fintype.ofFinite ι
+  use Finset.sup' Finset.univ ⟨i, Finset.mem_univ i⟩ f
+  simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff]
+  exact fun j ↦ Finset.le_sup' f <| Finset.mem_univ j
+
+lemma ciInf_le (i : ι) : ⨅ j, f j ≤ f i :=
+  le_ciSup (α := αᵒᵈ) f i
+
+end Finite
+
 /-!
 ### Relation between `sSup` / `sInf` and `Finset.sup'` / `Finset.inf'`
 

Mathlib/RingTheory/Finiteness/Nilpotent.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Mathlib.RingTheory.Finiteness.Defs
-import Mathlib.RingTheory.Nilpotent.Defs
+import Mathlib.RingTheory.Finiteness.Basic
+import Mathlib.RingTheory.Nilpotent.Lemmas
 
 /-!
 # Nilpotent maps on finite modules
@@ -26,3 +26,36 @@ theorem Module.End.isNilpotent_iff_of_finite [Module.Finite R M] {f : End R M} :
   | zero => simp
   | add => simp_all
   | smul => simp_all
+
+namespace Matrix
+
+open scoped Matrix
+
+variable {ι : Type*} [DecidableEq ι] [Fintype ι] {A : Matrix ι ι R}
+
+@[simp]
+theorem isNilpotent_transpose_iff :
+    IsNilpotent Aᵀ ↔ IsNilpotent A := by
+  simp_rw [IsNilpotent, ← transpose_pow, transpose_eq_zero]
+
+theorem isNilpotent_iff :
+    IsNilpotent A ↔ ∀ v, ∃ n : ℕ, A ^ n *ᵥ v = 0 := by
+  simp_rw [← isNilpotent_toLin'_iff, Module.End.isNilpotent_iff_of_finite, ← toLin'_pow,
+    toLin'_apply]
+
+theorem isNilpotent_iff_forall_row :
+    IsNilpotent A ↔ ∀ i, ∃ n : ℕ, (A ^ n).row i = 0 := by
+  rw [← isNilpotent_transpose_iff, isNilpotent_iff]
+  refine ⟨fun h i ↦ ?_, fun h v ↦ ?_⟩
+  · obtain ⟨n, hn⟩ := h (Pi.single i 1)
+    exact ⟨n, by simpa [← transpose_pow] using hn⟩
+  · choose n hn using h
+    suffices ∀ i, (A ^ ⨆ j, n j) i = 0 from ⟨⨆ j, n j, by simp [mulVec_eq_sum, this]⟩
+    exact fun i ↦ pow_row_eq_zero_of_le (hn i) (Finite.le_ciSup n i)
+
+theorem isNilpotent_iff_forall_col :
+    IsNilpotent A ↔ ∀ i, ∃ n : ℕ, (A ^ n).col i = 0 := by
+  rw [← isNilpotent_transpose_iff, isNilpotent_iff_forall_row]
+  simp_rw [← transpose_pow, row_transpose]
+
+end Matrix

Mathlib/RingTheory/Nilpotent/Lemmas.lean

@@ -93,6 +93,14 @@ lemma isNilpotent_toMatrix_iff (b : Basis ι R M) (f : M →ₗ[R] M) :
 
 end LinearMap
 
+@[simp]
+lemma Matrix.isNilpotent_toLin'_iff {ι : Type*} [DecidableEq ι] [Fintype ι] [CommSemiring R]
+    (A : Matrix ι ι R) :
+    IsNilpotent A.toLin' ↔ IsNilpotent A := by
+  have : A.toLin'.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι) = A := LinearMap.toMatrix'_toLin' A
+  conv_rhs => rw [← this]
+  rw [LinearMap.isNilpotent_toMatrix_iff]
+
 namespace Module.End
 
 section