feat: generalise results about Lie module weight spans from Abelian t…

…o nilpotent Lie algebras (#8718)

Mathlib/Algebra/Lie/Killing.lean

@@ -34,7 +34,7 @@ We define the trace / Killing form in this file and prove some basic properties.
    form on `L` via the trace form construction.
  * `LieAlgebra.IsKilling`: a typeclass encoding the fact that a Lie algebra has a non-singular
    Killing form.
- * `LieAlgebra.IsKilling.ker_restrictBilinear_of_isCartanSubalgebra_eq_bot`: if the Killing form of
+ * `LieAlgebra.IsKilling.ker_restrictBilinear_eq_bot_of_isCartanSubalgebra`: if the Killing form of
    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.
@@ -60,7 +60,7 @@ attribute [local instance] Module.free_of_finite_type_torsion_free'
 local notation "φ" => LieModule.toEndomorphism R L M
 
 open LinearMap (trace)
-open Set BigOperators
+open Set BigOperators FiniteDimensional
 
 namespace LieModule
 
@@ -117,6 +117,36 @@ lemma traceForm_apply_lie_apply' (x y z : L) :
   apply LinearMap.isNilpotent_trace_of_isNilpotent
   exact isNilpotent_toEndomorphism_of_isNilpotent₂ R L M x y
 
+@[simp]
+lemma trace_toEndomorphism_weightSpace [IsDomain R] [IsPrincipalIdealRing R]
+    [LieAlgebra.IsNilpotent R L] (χ : L → R) (x : L) :
+    trace R _ (toEndomorphism R L (weightSpace M χ) x) = finrank R (weightSpace M χ) • χ x := by
+  suffices _root_.IsNilpotent ((toEndomorphism R L (weightSpace M χ) x) - χ x • LinearMap.id) by
+    replace this := (LinearMap.isNilpotent_trace_of_isNilpotent this).eq_zero
+    rwa [map_sub, map_smul, LinearMap.trace_id, sub_eq_zero, smul_eq_mul, mul_comm,
+      ← nsmul_eq_mul] at this
+  rw [← Module.algebraMap_end_eq_smul_id]
+  exact isNilpotent_toEndomorphism_sub_algebraMap M χ x
+
+@[simp]
+lemma traceForm_weightSpace_eq [IsDomain R] [IsPrincipalIdealRing R]
+    [LieAlgebra.IsNilpotent R L] [IsNoetherian R M] [LinearWeights R L M] (χ : L → R) (x y : L) :
+    traceForm R L (weightSpace M χ) x y = finrank R (weightSpace M χ) • (χ x * χ y) := by
+  set d := finrank R (weightSpace M χ)
+  have h₁ : χ y • d • χ x - χ y • χ x • (d : R) = 0 := by simp [mul_comm (χ x)]
+  have h₂ : χ x • d • χ y = d • (χ x * χ y) := by
+    simpa [nsmul_eq_mul, smul_eq_mul] using mul_left_comm (χ x) d (χ y)
+  have := traceForm_eq_zero_of_isNilpotent R L (shiftedWeightSpace R L M χ)
+  replace this := LinearMap.congr_fun (LinearMap.congr_fun this x) y
+  rwa [LinearMap.zero_apply, LinearMap.zero_apply, traceForm_apply_apply,
+    shiftedWeightSpace.toEndomorphism_eq, shiftedWeightSpace.toEndomorphism_eq,
+    ← LinearEquiv.conj_comp, LinearMap.trace_conj', LinearMap.comp_sub, LinearMap.sub_comp,
+    LinearMap.sub_comp, map_sub, map_sub, map_sub, LinearMap.comp_smul, LinearMap.smul_comp,
+    LinearMap.comp_id, LinearMap.id_comp, LinearMap.map_smul, LinearMap.map_smul,
+    trace_toEndomorphism_weightSpace, trace_toEndomorphism_weightSpace,
+    LinearMap.comp_smul, LinearMap.smul_comp, LinearMap.id_comp, map_smul, map_smul,
+    LinearMap.trace_id, ← traceForm_apply_apply, h₁, h₂, sub_zero, sub_eq_zero] at this
+
 /-- The upper and lower central series of `L` are orthogonal wrt the trace form of any Lie module
 `M`. -/
 lemma traceForm_eq_zero_if_mem_lcs_of_mem_ucs {x y : L} (k : ℕ)
@@ -393,7 +423,7 @@ variable [IsKilling R L]
 
 /-- If the Killing form of a Lie algebra is non-singular, it remains non-singular when restricted
 to a Cartan subalgebra. -/
-lemma ker_restrictBilinear_of_isCartanSubalgebra_eq_bot
+lemma ker_restrictBilinear_eq_bot_of_isCartanSubalgebra
     [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
     LinearMap.ker (H.restrictBilinear (killingForm R L)) = ⊥ := by
   have h : Codisjoint (rootSpace H 0) (LieModule.posFittingComp R H L) :=
@@ -411,6 +441,11 @@ lemma restrictBilinear_killingForm (H : LieSubalgebra R L) :
     H.restrictBilinear (killingForm R L) = LieModule.traceForm R H L :=
   rfl
 
+@[simp] lemma ker_traceForm_eq_bot_of_isCartanSubalgebra
+    [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
+    LinearMap.ker (LieModule.traceForm R H L) = ⊥ :=
+  ker_restrictBilinear_eq_bot_of_isCartanSubalgebra R L H
+
 /-- The converse of this is true over a field of characteristic zero. There are counterexamples
 over fields with positive characteristic. -/
 instance isSemisimple [IsDomain R] [IsPrincipalIdealRing R] : IsSemisimple R L := by
@@ -425,7 +460,7 @@ instance instIsLieAbelianOfIsCartanSubalgebra
     (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
     IsLieAbelian H :=
   LieModule.isLieAbelian_of_ker_traceForm_eq_bot R H L <|
-    ker_restrictBilinear_of_isCartanSubalgebra_eq_bot R L H
+    ker_restrictBilinear_eq_bot_of_isCartanSubalgebra R L H
 
 end IsKilling
 
@@ -438,8 +473,8 @@ section Field
 open LieModule FiniteDimensional
 open Submodule (span)
 
-lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul
-    [IsLieAbelian L] [IsTriangularizable K L M] (x y : L) :
+lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul [LieAlgebra.IsNilpotent K L]
+    [LinearWeights K L M] [IsTriangularizable K L M] (x y : L) :
     traceForm K L M x y = ∑ χ in weight K L M, finrank K (weightSpace M χ) • (χ x * χ y) := by
   have hxy : ∀ χ : L → K, MapsTo (toEndomorphism K L M x ∘ₗ toEndomorphism K L M y)
       (weightSpace M χ) (weightSpace M χ) :=
@@ -453,34 +488,11 @@ lemma LieModule.traceForm_eq_sum_finrank_nsmul_mul
     (LieSubmodule.iSup_eq_top_iff_coe_toSubmodule.mp <| iSup_weightSpace_eq_top K L M)
   simp only [LinearMap.coeFn_sum, Finset.sum_apply, traceForm_apply_apply,
     LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
-  refine Finset.sum_congr (by simp) (fun χ _ ↦ ?_)
-  suffices _root_.IsNilpotent ((toEndomorphism K L M x ∘ₗ toEndomorphism K L M y).restrict (hxy χ) -
-      algebraMap K _ (χ x * χ y)) by
-    replace this := (LinearMap.isNilpotent_trace_of_isNilpotent this).eq_zero
-    rwa [Module.algebraMap_end_eq_smul_id, map_sub, map_smul, LinearMap.trace_id, sub_eq_zero,
-      smul_eq_mul, mul_comm, ← nsmul_eq_mul] at this
-  set nx := toEndomorphism K L (weightSpace M χ) x - algebraMap K _ (χ x)
-  set ny := toEndomorphism K L (weightSpace M χ) y - algebraMap K _ (χ y)
-  have h_np : _root_.IsNilpotent (χ x • ny + χ y • nx + nx * ny) := by
-    -- This subproof would be much prettier if we had tactics for automatically discharging
-    -- `Commute` and `IsNilpotent` goals.
-    have hx : _root_.IsNilpotent nx := isNilpotent_toEndomorphism_sub_algebraMap M χ x
-    have hy : _root_.IsNilpotent ny := isNilpotent_toEndomorphism_sub_algebraMap M χ y
-    have h : Commute nx ny := by
-      refine Commute.sub_left (Commute.sub_right ?_ (Algebra.commute_algebraMap_right (χ y) _))
-        (Algebra.commute_algebraMap_left (χ x) ny)
-      rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
-    exact (((h.symm.mul_right rfl).smul_left _).add_left
-      (((Commute.refl _).mul_right h).smul_left _)).isNilpotent_add
-      (((h.symm.smul_right _).smul_left _).isNilpotent_add (hy.smul _) (hx.smul _))
-      (h.isNilpotent_mul_right hy)
-  have : (toEndomorphism K L M x ∘ₗ toEndomorphism K L M y).restrict (hxy χ) -
-      algebraMap K _ (χ x * χ y) = χ x • ny + χ y • nx + nx * ny := by
-    ext; simp [smul_sub, smul_comm (χ x) (χ y)]
-  rwa [this]
-
-lemma LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot
-    [IsLieAbelian L] [IsTriangularizable K L M] [FiniteDimensional K L]
+  exact Finset.sum_congr (by simp) (fun χ _ ↦ traceForm_weightSpace_eq K L M χ x y)
+
+@[simp]
+lemma LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot [LieAlgebra.IsNilpotent K L]
+    [LinearWeights K L M] [IsTriangularizable K L M] [FiniteDimensional K L]
     (h : LinearMap.ker (traceForm K L M) = ⊥) :
     span K (range (weight.toLinear K L M)) = ⊤ := by
   by_contra contra
@@ -501,12 +513,9 @@ lemma LieModule.span_weight_eq_top_of_ker_traceForm_eq_bot
 
 /-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular
 Killing form, the corresponding roots span the dual space of `H`. -/
-@[simp]
 lemma LieAlgebra.IsKilling.span_weight_eq_top [FiniteDimensional K L] [IsKilling K L]
     (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [IsTriangularizable K H L] :
     span K (range (weight.toLinear K H L)) = ⊤ := by
-  have : LinearMap.ker (traceForm K H L) = ⊥ := by
-    rw [← restrictBilinear_killingForm, ker_restrictBilinear_of_isCartanSubalgebra_eq_bot]
-  rw [span_weight_eq_top_of_ker_traceForm_eq_bot K H L this]
+  simp
 
 end Field

Mathlib/Algebra/Lie/Submodule.lean

@@ -186,7 +186,7 @@ instance {S : Type*} [Semiring S] [SMul S R] [SMul Sᵐᵒᵖ R] [Module S M] [M
     [IsScalarTower S R M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S N :=
   N.toSubmodule.isCentralScalar
 
-instance : LieModule R L N where
+instance instLieModule : LieModule R L N where
   lie_smul := by intro t x y; apply SetCoe.ext; apply lie_smul
   smul_lie := by intro t x y; apply SetCoe.ext; apply smul_lie
 

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -26,7 +26,7 @@ or `R` has characteristic zero.
 
 ## Main definitions
  * `LieModule.LinearWeights`: a typeclass encoding the fact that a given Lie module has linear
-   weights.
+   weights, and furthermore that the weights vanish on the derived ideal.
  * `LieModule.instLinearWeightsOfCharZero`: a typeclass instance encoding the fact that for an
    Abelian Lie algebra, the weights of any Lie module are linear.
  * `LieModule.instLinearWeightsOfIsLieAbelian`: a typeclass instance encoding the fact that in
@@ -45,10 +45,12 @@ variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
 
 namespace LieModule
 
-/-- A typeclass encoding the fact that a given Lie module has linear weights. -/
+/-- A typeclass encoding the fact that a given Lie module has linear weights, vanishing on the
+derived ideal. -/
 class LinearWeights [LieAlgebra.IsNilpotent R L] : Prop :=
   map_add : ∀ χ : L → R, weightSpace M χ ≠ ⊥ → ∀ x y, χ (x + y) = χ x + χ y
   map_smul : ∀ χ : L → R, weightSpace M χ ≠ ⊥ → ∀ (t : R) x, χ (t • x) = t • χ x
+  map_lie : ∀ χ : L → R, weightSpace M χ ≠ ⊥ → ∀ x y : L, χ ⁅x, y⁆ = 0
 
 /-- A weight of a Lie module, bundled as a linear map. -/
 @[simps]
@@ -59,23 +61,31 @@ def weight.toLinear [LieAlgebra.IsNilpotent R L] [LinearWeights R L M]
   map_add' := LinearWeights.map_add (χ : L → R) (M := M) <| (Finite.mem_toFinset _).mp χ.property
   map_smul' := LinearWeights.map_smul (χ : L → R) (M := M) <| (Finite.mem_toFinset _).mp χ.property
 
+@[simp]
+lemma weight.toLinear_apply_lie [LieAlgebra.IsNilpotent R L] [LinearWeights R L M]
+    [NoZeroSMulDivisors R M] [IsNoetherian R M] (χ : weight R L M) (x y : L) :
+    (χ : L → R) ⁅x, y⁆ = 0 :=
+  LinearWeights.map_lie (χ : L → R) ((Finite.mem_toFinset _).mp χ.property) x y
+
 /-- For an Abelian Lie algebra, the weights of any Lie module are linear. -/
 instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R M] :
-    LinearWeights R L M where
-  map_add := by
+    LinearWeights R L M :=
+  have aux : ∀ (χ : L → R), weightSpace M χ ≠ ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y := by
     have h : ∀ x y, Commute (toEndomorphism R L M x) (toEndomorphism R L M y) := fun x y ↦ by
       rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero]
     intro χ hχ x y
     simp_rw [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, weightSpace, weightSpaceOf,
       LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, Submodule.eta] at hχ
     exact Module.End.map_add_of_iInf_generalizedEigenspace_ne_bot_of_commute
       (toEndomorphism R L M).toLinearMap χ hχ h x y
-  map_smul := by
-    intro χ hχ t x
-    simp_rw [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, weightSpace, weightSpaceOf,
-      LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, Submodule.eta] at hχ
-    exact Module.End.map_smul_of_iInf_generalizedEigenspace_ne_bot
-      (toEndomorphism R L M).toLinearMap χ hχ t x
+  { map_add := aux
+    map_smul := fun χ hχ t x ↦ by
+      simp_rw [Ne.def, ← LieSubmodule.coe_toSubmodule_eq_iff, weightSpace, weightSpaceOf,
+        LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, Submodule.eta] at hχ
+      exact Module.End.map_smul_of_iInf_generalizedEigenspace_ne_bot
+        (toEndomorphism R L M).toLinearMap χ hχ t x
+    map_lie := fun χ hχ t x ↦ by
+      rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_add] }
 
 section FiniteDimensional
 
@@ -101,16 +111,86 @@ lemma zero_lt_finrank_weightSpace {χ : L → R} (hχ : weightSpace M χ ≠ ⊥
   rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
     Nat.cast_pos] at hχ
 
-/-- In characteristic zero, the weights of any finite-dimensional Lie module are linear. -/
+/-- In characteristic zero, the weights of any finite-dimensional Lie module are linear and vanish
+on the derived ideal. -/
 instance instLinearWeightsOfCharZero [CharZero R] :
     LinearWeights R L M where
-  map_add := fun χ hχ x y ↦ by
+  map_add χ hχ x y := by
     rw [← smul_right_inj (zero_lt_finrank_weightSpace hχ).ne', smul_add, ← Pi.smul_apply,
       ← Pi.smul_apply, ← Pi.smul_apply, ← trace_comp_toEndomorphism_weight_space_eq, map_add]
-  map_smul := fun χ hχ t x ↦ by
+  map_smul χ hχ t x := by
     rw [← smul_right_inj (zero_lt_finrank_weightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
       ← Pi.smul_apply (finrank R _), ← trace_comp_toEndomorphism_weight_space_eq, map_smul]
+  map_lie χ hχ x y := by
+    rw [← smul_right_inj (zero_lt_finrank_weightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
+      ← trace_comp_toEndomorphism_weight_space_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
+      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
 
 end FiniteDimensional
 
+variable [LieAlgebra.IsNilpotent R L] [LinearWeights R L M] (χ : L → R)
+
+/-- A type synonym for the `χ`-weight space but with the action of `x : L` on `m : weightSpace M χ`,
+shifted to act as `⁅x, m⁆ - χ x • m`. -/
+def shiftedWeightSpace := weightSpace M χ
+
+namespace shiftedWeightSpace
+
+private lemma aux [h : Nontrivial (shiftedWeightSpace R L M χ)] : weightSpace M χ ≠ ⊥ :=
+  (LieSubmodule.nontrivial_iff_ne_bot _ _ _).mp h
+
+instance : LieRingModule L (shiftedWeightSpace R L M χ) where
+  bracket x m := ⁅x, m⁆ - χ x • m
+  add_lie x y m := by
+    nontriviality shiftedWeightSpace R L M χ
+    simp only [add_lie, LinearWeights.map_add χ (aux R L M χ), add_smul]
+    abel
+  lie_add x m n := by
+    nontriviality shiftedWeightSpace R L M χ
+    simp only [lie_add, LinearWeights.map_add χ (aux R L M χ), smul_add]
+    abel
+  leibniz_lie x y m := by
+    nontriviality shiftedWeightSpace R L M χ
+    simp only [lie_sub, lie_smul, lie_lie, LinearWeights.map_lie χ (aux R L M χ), zero_smul,
+      sub_zero, smul_sub, smul_comm (χ x)]
+    abel
+
+@[simp] lemma coe_lie_shiftedWeightSpace_apply (x : L) (m : shiftedWeightSpace R L M χ) :
+    ⁅x, m⁆ = ⁅x, (m : M)⁆ - χ x • m :=
+  rfl
+
+instance : LieModule R L (shiftedWeightSpace R L M χ) where
+  smul_lie t x m := by
+    nontriviality shiftedWeightSpace R L M χ
+    apply Subtype.ext
+    simp only [coe_lie_shiftedWeightSpace_apply, smul_lie, LinearWeights.map_smul χ (aux R L M χ),
+      SetLike.val_smul, smul_sub, sub_right_inj, smul_assoc t]
+  lie_smul t x m := by
+    nontriviality shiftedWeightSpace R L M χ
+    apply Subtype.ext
+    simp only [coe_lie_shiftedWeightSpace_apply, lie_smul, LinearWeights.map_smul χ (aux R L M χ),
+      SetLike.val_smul, smul_sub, sub_right_inj, smul_comm t]
+
+/-- Forgetting the action of `L`, the spaces `weightSpace M χ` and `shiftedWeightSpace R L M χ` are
+equivalent. -/
+@[simps] def shift : weightSpace M χ ≃ₗ[R] shiftedWeightSpace R L M χ where
+  toFun := id
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  invFun := id
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+lemma toEndomorphism_eq (x : L) :
+    toEndomorphism R L (shiftedWeightSpace R L M χ) x =
+    (shift R L M χ).conj (toEndomorphism R L (weightSpace M χ) x - χ x • LinearMap.id) := by
+  ext; simp [LinearEquiv.conj_apply]
+
+/-- By Engel's theorem, if `M` is Noetherian, the shifted action `⁅x, m⁆ - χ x • m` makes the
+`χ`-weight space into a nilpotent Lie module. -/
+instance [IsNoetherian R M] : IsNilpotent R L (shiftedWeightSpace R L M χ) :=
+  LieModule.isNilpotent_iff_forall'.mpr fun x ↦ isNilpotent_toEndomorphism_sub_algebraMap M χ x
+
+end shiftedWeightSpace
+
 end LieModule