feat(algebra/lie/nilpotent): basic lemmas about nilpotency for Lie su…

…balgebras of associative algebras (#8090)

The main lemma is: `lie_algebra.is_nilpotent_ad_of_is_nilpotent` which is the first step in proving Engel's theorem.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/basic.lean

@@ -10,6 +10,7 @@ import linear_algebra.tensor_product
 import ring_theory.subring
 import deprecated.subring
 import algebra.opposites
+import algebra.iterate_hom
 
 /-!
 # Algebra over Commutative Semiring
@@ -1173,6 +1174,10 @@ def lmul_left_right (vw: A × A) : A →ₗ[R] A :=
 def lmul' : A ⊗[R] A →ₗ[R] A :=
 tensor_product.lift (lmul R A).to_linear_map
 
+lemma commute_lmul_left_right (a b : A) :
+  commute (lmul_left R a) (lmul_right R b) :=
+by { ext c, exact (mul_assoc a c b).symm, }
+
 variables {R A}
 
 @[simp] lemma lmul_apply (p q : A) : lmul R A p q = p * q := rfl
@@ -1195,6 +1200,38 @@ by { ext, simp only [linear_map.id_coe, mul_one, id.def, lmul_right_apply] }
   lmul_right R (a * b) = (lmul_right R b).comp (lmul_right R a) :=
 by { ext, simp only [lmul_right_apply, linear_map.comp_apply, mul_assoc] }
 
+@[simp] lemma lmul_left_zero_eq_zero :
+  lmul_left R (0 : A) = 0 :=
+(lmul R A).map_zero
+
+@[simp] lemma lmul_right_zero_eq_zero :
+  lmul_right R (0 : A) = 0 :=
+(lmul R A).to_linear_map.flip.map_zero
+
+@[simp] lemma lmul_left_eq_zero_iff (a : A) :
+  lmul_left R a = 0 ↔ a = 0 :=
+begin
+  split; intros h,
+  { rw [← mul_one a, ← lmul_left_apply a 1, h, linear_map.zero_apply], },
+  { rw h, exact lmul_left_zero_eq_zero, },
+end
+
+@[simp] lemma lmul_right_eq_zero_iff (a : A) :
+  lmul_right R a = 0 ↔ a = 0 :=
+begin
+  split; intros h,
+  { rw [← one_mul a, ← lmul_right_apply a 1, h, linear_map.zero_apply], },
+  { rw h, exact lmul_right_zero_eq_zero, },
+end
+
+@[simp] lemma pow_lmul_left (a : A) (n : ℕ) :
+  (lmul_left R a) ^ n = lmul_left R (a ^ n) :=
+((lmul R A).map_pow a n).symm
+
+@[simp] lemma pow_lmul_right (a : A) (n : ℕ) :
+  (lmul_right R a) ^ n = lmul_right R (a ^ n) :=
+linear_map.coe_injective $ ((lmul_right R a).coe_pow n).symm ▸ (mul_right_iterate a n)
+
 @[simp] lemma lmul'_apply {x y : A} : lmul' R (x ⊗ₜ y) = x * y :=
 by simp only [algebra.lmul', tensor_product.lift.tmul, alg_hom.to_linear_map_apply, lmul_apply]
 

src/algebra/lie/nilpotent.lean

@@ -5,6 +5,7 @@ Authors: Oliver Nash
 -/
 import algebra.lie.solvable
 import linear_algebra.eigenspace
+import ring_theory.nilpotent
 
 /-!
 # Nilpotent Lie algebras
@@ -199,3 +200,33 @@ instance [h : lie_algebra.is_nilpotent R L] : lie_algebra.is_nilpotent R (⊤ :
 lie_subalgebra.top_equiv_self.nilpotent_iff_equiv_nilpotent.mpr h
 
 end nilpotent_algebras
+
+section of_associative
+
+variables (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A]
+
+lemma lie_algebra.ad_nilpotent_of_nilpotent {a : A} (h : is_nilpotent a) :
+  is_nilpotent (lie_algebra.ad R A a) :=
+begin
+  rw lie_algebra.ad_eq_lmul_left_sub_lmul_right,
+  have hl : is_nilpotent (algebra.lmul_left R a), { rwa algebra.is_nilpotent_lmul_left_iff, },
+  have hr : is_nilpotent (algebra.lmul_right R a), { rwa algebra.is_nilpotent_lmul_right_iff, },
+  exact (algebra.commute_lmul_left_right R a a).is_nilpotent_sub hl hr,
+end
+
+variables {R}
+
+lemma lie_subalgebra.is_nilpotent_ad_of_is_nilpotent_ad {L : Type v} [lie_ring L] [lie_algebra R L]
+  (K : lie_subalgebra R L) {x : K} (h : is_nilpotent (lie_algebra.ad R L ↑x)) :
+  is_nilpotent (lie_algebra.ad R K x) :=
+begin
+  obtain ⟨n, hn⟩ := h,
+  use n,
+  exact linear_map.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn,
+end
+
+lemma lie_algebra.is_nilpotent_ad_of_is_nilpotent {L : lie_subalgebra R A} {x : L}
+  (h : is_nilpotent (x : A)) : is_nilpotent (lie_algebra.ad R L x) :=
+L.is_nilpotent_ad_of_is_nilpotent_ad $ lie_algebra.ad_nilpotent_of_nilpotent R h
+
+end of_associative

src/algebra/lie/of_associative.lean

@@ -122,6 +122,22 @@ def lie_algebra.ad : L →ₗ⁅R⁆ module.End R L := lie_module.to_endomorphis
 
 @[simp] lemma lie_algebra.ad_apply (x y : L) : lie_algebra.ad R L x y = ⁅x, y⁆ := rfl
 
+open lie_algebra
+
+lemma lie_algebra.ad_eq_lmul_left_sub_lmul_right (A : Type v) [ring A] [algebra R A] :
+  (ad R A : A → module.End R A) = algebra.lmul_left R - algebra.lmul_right R :=
+by { ext a b, simp [lie_ring.of_associative_ring_bracket], }
+
+variables {R L}
+
+lemma lie_subalgebra.ad_comp_incl_eq (K : lie_subalgebra R L) (x : K) :
+  (ad R L ↑x).comp (K.incl : K →ₗ[R] L) = (K.incl : K →ₗ[R] L).comp (ad R K x) :=
+begin
+  ext y,
+  simp only [ad_apply, lie_hom.coe_to_linear_map, lie_subalgebra.coe_incl, linear_map.coe_comp,
+    lie_subalgebra.coe_bracket, function.comp_app],
+end
+
 end adjoint_action
 
 /-- A subalgebra of an associative algebra is a Lie subalgebra of the associated Lie algebra. -/

src/linear_algebra/basic.lean

@@ -310,6 +310,17 @@ begin
       ← linear_map.comp_assoc, h, linear_map.comp_assoc, linear_map.mul_eq_comp], },
 end
 
+lemma submodule_pow_eq_zero_of_pow_eq_zero {N : submodule R M}
+  {g : module.End R N} {G : module.End R M} (h : G.comp N.subtype = N.subtype.comp g)
+  {k : ℕ} (hG : G^k = 0) : g^k = 0 :=
+begin
+  ext m,
+  have hg : N.subtype.comp (g^k) m = 0,
+  { rw [← commute_pow_left_of_commute h, hG, zero_comp, zero_apply], },
+  simp only [submodule.subtype_apply, comp_app, submodule.coe_eq_zero, coe_comp] at hg,
+  rw [hg, linear_map.zero_apply],
+end
+
 lemma coe_pow (f : M →ₗ[R] M) (n : ℕ) : ⇑(f^n) = (f^[n]) :=
 by { ext m, apply pow_apply, }
 

src/ring_theory/nilpotent.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import data.nat.choose.sum
+import algebra.algebra.basic
 
 /-!
 # Nilpotent elements
@@ -19,7 +20,7 @@ import data.nat.choose.sum
 
 -/
 
-universes u
+universes u v
 
 variables {R : Type u} {x y : R}
 
@@ -101,3 +102,25 @@ end
 end ring
 
 end commute
+
+namespace algebra
+
+variables (R) {A : Type v} [comm_semiring R] [semiring A] [algebra R A]
+
+@[simp] lemma is_nilpotent_lmul_left_iff (a : A) :
+  is_nilpotent (lmul_left R a) ↔ is_nilpotent a :=
+begin
+  split; rintros ⟨n, hn⟩; use n;
+  simp only [lmul_left_eq_zero_iff, pow_lmul_left] at ⊢ hn;
+  exact hn,
+end
+
+@[simp] lemma is_nilpotent_lmul_right_iff (a : A) :
+  is_nilpotent (lmul_right R a) ↔ is_nilpotent a :=
+begin
+  split; rintros ⟨n, hn⟩; use n;
+  simp only [lmul_right_eq_zero_iff, pow_lmul_right] at ⊢ hn;
+  exact hn,
+end
+
+end algebra